diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index e7f7e4088..42c6eb1ca 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -200,6 +200,51 @@
   + lemma `continuous_uncurry`
   + lemma `curry_continuous`
   + lemma `uncurry_continuous`
+- in file `normedtype.v`,
+  + new lemma `continuous_within_itvP`.
+
+- in `ereal.v`:
+  + lemma `ereal_supy`
+
+- in `mathcomp_extra.v`:
+  + lemmas `last_filterP`,
+    `path_lt_filter0`, `path_lt_filterT`, `path_lt_head`, `path_lt_last_filter`,
+	`path_lt_le_last`
+
+- in file `realfun.v`,
+  + new definitions `itv_partition`, `itv_partitionL`, `itv_partitionR`, 
+    `variation`, `variations`, `bounded_variation`, `total_variation`, 
+    `neg_tv`, and `pos_tv`.
+
+  + new lemmas `left_right_continuousP`,
+    `nondecreasing_funN`, `nonincreasing_funN`
+
+  + new lemmas `itv_partition_nil`, `itv_partition_cons`, `itv_partition1`,
+    `itv_partition_size_neq0`, `itv_partitionxx`, `itv_partition_le`,
+    `itv_partition_cat`, `itv_partition_nth_size`,
+    `itv_partition_nth_ge`, `itv_partition_nth_le`, 
+    `nondecreasing_fun_itv_partition`, `nonincreasing_fun_itv_partition`, 
+    `itv_partitionLP`, `itv_partitionRP`, `in_itv_partition`, 
+    `notin_itv_partition`, `itv_partition_rev`,
+
+  + new lemmas `variation_zip`, `variation_prev`, `variation_next`, `variation_nil`,
+    `variation_ge0`, `variationN`, `variation_le`, `nondecreasing_variation`, 
+    `nonincreasing_variation`, `variationD`, `variation_itv_partitionLR`, 
+    `le_variation`, `variation_opp_rev`, `variation_rev_opp`
+
+  + new lemmas `variations_variation`, `variations_neq0`, `variationsN`, `variationsxx`
+
+  + new lemmas `bounded_variationxx`, `bounded_variationD`, `bounded_variationN`,
+    `bounded_variationl`, `bounded_variationr`, `variations_opp`, 
+    `nondecreasing_bounded_variation`
+
+  + new lemmas `total_variationxx`, `total_variation_ge`, `total_variation_ge0`,
+    `bounded_variationP`, `nondecreasing_total_variation`, `total_variationN`,
+	  `total_variation_le`, `total_variationD`, `neg_tv_nondecreasing`,
+    `total_variation_pos_neg_tvE`, `fine_neg_tv_nondecreasing`,
+    `neg_tv_bounded_variation`, `total_variation_right_continuous`,
+    `neg_tv_right_continuous`, `total_variation_opp`,
+    `total_variation_left_continuous`, `total_variation_continuous`
 
 ### Changed
 
diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
index 59c5481c8..7e4e7091b 100644
--- a/classical/mathcomp_extra.v
+++ b/classical/mathcomp_extra.v
@@ -934,3 +934,54 @@ Qed.
 
 Definition monotonous d (T : porderType d) (pT : predType T) (A : pT) (f : T -> T) :=
   {in A &, {mono f : x y / (x <= y)%O}} \/ {in A &, {mono f : x y /~ (x <= y)%O}}.
+
+(* NB: these lemmas have been introduced to develop the theory of bounded variation *)
+Section path_lt.
+Context d {T : orderType d}.
+Implicit Types (a b c : T) (s : seq T).
+
+Lemma last_filterP a (P : pred T) s :
+  P a -> P (last a [seq x <- s | P x]).
+Proof.
+by elim: s a => //= t1 t2 ih a Pa; case: ifPn => //= Pt1; exact: ih.
+Qed.
+
+Lemma path_lt_filter0 a s : path <%O a s -> [seq x <- s | (x < a)%O] = [::].
+Proof.
+move=> /lt_path_min/allP sa; rewrite -(filter_pred0 s).
+apply: eq_in_filter => x xs.
+by apply/negbTE; have := sa _ xs; rewrite ltNge; apply: contra => /ltW.
+Qed.
+
+Lemma path_lt_filterT a s : path <%O a s -> [seq x <- s | (a < x)%O] = s.
+Proof.
+move=> /lt_path_min/allP sa; rewrite -[RHS](filter_predT s).
+by apply: eq_in_filter => x xs; exact: sa.
+Qed.
+
+Lemma path_lt_head a b s : (a < b)%O -> path <%O b s -> path <%O a s.
+Proof.
+by elim: s b => // h t ih b /= ab /andP[bh ->]; rewrite andbT (lt_trans ab).
+Qed.
+
+(* TODO: this lemma feels a bit too technical, generalize? *)
+Lemma path_lt_last_filter a b c s :
+  (a < c)%O -> (c < b)%O -> path <%O a s -> last a s = b ->
+  last c [seq x <- s | (c < x)%O] = b.
+Proof.
+elim/last_ind : s a b c => /= [|h t ih a b c ac cb].
+  move=> a b c ac cb _ ab.
+  by apply/eqP; rewrite eq_le (ltW cb) -ab (ltW ac).
+rewrite rcons_path => /andP[ah ht]; rewrite last_rcons => tb.
+by rewrite filter_rcons tb cb last_rcons.
+Qed.
+
+Lemma path_lt_le_last a s : path <%O a s -> (a <= last a s)%O.
+Proof.
+elim: s a => // a [_ c /andP[/ltW//]|b t ih i/= /and3P[ia ab bt]] /=.
+have /= := ih a; rewrite ab bt => /(_ erefl).
+by apply: le_trans; exact/ltW.
+Qed.
+
+End path_lt.
+Arguments last_filterP {d T a} P s.
diff --git a/theories/ereal.v b/theories/ereal.v
index 896c4fc7e..1201c4ea3 100644
--- a/theories/ereal.v
+++ b/theories/ereal.v
@@ -511,6 +511,11 @@ case: xgetP => /=; first by move=> _ -> -[] /ubP geS _; apply geS.
 by case: (ereal_supremums_neq0 S) => /= x0 Sx0; move/(_ x0).
 Qed.
 
+Lemma ereal_supy S : S +oo -> ereal_sup S = +oo.
+Proof.
+by move=> Soo; apply/eqP; rewrite eq_le leey/=; exact: ereal_sup_ub.
+Qed.
+
 Lemma ereal_sup_le S x : (exists2 y, S y & x <= y) -> x <= ereal_sup S.
 Proof. by move=> [y Sy] /le_trans; apply; exact: ereal_sup_ub. Qed.
 
diff --git a/theories/normedtype.v b/theories/normedtype.v
index 7b5526635..01ea11f42 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -2075,6 +2075,51 @@ by apply: xe_A => //; rewrite eq_sym.
 Qed.
 Arguments cvg_at_leftE {R V} f x.
 
+Lemma continuous_within_itvP {R : realType } a b (f : R -> R) :
+  a < b ->
+  {within `[a,b], continuous f} <->
+  {in `]a,b[, continuous f} /\ f @ a^'+ --> f a /\ f @b^'- --> f b.
+Proof.
+move=> ab; split=> [abf|].
+  split.
+    suff : {in `]a, b[%classic, continuous f}.
+      by move=> P c W; apply: P; rewrite inE.
+    rewrite -continuous_open_subspace; last exact: interval_open.
+    by move: abf; exact/continuous_subspaceW/subset_itvW.
+  have [aab bab] : a \in `[a, b] /\ b \in `[a, b].
+    by rewrite !in_itv/= !lexx (ltW ab).
+  split; apply/cvgrPdist_lt => eps eps_gt0 /=.
+  + move/continuous_withinNx/cvgrPdist_lt/(_ _ eps_gt0) : (abf a).
+    rewrite /dnbhs/= near_withinE !near_simpl// /prop_near1 /nbhs/=.
+    rewrite -nbhs_subspace_in// /within/= near_simpl.
+    apply: filter_app; exists (b - a); rewrite /= ?subr_gt0// => c cba + ac.
+    apply=> //; rewrite ?gt_eqF// !in_itv/= (ltW ac)/=; move: cba => /=.
+    by rewrite ltr0_norm ?subr_lt0// opprB ltr_add2r => /ltW.
+  + move/continuous_withinNx/cvgrPdist_lt/(_ _ eps_gt0) : (abf b).
+    rewrite /dnbhs/= near_withinE !near_simpl /prop_near1 /nbhs/=.
+    rewrite -nbhs_subspace_in// /within/= near_simpl.
+    apply: filter_app; exists (b - a); rewrite /= ?subr_gt0// => c cba + ac.
+    apply=> //; rewrite ?lt_eqF// !in_itv/= (ltW ac)/= andbT; move: cba => /=.
+    by rewrite gtr0_norm ?subr_gt0// ltr_add2l ltr_oppr opprK => /ltW.
+case=> ctsoo [ctsL ctsR]; apply/subspace_continuousP => x /andP[].
+rewrite !bnd_simp/= !le_eqVlt => /predU1P[<-{x}|ax] /predU1P[|].
+- by move/eqP; rewrite lt_eqF.
+- move=> _; apply/cvgrPdist_lt => eps eps_gt0 /=.
+  move/cvgrPdist_lt/(_ _ eps_gt0): ctsL; rewrite /at_right !near_withinE.
+  apply: filter_app; exists (b - a); rewrite /= ?subr_gt0// => c cba + ac.
+  have : a <= c by move: ac => /andP[].
+  by rewrite le_eqVlt => /predU1P[->|/[swap] /[apply]//]; rewrite subrr normr0.
+- move=> ->; apply/cvgrPdist_lt => eps eps_gt0 /=.
+  move/cvgrPdist_lt/(_ _ eps_gt0): ctsR; rewrite /at_left !near_withinE.
+  apply: filter_app; exists (b - a); rewrite /= ?subr_gt0 // => c cba + ac.
+  have : c <= b by move: ac => /andP[].
+  by rewrite le_eqVlt => /predU1P[->|/[swap] /[apply]//]; rewrite subrr normr0.
+- move=> xb; have aboox : x \in `]a, b[ by rewrite !in_itv/= ax.
+  rewrite within_interior; first exact: ctsoo.
+  suff : `]a, b[ `<=` interior `[a, b] by exact.
+  by rewrite -open_subsetE; [exact: subset_itvW| exact: interval_open].
+Qed.
+
 (* TODO: generalize to R : numFieldType *)
 Section hausdorff.
 
diff --git a/theories/realfun.v b/theories/realfun.v
index efdda2280..e4502e512 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -14,16 +14,30 @@ From HB Require Import structures.
 (* numbers (e.g., the continuity of the inverse of a continuous function).    *)
 (*                                                                            *)
 (* ```                                                                        *)
-(*        nondecreasing_fun f == the function f is non-decreasing             *)
-(*        nonincreasing_fun f == the function f is non-increasing             *)
-(*           increasing_fun f == the function f is (strictly) increasing      *)
-(*           decreasing_fun f == the function f is (strictly) decreasing      *)
+(*      nondecreasing_fun f == the function f is non-decreasing               *)
+(*      nonincreasing_fun f == the function f is non-increasing               *)
+(*         increasing_fun f == the function f is (strictly) increasing        *)
+(*         decreasing_fun f == the function f is (strictly) decreasing        *)
 (*                                                                            *)
-(*  lime_sup f a/lime_inf f a == limit sup/inferior of the extended           *)
-(*                               real-valued function f at point a            *)
+(*   derivable_oo_continuous_bnd f x y == f is derivable on `]x, y[ and       *)
+(*                             continuous up to the boundary                  *)
 (*                                                                            *)
-(* derivable_oo_continuous_bnd f x y == f is derivable on `]x, y[ and         *)
-(*                               continuous up to the boundary                *)
+(*      itv_partition a b s == s is a partition of the interval `[a, b]       *)
+(*       itv_partitionL s c == the left side of splitting a partition at c    *)
+(*       itv_partitionR s c == the right side of splitting a partition at c   *)
+(*        variation a b f s == the sum of f at all points in the partition s  *)
+(*         variations a b f == the set of all variations of f between a and b *)
+(*  bounded_variation a b f == all variations of f are bounded                *)
+(*    total_variation a b f == the sup over all variations of f from a to b   *)
+(*             neg_tv a f x == the decreasing component of f                  *)
+(*             pos_tv a f x == the increasing component of f                  *)
+(*                                                                            *)
+(* ```                                                                        *)
+(*                                                                            *)
+(* * Limit superior and inferior for functions:                               *)
+(* ```                                                                        *)
+(*   lime_sup f a/lime_inf f a == limit sup/inferior of the extended real-    *)
+(*                             valued function f at point a                   *)
 (* ```                                                                        *)
 (*                                                                            *)
 (******************************************************************************)
@@ -49,6 +63,23 @@ Notation "'increasing_fun' f" := ({mono f : n m / (n <= m)%O >-> (n <= m)%O})
 Notation "'decreasing_fun' f" := ({mono f : n m / (n <= m)%O >-> (n >= m)%O})
   (at level 10).
 
+Lemma nondecreasing_funN {R : realType} a b (f : R -> R) :
+  {in `[a, b] &, nondecreasing_fun f} <->
+  {in `[a, b] &, nonincreasing_fun (\- f)}.
+Proof.
+split=> [h m n mab nab mn|h m n mab nab mn]; first by rewrite lerNr opprK h.
+by rewrite -(opprK (f n)) -lerNr h.
+Qed.
+
+Lemma nonincreasing_funN {R : realType} a b (f : R -> R) :
+  {in `[a, b] &, nonincreasing_fun f} <->
+  {in `[a, b] &, nondecreasing_fun (\- f)}.
+Proof.
+apply: iff_sym; apply: (iff_trans (nondecreasing_funN a b (\- f))).
+rewrite [in X in _ <-> X](_ : f = \- (\- f))//.
+by apply/funext => x /=; rewrite opprK.
+Qed.
+
 Section fun_cvg.
 
 Section fun_cvg_realFieldType.
@@ -87,6 +118,18 @@ apply: near_eq_cvg; near do rewrite subrK; exists M.
 by rewrite num_real.
 Unshelve. all: by end_near. Qed.
 
+Lemma left_right_continuousP {T : topologicalType} (f : R -> T) x :
+  f @ x^'- --> f x /\ f @ x^'+ --> f x <-> f @ x --> f x.
+Proof.
+split; last by move=> cts; split; exact: cvg_within_filter.
+move=> [+ +] U /= Uz => /(_ U Uz) + /(_ U Uz); near_simpl.
+rewrite !near_withinE => lf rf; apply: filter_app lf; apply: filter_app rf.
+near=> t => xlt xgt; have := @real_leVge R x t; rewrite !num_real.
+move=> /(_ isT isT) /orP; rewrite !le_eqVlt => -[|] /predU1P[|//].
+- by move=> <-; exact: nbhs_singleton.
+- by move=> ->; exact: nbhs_singleton.
+Unshelve. all: by end_near. Qed.
+
 Lemma cvg_at_right_left_dnbhs (f : R -> R) (p : R) (l : R) :
   f x @[x --> p^'+] --> l -> f x @[x --> p^'-] --> l ->
   f x @[x --> p^'] --> l.
@@ -105,7 +148,6 @@ rewrite neq_lt => /orP[tp|pt].
   move=> z/= + _ => /lt_le_trans; apply.
   by rewrite ler_pdivrMr// ler_pMr// ler1n.
 Unshelve. all: by end_near. Qed.
-
 End fun_cvg_realFieldType.
 
 Section cvgr_fun_cvg_seq.
@@ -250,36 +292,36 @@ have supf : has_sup [set f x | x in [set` Interval (BRight a) b]].
   - exists (f ((a + t) / 2)), ((a + t) / 2) => //=.
     by rewrite in_itv/= midf_lt// midf_le// ltW.
   - by exists (f (a + 1)), (a + 1).
-  - by exists (f (a + 1)), (a + 1) => //=; rewrite in_itv/= ltr_addl andbT.
+  - by exists (f (a + 1)), (a + 1) => //=; rewrite in_itv/= ltrDl andbT.
 apply/cvgrPdist_le => _/posnumP[e].
 have {supf} [p [ap pb]] :
     exists p, [/\ a < p, (BLeft p < b)%O & M - e%:num <= f p].
   have [_ -[p apb] <- /ltW efp] := sup_adherent (gt0 e) supf.
   move: apb; rewrite /= in_itv/= -[X in _ && X]/(BLeft p < b)%O => /andP[ap pb].
   by exists p; split.
-rewrite ler_subl_addr {}/M.
+rewrite lerBlDr {}/M.
 move: b ab pb lef ubf => [[|] b|[//|]] ab pb lef ubf; set M := sup _ => Mefp.
 - near=> r; rewrite ler_distl; apply/andP; split.
-  + suff: f r <= M by apply: le_trans; rewrite ler_subl_addr ler_addl.
+  + suff: f r <= M by apply: le_trans; rewrite lerBlDr lerDl.
     apply: sup_ub => //=; exists r => //; rewrite in_itv/=.
     by apply/andP; split; near: r; [exact: nbhs_right_gt|exact: nbhs_right_lt].
-  + rewrite (le_trans Mefp)// ler_add2r lef//=; last 2 first.
+  + rewrite (le_trans Mefp)// lerD2r lef//=; last 2 first.
       by rewrite in_itv/= ap.
       by near: r; exact: nbhs_right_le.
     apply/andP; split; near: r; [exact: nbhs_right_gt|exact: nbhs_right_lt].
 - near=> r; rewrite ler_distl; apply/andP; split.
-  + suff: f r <= M by apply: le_trans; rewrite ler_subl_addr ler_addl.
+  + suff: f r <= M by apply: le_trans; rewrite lerBlDr lerDl.
     apply: sup_ub => //=; exists r => //; rewrite in_itv/=.
     by apply/andP; split; near: r; [exact: nbhs_right_gt|exact: nbhs_right_le].
-  + rewrite (le_trans Mefp)// ler_add2r lef//=; last 2 first.
+  + rewrite (le_trans Mefp)// lerD2r lef//=; last 2 first.
       by rewrite in_itv/= ap.
       by near: r; exact: nbhs_right_le.
     by apply/andP; split; near: r; [exact: nbhs_right_gt|exact: nbhs_right_le].
 - near=> r; rewrite ler_distl; apply/andP; split.
-  suff: f r <= M by apply: le_trans; rewrite ler_subl_addr ler_addl.
+  suff: f r <= M by apply: le_trans; rewrite lerBlDr lerDl.
   apply: sup_ub => //=; exists r => //; rewrite in_itv/= andbT.
     by near: r; apply: nbhs_right_gt.
-  rewrite (le_trans Mefp)// ler_add2r lef//.
+  rewrite (le_trans Mefp)// lerD2r lef//.
   - by rewrite in_itv/= andbT; near: r; exact: nbhs_right_gt.
   - by rewrite in_itv/= ap.
   - by near: r; exact: nbhs_right_le.
@@ -302,7 +344,7 @@ Lemma nondecreasing_at_right_cvgr f a (b : itv_bound R) : (BRight a < b)%O ->
 Proof.
 move=> ab nif hlb; set M := inf _.
 have ndNf : {in Interval (BRight a) b &, nonincreasing_fun (\- f)}.
-  by move=> r s rab sab /nif; rewrite ler_opp2; exact.
+  by move=> r s rab sab /nif; rewrite lerN2; exact.
 have hub : has_ubound [set (\- f) x | x in [set` Interval (BRight a) b]].
   apply/has_ub_lbN; rewrite image_comp/=.
   rewrite [X in has_lbound X](_ : _ = f @` [set` Interval (BRight a) b])//.
@@ -442,7 +484,7 @@ have [lnoo|lnoo] := eqVneq l -oo.
   rewrite in_itv/= -[X in _ && X]/(BLeft y < b)%O/= => /andP[ay yb] <- fyM.
   exists (y - a)%R => /=; first by rewrite subr_gt0.
   move=> z /= + az.
-  rewrite ltr0_norm ?subr_lt0// opprB ltr_subl_addr subrK => zy.
+  rewrite ltr0_norm ?subr_lt0// opprB ltrBlDr subrK => zy.
   rewrite (le_trans _ (ltW fyM))// ndf ?ltW//.
     by rewrite in_itv/= -[X in _ && X]/(BLeft z < b)%O/= az/= (lt_trans _ yb).
   by rewrite in_itv/= -[X in _ && X]/(BLeft y < b)%O/= (lt_trans az zy).
@@ -461,7 +503,7 @@ have [fpoo|fpoo] := pselect {in Interval (BRight a) b, forall x, f x = +oo}.
   move: b ab ndf lnoo Snoo fpoo => [[|] s|[//|]] ab ndf lnoo Snoo fpoo /=.
   - by exists ((a + s) / 2)%R; rewrite ?fpoo// in_itv/= !midf_lt.
   - by exists ((a + s) / 2)%R; rewrite ?fpoo// in_itv/= !(midf_lt, midf_le)// ltW.
-  - by exists (a + 1)%R; rewrite ?fpoo// in_itv/= andbT ltr_addl.
+  - by exists (a + 1)%R; rewrite ?fpoo// in_itv/= andbT ltrDl.
 have [/ereal_inf_pinfty lpoo|lpoo] := eqVneq l +oo.
   by exfalso; apply/fpoo => r rab; rewrite (lpoo (f r))//; exists r.
 have l_fin_num : l \is a fin_num by rewrite fin_numE lpoo lnoo.
@@ -514,7 +556,7 @@ have <- : inf [set g x | x in [set` Interval (BRight a) b]] = fine l.
       + exists (g ((a + s) / 2))%R, ((a + s) / 2)%R => //=.
         by rewrite /= in_itv/= !(midf_lt, midf_le)// ltW.
       + exists (g (a + 1)%R), (a + 1)%R => //=.
-        by rewrite in_itv/= andbT ltr_addl.
+        by rewrite in_itv/= andbT ltrDl.
   rewrite fineK//; apply/eqP; rewrite eq_le; apply/andP; split; last first.
     apply: le_ereal_inf => _ /= [_ [m _] <-] <-.
     rewrite /g; case: ifPn => [/andP[am mx]|].
@@ -549,8 +591,8 @@ suff: g x @[x --> a^'+] --> inf [set g x | x in [set` Interval (BRight a) b]].
   suff nx : (n < x)%R by rewrite ltNge xn in nx.
   near: n; exists ((x - a) / 2)%R; first by rewrite /= divr_gt0// subr_gt0.
   move=> y /= /[swap] ay.
-  rewrite ltr0_norm// ?subr_lt0// opprB ltr_subl_addr => /lt_le_trans; apply.
-  by rewrite -ler_subr_addr ler_pdivr_mulr// ler_pmulr// ?ler1n// subr_gt0.
+  rewrite ltr0_norm// ?subr_lt0// opprB ltrBlDr => /lt_le_trans; apply.
+  by rewrite -lerBrDr ler_pdivrMr// ler_pMr// ?ler1n// subr_gt0.
 apply: nondecreasing_at_right_cvgr => //.
 - move=> m n; rewrite !in_itv/= -[X in _ && X]/(BLeft m < b)%O.
   rewrite -[X in _ -> _ && X -> _]/(BLeft n < b)%O.
@@ -1210,6 +1252,7 @@ have : f a >= f b by rewrite (itvP xfafb).
 by case: ltrgtP xfafb => // ->.
 Qed.
 
+
 Lemma segment_inc_surj_continuous a b f :
     {in `[a, b] &, {mono f : x y / x <= y}} -> set_surj `[a, b] `[f a, f b] f ->
   {within `[a, b], continuous f}.
@@ -1518,3 +1561,866 @@ End is_derive_inverse.
 
 #[global] Hint Extern 0 (is_derive _ _ (fun _ => (_ _)^-1) _) =>
   (eapply is_deriveV; first by []) : typeclass_instances.
+
+Section interval_partition.
+Context {R : realType}.
+Implicit Type (a b : R) (s : seq R).
+
+(** a :: s is a partition of the interval [a, b] *)
+Definition itv_partition a b s := [/\ path <%R a s & last a s == b].
+
+Lemma itv_partition_nil a b : itv_partition a b [::] -> a = b.
+Proof. by move=> [_ /eqP <-]. Qed.
+
+Lemma itv_partition_cons a b x s :
+  itv_partition a b (x :: s) -> itv_partition x b s.
+Proof. by rewrite /itv_partition/= => -[/andP[]]. Qed.
+
+Lemma itv_partition1 a b : a < b -> itv_partition a b [:: b].
+Proof. by rewrite /itv_partition /= => ->. Qed.
+
+Lemma itv_partition_size_neq0 a b s :
+  (size s > 0)%N -> itv_partition a b s -> a < b.
+Proof.
+elim: s a => // x [_ a _|h t ih a _]; rewrite /itv_partition /=.
+  by rewrite andbT => -[ax /eqP <-].
+move=> [] /andP[ax /andP[xy] ht /eqP tb].
+by rewrite (lt_trans ax)// ih// /itv_partition /= xy/= tb.
+Qed.
+
+Lemma itv_partitionxx a s : itv_partition a a s -> s = [::].
+Proof.
+case: s => //= h t [/= /andP[ah /lt_path_min/allP ht] /eqP hta].
+suff : h < a by move/lt_trans => /(_ _ ah); rewrite ltxx.
+apply/ht; rewrite -hta.
+by have := mem_last h t; rewrite inE hta lt_eqF.
+Qed.
+
+Lemma itv_partition_le a b s : itv_partition a b s -> a <= b.
+Proof.
+case: s => [/itv_partition_nil ->//|h t /itv_partition_size_neq0 - /(_ _)/ltW].
+exact.
+Qed.
+
+Lemma itv_partition_cat a b c s t :
+  itv_partition a b s -> itv_partition b c t -> itv_partition a c (s ++ t).
+Proof.
+rewrite /itv_partition => -[sa /eqP asb] [bt btc].
+by rewrite cat_path// sa /= last_cat asb.
+Qed.
+
+Lemma itv_partition_nth_size def a b s : itv_partition a b s ->
+  nth def (a :: s) (size s) = b.
+Proof.
+by elim: s a => [a/= /itv_partition_nil//|y t ih a /= /itv_partition_cons/ih].
+Qed.
+
+Lemma itv_partition_nth_ge a b s m : (m < (size s).+1)%N ->
+  itv_partition a b s -> a <= nth b (a :: s) m.
+Proof.
+elim: m s a b => [s a b _//|n ih [//|h t] a b].
+rewrite ltnS => nh [/= /andP[ah ht] lb].
+by rewrite (le_trans (ltW ah))// ih.
+Qed.
+
+Lemma itv_partition_nth_le a b s m : (m < (size s).+1)%N ->
+  itv_partition a b s -> nth b (a :: s) m <= b.
+Proof.
+elim: m s a => [s a _|n ih]; first exact: itv_partition_le.
+by move=> [//|a h t /= nt] H; rewrite ih//; exact: itv_partition_cons H.
+Qed.
+
+Lemma nondecreasing_fun_itv_partition a b f s :
+  {in `[a, b] &, nondecreasing_fun f} -> itv_partition a b s ->
+  let F : nat -> R := f \o nth b (a :: s) in
+  forall k, (k < size s)%N -> F k <= F k.+1.
+Proof.
+move=> ndf abs F k ks.
+have [_] := nondecreasing_seqP F; apply => m n mn; rewrite /F/=.
+have [ms|ms] := ltnP m (size s).+1; last first.
+  rewrite nth_default//.
+  have [|ns] := ltnP n (size s).+1; last by rewrite nth_default.
+  by move=> /(leq_ltn_trans mn); rewrite ltnS leqNgt ms.
+have [ns|ns] := ltnP n (size s).+1; last first.
+  rewrite [in leRHS]nth_default//=; apply/ndf/itv_partition_nth_le => //.
+    by rewrite in_itv/= itv_partition_nth_le// andbT itv_partition_nth_ge.
+  by rewrite in_itv/= lexx andbT; exact: (itv_partition_le abs).
+move: abs; rewrite /itv_partition => -[] sa sab.
+move: mn; rewrite leq_eqVlt => /predU1P[->//|mn].
+apply/ndf/ltW/sorted_ltn_nth => //=; last exact: lt_trans.
+  by rewrite in_itv/= itv_partition_nth_le// andbT itv_partition_nth_ge.
+by rewrite in_itv/= itv_partition_nth_le// andbT itv_partition_nth_ge.
+Qed.
+
+Lemma nonincreasing_fun_itv_partition a b f s :
+  {in `[a, b] &, nonincreasing_fun f} -> itv_partition a b s ->
+  let F : nat -> R := f \o nth b (a :: s) in
+  forall k, (k < size s)%N -> F k.+1 <= F k.
+Proof.
+move/nonincreasing_funN => ndNf abs F k ks; rewrite -(opprK (F k)) ler_oppr.
+exact: (nondecreasing_fun_itv_partition ndNf abs).
+Qed.
+
+(** given a partition of [a, b] and c, returns a partition of [a, c] *)
+Definition itv_partitionL s c := rcons [seq x <- s | x < c] c.
+
+Lemma itv_partitionLP a b c s : a < c -> c < b -> itv_partition a b s ->
+  itv_partition a c (itv_partitionL s c).
+Proof.
+move=> ac bc [] al /eqP htb; split.
+  rewrite /itv_partitionL rcons_path/=; apply/andP; split.
+    by apply: path_filter => //; exact: lt_trans.
+  exact: (last_filterP [pred x | x < c]).
+by rewrite /itv_partitionL last_rcons.
+Qed.
+
+(** given a partition of [a, b] and c, returns a partition of [c, b] *)
+Definition itv_partitionR s c := [seq x <- s | c < x].
+
+Lemma itv_partitionRP a b c s : a < c -> c < b -> itv_partition a b s ->
+  itv_partition c b (itv_partitionR s c).
+Proof.
+move=> ac cb [] sa /eqP alb; rewrite /itv_partition; split.
+  move: sa; rewrite lt_path_sortedE => /andP[allas ss].
+  rewrite lt_path_sortedE filter_all/=.
+  by apply: sorted_filter => //; exact: lt_trans.
+exact/eqP/(path_lt_last_filter ac).
+Qed.
+
+Lemma in_itv_partition c s : sorted <%R s -> c \in s ->
+  s = itv_partitionL s c ++ itv_partitionR s c.
+Proof.
+elim: s c => // h t ih c /= ht.
+rewrite inE => /predU1P[->{c}/=|ct].
+  rewrite ltxx /itv_partitionL /= ltxx /itv_partitionR/= path_lt_filter0//=.
+  by rewrite path_lt_filterT.
+rewrite /itv_partitionL/=; case: ifPn => [hc|].
+  by rewrite ltNge (ltW hc)/= /= [in LHS](ih _ _ ct)//; exact: path_sorted ht.
+rewrite -leNgt le_eqVlt => /predU1P[ch|ch].
+  by rewrite ch ltxx path_lt_filter0//= /itv_partitionR path_lt_filterT.
+move: ht; rewrite lt_path_sortedE => /andP[/allP/(_ _ ct)].
+by move=> /lt_trans-/(_ _ ch); rewrite ltxx.
+Qed.
+
+Lemma notin_itv_partition c s : sorted <%R s -> c \notin s ->
+  s = [seq x <- s | x < c] ++ itv_partitionR s c.
+Proof.
+elim: s c => // h t ih c /= ht.
+rewrite inE negb_or => /andP[]; rewrite neq_lt => /orP[ch|ch] ct.
+  rewrite ch ltNge (ltW ch)/= path_lt_filter0/= /itv_partitionR; last first.
+    exact: path_lt_head ht.
+  by rewrite path_lt_filterT//; exact: path_lt_head ht.
+by rewrite ch/= ltNge (ltW ch)/= -ih//; exact: path_sorted ht.
+Qed.
+
+Lemma itv_partition_rev a b s : itv_partition a b s ->
+  itv_partition (- b) (- a) (rev (belast (- a) (map -%R s))).
+Proof.
+move=> [sa /eqP alb]; split.
+  rewrite (_ : - b = last (- a) (map -%R s)); last by rewrite last_map alb.
+  rewrite rev_path// path_map.
+  by apply: sub_path sa => x y xy/=; rewrite ltr_oppr opprK.
+case: s sa alb => [_ <-//|h t] /= /andP[ah ht] <-{b}.
+by rewrite rev_cons last_rcons.
+Qed.
+
+End interval_partition.
+
+Section variation.
+Context {R : realType}.
+Implicit Types (a b : R) (f g : R -> R).
+
+Definition variation a b f s := let F := f \o nth b (a :: s) in
+  \sum_(0 <= n < size s) `|F n.+1 - F n|%R.
+
+Lemma variation_zip a b f s : itv_partition a b s ->
+  variation a b f s = \sum_(x <- zip s (a :: s)) `|f x.1 - f x.2|.
+Proof.
+elim: s a b => // [a b|h t ih a b].
+  by rewrite /itv_partition /= => -[_ /eqP <-]; rewrite /variation/= !big_nil.
+rewrite /itv_partition /variation => -[]/= /andP[ah ht] /eqP htb.
+rewrite big_nat_recl//= big_cons/=; congr +%R.
+have /ih : itv_partition h b t by split => //; exact/eqP.
+by rewrite /variation => ->; rewrite !big_seq; apply/eq_bigr => r rt.
+Qed.
+
+(* NB: not used yet but should allow for "term-by-term" comparisons *)
+Lemma variation_prev a b f s : itv_partition a b s ->
+  variation a b f s = \sum_(x <- s) `|f x - f (prev (locked (a :: s)) x)|.
+Proof.
+move=> [] sa /eqP asb; rewrite /variation [in LHS]/= (big_nth b) !big_nat.
+apply: eq_bigr => i /andP[_ si]; congr (`| _ - f _ |).
+rewrite -lock.
+rewrite prev_nth inE gt_eqF; last first.
+  rewrite -[a]/(nth b (a :: s) 0) -[ltRHS]/(nth b (a :: s) i.+1).
+  exact: lt_sorted_ltn_nth.
+rewrite orFb mem_nth// index_uniq//.
+  by apply: set_nth_default => /=; rewrite ltnS ltnW.
+by apply: (sorted_uniq lt_trans) => //; apply: path_sorted sa.
+Qed.
+
+Lemma variation_next a b f s : itv_partition a b s ->
+  variation a b f s =
+  \sum_(x <- belast a s) `|f (next (locked (a :: s)) x) - f x|.
+Proof.
+move=> [] sa /eqP asb; rewrite /variation [in LHS]/= (big_nth b) !big_nat.
+rewrite size_belast; apply: eq_bigr => i /andP[_ si].
+congr (`| f _ - f _ |); last first.
+  by rewrite lastI -cats1 nth_cat size_belast// si.
+rewrite -lock next_nth.
+rewrite {1}lastI mem_rcons inE mem_nth ?size_belast// orbT.
+rewrite lastI -cats1 index_cat mem_nth ?size_belast//.
+rewrite index_uniq ?size_belast//.
+  exact: set_nth_default.
+have /lt_sorted_uniq : sorted <%R (a :: s) by [].
+by rewrite lastI rcons_uniq => /andP[].
+Qed.
+
+Lemma variation_nil a b f : variation a b f [::] = 0.
+Proof. by rewrite /variation/= big_nil. Qed.
+
+Lemma variation_ge0 a b f s : 0 <= variation a b f s.
+Proof. exact/sumr_ge0. Qed.
+
+Lemma variationN a b f s : variation a b (\- f) s = variation a b f s.
+Proof.
+by rewrite /variation; apply: eq_bigr => k _ /=; rewrite -opprD normrN.
+Qed.
+
+Lemma variation_le a b f g s :
+  variation a b (f \+ g)%R s <= variation a b f s + variation a b g s.
+Proof.
+rewrite [in leRHS]/variation -big_split/=.
+apply: ler_sum => k _; apply: le_trans; last exact: ler_norm_add.
+by rewrite /= addrACA addrA opprD addrA.
+Qed.
+
+Lemma nondecreasing_variation a b f s : {in `[a, b] &, nondecreasing_fun f} ->
+  itv_partition a b s -> variation a b f s = f b - f a.
+Proof.
+move=> ndf abs; rewrite /variation; set F : nat -> R := f \o nth _ (a :: s).
+transitivity (\sum_(0 <= n < size s) (F n.+1 - F n)).
+  rewrite !big_nat; apply: eq_bigr => k; rewrite leq0n/= => ks.
+  by rewrite ger0_norm// subr_ge0; exact: nondecreasing_fun_itv_partition.
+by rewrite telescope_sumr// /F/= (itv_partition_nth_size _ abs).
+Qed.
+
+Lemma nonincreasing_variation a b f s : {in `[a, b] &, nonincreasing_fun f} ->
+  itv_partition a b s -> variation a b f s = f a - f b.
+Proof.
+move=> /nonincreasing_funN ndNf abs; have := nondecreasing_variation ndNf abs.
+by rewrite opprK addrC => <-; rewrite variationN.
+Qed.
+
+Lemma variationD a b c f s t : a <= c -> c <= b ->
+  itv_partition a c s -> itv_partition c b t ->
+  variation a c f s + variation c b f t = variation a b f (s ++ t).
+Proof.
+rewrite le_eqVlt => /predU1P[<-{c} cb|ac].
+  by move=> /itv_partitionxx ->; rewrite variation_nil add0r.
+rewrite le_eqVlt => /predU1P[<-{b}|cb].
+  by move=> ? /itv_partitionxx ->; rewrite variation_nil addr0 cats0.
+move=> acs cbt; rewrite /variation /= [in RHS]/index_iota subn0 size_cat.
+rewrite iotaD add0n big_cat/= -[in X in _ = X + _](subn0 (size s)); congr +%R.
+  rewrite -/(index_iota 0 (size s)) 2!big_nat.
+  apply: eq_bigr => k /[!leq0n] /= ks.
+  rewrite nth_cat ks -cat_cons nth_cat /= ltnS (ltnW ks).
+  by rewrite !(set_nth_default b c)//= ltnS ltnW.
+rewrite -[in RHS](addnK (size s) (size t)).
+rewrite -/(index_iota (size s) (size t + size s)).
+rewrite -{1}[in RHS](add0n (size s)) big_addn addnK 2!big_nat; apply: eq_bigr.
+move=> k /[!leq0n]/= kt.
+rewrite nth_cat {1}(addnC k) -ltn_subRL subnn ltn0 addnK.
+case: k kt => [t0 /=|k kt].
+  rewrite add0n -cat_cons nth_cat/= ltnS leqnn -last_nth.
+  by case: acs => _ /eqP ->.
+rewrite addSnnS (addnC k) -cat_cons nth_cat/= -ltn_subRL subnn ltn0.
+by rewrite -(addnC k) addnK.
+Qed.
+
+(* NB: this is the only lemma that uses variation_zip *)
+Lemma variation_itv_partitionLR a b c f s : a < c -> c < b ->
+  itv_partition a b s ->
+  variation a b f s <= variation a b f (itv_partitionL s c ++ itv_partitionR s c).
+Proof.
+move=> ac bc abs; have [cl|cl] := boolP (c \in s).
+  by rewrite -in_itv_partition//; case: abs => /path_sorted.
+rewrite /itv_partitionL [in leLHS](notin_itv_partition _ cl)//; last first.
+  by apply: path_sorted; case: abs => + _; exact.
+rewrite -notin_itv_partition//; last first.
+  by apply: path_sorted; case: abs => /= + _; exact.
+rewrite !variation_zip//; last first.
+  by apply: itv_partition_cat;
+    [exact: (itv_partitionLP _ bc)|exact: (itv_partitionRP ac)].
+rewrite [in leLHS](notin_itv_partition _ cl); last first.
+  by apply: path_sorted; case: abs => + _; exact.
+set L := [seq x <- s | x < c].
+rewrite -cats1 -catA.
+move: L => L.
+set B := itv_partitionR s c.
+move: B => B.
+elim/last_ind : L => [|L0 L1 _].
+  rewrite !cat0s /=; case: B => [|B0 B1].
+    by rewrite big_nil big_cons/= big_nil addr0.
+  rewrite !big_cons/= addrA lerD// [leRHS]addrC.
+  by rewrite (le_trans _ (ler_normD _ _))// addrA subrK.
+rewrite -cats1.
+rewrite (_ : a :: _ ++ B = (a :: L0) ++ [:: L1] ++ B)//; last first.
+  by rewrite -!catA -cat_cons.
+rewrite zip_cat; last by rewrite cats1 size_rcons.
+rewrite (_ : a :: _ ++ _ ++ B = (a :: L0) ++ [:: L1] ++ [:: c] ++ B); last first.
+  by rewrite -!catA -cat_cons.
+rewrite zip_cat; last by rewrite cats1 size_rcons.
+rewrite !big_cat lerD//.
+case: B => [|B0 B1].
+  by rewrite /= big_nil big_cons big_nil addr0.
+rewrite -cat1s zip_cat// catA.
+rewrite (_ : [:: L1] ++ _ ++ B1 = ([:: L1] ++ [:: c]) ++ [:: B0] ++ B1); last first.
+  by rewrite catA.
+rewrite zip_cat// !big_cat lerD//= !big_cons !big_nil !addr0/= [leRHS]addrC.
+  by rewrite (le_trans _ (ler_normD _ _))// addrA subrK.
+Qed.
+
+Lemma le_variation a b f s x : variation a b f s <= variation a b f (x :: s).
+Proof.
+case: s => [|h t].
+  by rewrite variation_nil /variation/= big_nat_recl//= big_nil addr0.
+rewrite /variation/= !big_nat_recl//= addrA lerD2r.
+by rewrite (le_trans _ (ler_normD _ _))// (addrC (f x - _)) addrA subrK.
+Qed.
+
+Lemma variation_opp_rev a b f s : itv_partition a b s ->
+  variation a b f s =
+  variation (- b) (- a) (f \o -%R) (rev (belast (- a) (map -%R s))).
+Proof.
+move=> abl; rewrite belast_map /variation /= [LHS]big_nat_rev/= add0n.
+rewrite size_rev size_map size_belast 2!big_nat.
+apply: eq_bigr => k; rewrite leq0n /= => ks.
+rewrite nth_rev ?size_map ?size_belast// [in RHS]distrC.
+rewrite (nth_map a); last first.
+  by rewrite size_belast ltn_subLR// addSn ltnS leq_addl.
+rewrite opprK -rev_rcons nth_rev ?size_rcons ?size_map ?size_belast 1?ltnW//.
+rewrite subSn// -map_rcons (nth_map b) ?size_rcons ?size_belast; last first.
+  by rewrite ltnS ltn_subLR// addSn ltnS leq_addl.
+rewrite opprK nth_rcons size_belast -subSn// subSS.
+rewrite (ltn_subLR _ (ltnW ks)) if_same.
+case: k => [|k] in ks *.
+  rewrite add0n ltnn subn1 (_ : nth b s _ = b); last first.
+    case: abl ks => _.
+    elim/last_ind : s => // h t _; rewrite last_rcons => /eqP -> _.
+    by rewrite nth_rcons size_rcons ltnn eqxx.
+  rewrite (_ : nth b (a :: s) _ = nth a (belast a s) (size s).-1)//.
+  case: abl ks => _.
+  elim/last_ind : s => // h t _; rewrite last_rcons => /eqP -> _.
+  rewrite belast_rcons size_rcons/= -rcons_cons nth_rcons/= ltnS leqnn.
+  exact: set_nth_default.
+rewrite addSn ltnS leq_addl//; congr (`| f _ - f _ |).
+  elim/last_ind : s ks {abl} => // h t _; rewrite size_rcons ltnS => kh.
+  rewrite belast_rcons nth_rcons subSS ltn_subLR//.
+  by rewrite addSn ltnS leq_addl// subSn.
+elim/last_ind : s ks {abl} => // h t _; rewrite size_rcons ltnS => kh.
+rewrite belast_rcons subSS -rcons_cons nth_rcons /= ltn_subLR//.
+rewrite addnS ltnS leq_addl; apply: set_nth_default => //.
+by rewrite /= ltnS leq_subLR leq_addl.
+Qed.
+
+Lemma variation_rev_opp a b f s : itv_partition (- b) (- a) s ->
+  variation a b f (rev (belast b (map -%R s))) =
+  variation (- b) (- a) (f \o -%R) s.
+Proof.
+move=> abs; rewrite [in RHS]variation_opp_rev ?opprK//.
+suff: (f \o -%R) \o -%R = f by move=> ->.
+by apply/funext=> ? /=; rewrite opprK.
+Qed.
+
+Lemma variation_subseq a b f (s t : list R) :
+  itv_partition a b s -> itv_partition a b t ->
+  subseq s t ->
+  variation a b f s <= variation a b f t.
+Proof.
+elim: t s a => [? ? ? /= _ /eqP ->//|a s IH [|x t] w].
+  by rewrite variation_nil // variation_ge0.
+move=> /[dup] /itv_partition_cons itvxb /[dup] /itv_partition_le wb itvxt.
+move=> /[dup] /itv_partition_cons itvas itvws /=.
+have ab : a <= b by exact: (itv_partition_le itvas).
+have wa : w < a by case: itvws => /= /andP[].
+have waW : w <= a := ltW wa.
+case: ifPn => [|] nXA.
+  move/eqP : nXA itvxt itvxb => -> itvat itvt /= ta.
+  rewrite -[_ :: t]cat1s -[_ :: s]cat1s.
+  rewrite -?(@variationD _ _ a)//; [|exact: itv_partition1..].
+  by rewrite lerD// IH.
+move=> xts; rewrite -[_ :: s]cat1s -(@variationD _ _ a) => //; last first.
+  exact: itv_partition1.
+have [y [s' s'E]] : exists y s', s = y :: s'.
+  by case: {itvas itvws IH} s xts => // y s' ?; exists y, s'.
+apply: (@le_trans _ _ (variation w b f s)).
+  rewrite IH//.
+  case: itvws => /= /andP[_]; rewrite s'E /= => /andP[ay ys' lyb].
+  by split => //; rewrite (path_lt_head wa)//= ys' andbT.
+by rewrite variationD //; [exact: le_variation | exact: itv_partition1].
+Qed.
+
+End variation.
+
+Section bounded_variation.
+Context {R : realType}.
+Implicit Type (a b : R) (f : R -> R).
+
+Definition variations a b f := [set variation a b f l | l in itv_partition a b].
+
+Lemma variations_variation a b f s : itv_partition a b s ->
+  variations a b f (variation a b f s).
+Proof. by move=> abs; exists s. Qed.
+
+Lemma variations_neq0 a b f : a < b -> variations a b f !=set0.
+Proof.
+move=> ab; exists (variation a b f [:: b]); exists [:: b] => //.
+exact: itv_partition1.
+Qed.
+
+Lemma variationsN a b f : variations a b (\- f) = variations a b f.
+Proof.
+apply/seteqP; split => [_ [s abs] <-|r [s abs]].
+  by rewrite variationN; exact: variations_variation.
+by rewrite -variationN => <-; exact: variations_variation.
+Qed.
+
+Lemma variationsxx a f : variations a a f = [set 0].
+Proof.
+apply/seteqP; split => [x [_ /itv_partitionxx ->]|x ->].
+  by rewrite /variation big_nil => <-.
+by exists [::] => //=; rewrite /variation /= big_nil.
+Qed.
+
+Definition bounded_variation a b f := has_ubound (variations a b f).
+
+Notation BV := bounded_variation.
+
+Lemma bounded_variationxx a f : BV a a f.
+Proof. by exists 0 => r; rewrite variationsxx => ->. Qed.
+
+Lemma bounded_variationD a b f g : a < b ->
+  BV a b f -> BV a b g -> BV a b (f \+ g).
+Proof.
+move=> ab [r abfr] [s abgs]; exists (r + s) => _ [l abl] <-.
+apply: le_trans; first exact: variation_le.
+rewrite lerD//.
+- by apply: abfr; exact: variations_variation.
+- by apply: abgs; exact: variations_variation.
+Qed.
+
+Lemma bounded_variationN a b f : BV a b f -> BV a b (\- f).
+Proof. by rewrite /bounded_variation variationsN. Qed.
+
+Lemma bounded_variationl a c b f : a <= c -> c <= b -> BV a b f -> BV a c f.
+Proof.
+rewrite le_eqVlt => /predU1P[<-{c} ? ?|ac]; first exact: bounded_variationxx.
+rewrite le_eqVlt => /predU1P[<-{b}//|cb].
+move=> [x Hx]; exists x => _ [s acs] <-.
+rewrite (@le_trans _ _ (variation a b f (rcons s b)))//; last first.
+  apply/Hx/variations_variation; case: acs => sa /eqP asc.
+  by rewrite /itv_partition rcons_path last_rcons sa/= asc.
+rewrite {2}/variation size_rcons -[leLHS]addr0 big_nat_recr//= lerD//.
+rewrite /variation !big_nat ler_sum// => k; rewrite leq0n /= => ks.
+rewrite nth_rcons// ks -cats1 -cat_cons nth_cat /= ltnS (ltnW ks).
+by rewrite ![in leRHS](set_nth_default c)//= ltnS ltnW.
+Qed.
+
+Lemma bounded_variationr a c b f : a <= c -> c <= b -> BV a b f -> BV c b f.
+Proof.
+rewrite le_eqVlt => /predU1P[<-{c}//|ac].
+rewrite le_eqVlt => /predU1P[<-{b} ?|cb]; first exact: bounded_variationxx.
+move=> [x Hx]; exists x => _ [s cbs] <-.
+rewrite (@le_trans _ _ (variation a b f (c :: s)))//; last first.
+  apply/Hx/variations_variation; case: cbs => cs csb.
+  by rewrite /itv_partition/= ac/= cs.
+by rewrite {2}/variation/= -[leLHS]add0r big_nat_recl//= lerD.
+Qed.
+
+Lemma variations_opp a b f :
+  variations (- b) (- a) (f \o -%R) = variations a b f.
+Proof.
+rewrite eqEsubset; split=> [_ [s bas <-]| _ [s abs <-]].
+  eexists; last exact: variation_rev_opp.
+  by move/itv_partition_rev : bas; rewrite !opprK.
+eexists; last by exact/esym/variation_opp_rev.
+exact: itv_partition_rev abs.
+Qed.
+
+Lemma nondecreasing_bounded_variation a b f :
+  {in `[a, b] &, {homo f : x y / x <= y}} -> BV a b f.
+Proof.
+move=> incf; exists (f b - f a) => ? [l pabl <-]; rewrite le_eqVlt.
+by rewrite nondecreasing_variation// eqxx.
+Qed.
+
+End bounded_variation.
+
+Section total_variation.
+Context {R : realType}.
+Implicit Types (a b : R) (f : R -> R).
+
+Definition total_variation a b f :=
+  ereal_sup [set x%:E | x in variations a b f].
+
+Notation BV := bounded_variation.
+Notation TV := total_variation.
+
+Lemma total_variationxx a f : TV a a f = 0%E.
+Proof. by rewrite /total_variation variationsxx image_set1 ereal_sup1. Qed.
+
+Lemma total_variation_ge a b f : a <= b -> (`|f b - f a|%:E <= TV a b f)%E.
+Proof.
+rewrite le_eqVlt => /predU1P[<-{b}|ab].
+  by rewrite total_variationxx subrr normr0.
+apply: ereal_sup_ub => /=; exists (variation a b f [:: b]).
+  exact/variations_variation/itv_partition1.
+by rewrite /variation/= big_nat_recr//= big_nil add0r.
+Qed.
+
+Lemma total_variation_ge0 a b f : a <= b -> (0 <= TV a b f)%E.
+Proof. by move=> ab; rewrite (le_trans _ (total_variation_ge _ ab)). Qed.
+
+Lemma bounded_variationP a b f : a <= b -> BV a b f <-> TV a b f \is a fin_num.
+Proof.
+rewrite le_eqVlt => /predU1P[<-{b}|ab].
+  by rewrite total_variationxx; split => // ?; exact: bounded_variationxx.
+rewrite ge0_fin_numE; last exact/total_variation_ge0/ltW.
+split=> [abf|].
+  by rewrite /total_variation ereal_sup_EFin ?ltry//; exact: variations_neq0.
+rewrite /total_variation /bounded_variation ltey => /eqP; apply: contra_notP.
+by move/hasNub_ereal_sup; apply; exact: variations_neq0.
+Qed.
+
+Lemma nondecreasing_total_variation a b f : a <= b ->
+  {in `[a, b] &, nondecreasing_fun f} -> TV a b f = (f b - f a)%:E.
+Proof.
+rewrite le_eqVlt => /predU1P[<-{b} ?|ab ndf].
+  by rewrite total_variationxx subrr.
+rewrite /total_variation [X in ereal_sup X](_ : _ = [set (f b - f a)%:E]).
+  by rewrite ereal_sup1.
+apply/seteqP; split => [x/= [s [t abt <-{s} <-{x}]]|x/= ->{x}].
+  by rewrite nondecreasing_variation.
+exists (variation a b f [:: b]) => //.
+  exact/variations_variation/itv_partition1.
+by rewrite nondecreasing_variation//; exact: itv_partition1.
+Qed.
+
+Lemma total_variationN a b f : TV a b (\- f) = TV a b f.
+Proof. by rewrite /TV; rewrite variationsN. Qed.
+
+Lemma total_variation_le a b f g : a <= b ->
+  (TV a b (f \+ g)%R <= TV a b f + TV a b g)%E.
+Proof.
+rewrite le_eqVlt => /predU1P[<-{b}|ab].
+  by rewrite !total_variationxx adde0.
+have [abf|abf] := pselect (BV a b f); last first.
+  rewrite {2}/total_variation hasNub_ereal_sup//; last first.
+    exact: variations_neq0.
+  rewrite addye ?leey// -ltNye (@lt_le_trans _ _ 0%E)//.
+  exact/total_variation_ge0/ltW.
+have [abg|abg] := pselect (BV a b g); last first.
+  rewrite {3}/total_variation hasNub_ereal_sup//; last first.
+    exact: variations_neq0.
+  rewrite addey ?leey// -ltNye (@lt_le_trans _ _ 0%E)//.
+  exact/total_variation_ge0/ltW.
+move: abf abg => [r abfr] [s abgs].
+have BVabfg : BV a b (f \+ g).
+  by apply: bounded_variationD => //; [exists r|exists s].
+apply: ub_ereal_sup => y /= [r' [s' abs <-{r'} <-{y}]].
+apply: (@le_trans _ _ (variation a b f s' + variation a b g s')%:E).
+  exact: variation_le.
+by rewrite EFinD lee_add// ereal_sup_le//;
+  (eexists; last exact: lexx); (eexists; last reflexivity);
+  exact: variations_variation.
+Qed.
+
+Let total_variationD1 a b c f : a <= c -> c <= b ->
+  (TV a b f >= TV a c f + TV c b f)%E.
+Proof.
+rewrite le_eqVlt=> /predU1P[<-{c}|ac]; first by rewrite total_variationxx add0e.
+rewrite le_eqVlt=> /predU1P[<-{b}|cb]; first by rewrite total_variationxx adde0.
+have [abf|abf] := pselect (BV a b f); last first.
+  rewrite {3}/total_variation hasNub_ereal_sup ?leey//.
+  by apply: variations_neq0 => //; rewrite (lt_trans ac).
+have H s t : itv_partition a c s -> itv_partition c b t ->
+    (TV a b f >= (variation a c f s)%:E + (variation c b f t)%:E)%E.
+  move=> acs cbt; rewrite -EFinD; apply: ereal_sup_le.
+  exists (variation a b f (s ++ t))%:E.
+    eexists; last reflexivity.
+    by exists (s ++ t) => //; exact: itv_partition_cat acs cbt.
+  by rewrite variationD// ltW.
+rewrite [leRHS]ereal_sup_EFin//; last first.
+  by apply: variations_neq0; rewrite (lt_trans ac).
+have acf : BV a c f := bounded_variationl (ltW ac) (ltW cb) abf.
+have cbf : BV c b f := bounded_variationr (ltW ac) (ltW cb) abf.
+rewrite {1 2}/total_variation ereal_sup_EFin//; last exact: variations_neq0.
+rewrite ereal_sup_EFin//; last exact: variations_neq0.
+rewrite -EFinD -sup_sumE; last 2 first.
+  by split => //; exact: variations_neq0.
+  by split => //; exact: variations_neq0.
+apply: le_sup.
+- move=> r/= [s [l' acl' <-{s}]] [t [l cbl] <-{t} <-{r}].
+  exists (variation a b f (l' ++ l)); split; last by rewrite variationD// ltW.
+  exact/variations_variation/(itv_partition_cat acl' cbl).
+- have [r acfr] := variations_neq0 f ac.
+  have [s cbfs] := variations_neq0 f cb.
+  by exists (r + s); exists r => //; exists s.
+- by split => //; apply: variations_neq0; rewrite (lt_trans ac).
+Qed.
+
+Let total_variationD2 a b c f : a <= c -> c <= b ->
+  (TV a b f <= TV a c f + TV c b f)%E.
+Proof.
+rewrite le_eqVlt => /predU1P[<-{c}|ac]; first by rewrite total_variationxx add0e.
+rewrite le_eqVlt => /predU1P[<-{b}|cb]; first by rewrite total_variationxx adde0.
+case : (pselect (bounded_variation a c f)); first last.
+  move=> nbdac; have /eqP -> : TV a c f == +oo%E.
+    have: (-oo < TV a c f)%E by apply: (lt_le_trans _ (total_variation_ge0 f (ltW ac))).
+    by rewrite ltNye_eq => /orP [] => // /bounded_variationP => /(_ (ltW ac)).
+  by rewrite addye ?leey // -ltNye (@lt_le_trans _ _ 0)%E // ?total_variation_ge0 // ltW.
+case : (pselect (bounded_variation c b f)); first last.
+  move=> nbdac; have /eqP -> : TV c b f == +oo%E.
+    have: (-oo < TV c b f)%E.
+      exact: (lt_le_trans _ (total_variation_ge0 f (ltW cb))).
+    by rewrite ltNye_eq => /orP [] => // /bounded_variationP => /(_ (ltW cb)).
+  rewrite addey ?leey // -ltNye (@lt_le_trans _ _ 0%E)//.
+  exact/total_variation_ge0/ltW.
+move=> bdAB bdAC.
+rewrite /total_variation [x in (x + _)%E]ereal_sup_EFin //; last first.
+  exact: variations_neq0.
+rewrite [x in (_ + x)%E]ereal_sup_EFin //; last exact: variations_neq0.
+rewrite -EFinD -sup_sumE /has_sup; [|(by split => //; exact: variations_neq0)..].
+apply: ub_ereal_sup => ? [? [l pacl <- <-]]; rewrite lee_fin.
+apply: (le_trans (variation_itv_partitionLR _ ac _ _)) => //.
+apply: sup_ub => /=.
+  case: bdAB => M ubdM; case: bdAC => N ubdN; exists (N + M).
+  move=> q [?] [i pabi <-] [? [j pbcj <-]] <-.
+  by apply: lerD; [apply: ubdN;exists i|apply:ubdM;exists j].
+exists (variation a c f (itv_partitionL l c)).
+  by apply: variations_variation; exact: itv_partitionLP pacl.
+exists (variation c b f (itv_partitionR l c)).
+  by apply: variations_variation; exact: itv_partitionRP pacl.
+by rewrite variationD// ?ltW//;
+  [exact: itv_partitionLP pacl|exact: itv_partitionRP pacl].
+Qed.
+
+Lemma total_variationD a b c f : a <= c -> c <= b ->
+  (TV a b f = TV a c f + TV c b f)%E.
+Proof.
+by move=> ac cb; apply/eqP; rewrite eq_le; apply/andP; split;
+  [exact: total_variationD2|exact: total_variationD1].
+Qed.
+
+End total_variation.
+
+Section variation_continuity.
+Context {R : realType}.
+Implicit Type f : R -> R.
+
+Notation BV := bounded_variation.
+Notation TV := total_variation.
+
+Definition neg_tv a f (x : R) : \bar R := ((TV a x f - (f x)%:E) * 2^-1%:E)%E.
+
+Definition pos_tv a f (x : R) : \bar R := neg_tv a (\- f) x.
+
+Lemma neg_tv_nondecreasing a b f :
+  {in `[a, b] &, nondecreasing_fun (neg_tv a f)}.
+Proof.
+move=> x y xab yab xy; have ax : a <= x.
+  by move: xab; rewrite in_itv //= => /andP [].
+rewrite /neg_tv lee_pmul2r // lee_subr_addl // addeCA -EFinB.
+rewrite [TV a y _](total_variationD _ ax xy) //.
+apply: lee_add => //; apply: le_trans; last exact: total_variation_ge.
+by rewrite lee_fin ler_norm.
+Qed.
+
+Lemma bounded_variation_pos_neg_tvE a b f : BV a b f ->
+  {in `[a, b], f =1 (fine \o pos_tv a f) \- (fine \o neg_tv a f)}.
+Proof.
+move=> bdabf x; rewrite in_itv /= => /andP [ax xb].
+have ffin: TV a x f \is a fin_num.
+   apply/bounded_variationP => //.
+   exact: (bounded_variationl _ xb).
+have Nffin : TV a x (\- f) \is a fin_num.
+  apply/bounded_variationP => //; apply/bounded_variationN.
+  exact: (bounded_variationl ax xb).
+rewrite /pos_tv /neg_tv /= total_variationN -fineB -?muleBl // ?fineM //.
+- rewrite addeAC oppeD //= ?fin_num_adde_defl //.
+  by rewrite addeA subee // add0e -EFinD //= opprK mulrDl -Num.Theory.splitr.
+- by rewrite fin_numB ?fin_numD ?ffin; apply/andP; split.
+- by apply: fin_num_adde_defl; rewrite fin_numN fin_numD; apply/andP; split.
+- by rewrite fin_numM // fin_numD; apply/andP; split.
+- by rewrite fin_numM // fin_numD; apply/andP; split.
+Qed.
+
+Lemma fine_neg_tv_nondecreasing a b f : BV a b f ->
+  {in `[a, b] &, nondecreasing_fun (fine \o neg_tv a f)}.
+Proof.
+move=> bdv p q pab qab pq /=.
+move: (pab) (qab); rewrite ?in_itv /= => /andP[ap pb] /andP[aq qb].
+apply: fine_le; rewrite /neg_tv ?fin_numM // ?fin_numB /=.
+- apply/andP; split => //; apply/bounded_variationP => //.
+  exact: (bounded_variationl _ pb).
+- apply/andP; split => //; apply/bounded_variationP => //.
+  exact: (bounded_variationl _ qb).
+exact: (neg_tv_nondecreasing _ pab).
+Qed.
+
+Lemma neg_tv_bounded_variation a b f : BV a b f -> BV a b (fine \o neg_tv a f).
+Proof.
+move=> ?; apply: nondecreasing_bounded_variation.
+exact: fine_neg_tv_nondecreasing.
+Qed.
+
+Lemma total_variation_right_continuous a b x f : a <= x -> x < b ->
+  f @ x^'+ --> f x ->
+  BV a b f ->
+  fine \o TV a ^~ f @ x^'+ --> fine (TV a x f).
+Proof.
+move=> ax xb ctsf bvf; have ? : a <= b by apply:ltW; apply: (le_lt_trans ax).
+apply/cvgrPdist_lt=> _/posnumP[eps].
+have ? : Filter (nbhs x^'+) by exact: at_right_proper_filter.
+have xbl := ltW xb.
+have xbfin : TV x b f \is a fin_num.
+  by apply/bounded_variationP => //; exact: (bounded_variationr _ _ bvf).
+have [//|?] := @ub_ereal_sup_adherent R _ (eps%:num / 2) _ xbfin.
+case=> ? [l + <- <-]; rewrite -/(total_variation x b f).
+move: l => [|i j].
+  by move=> /itv_partition_nil /eqP; rewrite lt_eqF.
+move=> [/= /andP[xi ij /eqP ijb]] tv_eps.
+apply: filter_app (nbhs_right_ge _).
+apply: filter_app (nbhs_right_lt xi).
+have e20 : 0 < eps%:num / 2 by [].
+move/cvgrPdist_lt/(_ (eps%:num/2) e20) : ctsf; apply: filter_app.
+near=> t => fxt ti xt; have ta : a <= t by exact: (le_trans ax).
+have tb : t <= b by rewrite (le_trans (ltW ti))// -ijb path_lt_le_last.
+rewrite -fineB; last 2 first.
+  by apply/bounded_variationP => //; exact: bounded_variationl bvf.
+  by apply/bounded_variationP => //; exact: bounded_variationl bvf.
+rewrite (total_variationD _ ax xt).
+have tbfin : TV t b f \is a fin_num.
+  by apply/bounded_variationP => //; exact: (@bounded_variationr _ a).
+have xtfin : TV x t f \is a fin_num.
+  apply/bounded_variationP => //; apply: (@bounded_variationl _ _ _ b) => //.
+  exact: (@bounded_variationr _ a).
+rewrite oppeD ?fin_num_adde_defl// addeA subee //; first last.
+  by apply/bounded_variationP => //; exact: (@bounded_variationl _ _ _ b).
+rewrite sub0e fineN normrN ger0_norm; last first.
+  by rewrite fine_ge0// total_variation_ge0.
+move: (tv_eps); rewrite (total_variationD f _ tb) //.
+move: xt; rewrite le_eqVlt => /predU1P[->|xt].
+  by rewrite total_variationxx/=.
+have : variation x b f (i :: j) <= variation x t f (t :: nil) +
+                                   variation t b f (i :: j).
+  rewrite variationD//; last 2 first.
+    exact: itv_partition1.
+    by rewrite /itv_partition/= ti ij ijb.
+  exact: le_variation.
+rewrite -lee_fin => /lt_le_trans /[apply].
+rewrite {1}variation_prev; last exact: itv_partition1.
+rewrite /= -addeA -lte_subr_addr; last by rewrite fin_numD; apply/andP.
+rewrite EFinD -lte_fin ?fineK // oppeD //= ?fin_num_adde_defl // opprK addeA.
+move/lt_trans; apply.
+rewrite [x in (_ < x%:E)%E]Num.Theory.splitr EFinD addeC lte_add2lE //.
+rewrite -addeA.
+apply: (@le_lt_trans _ _ (variation x t f (t :: nil))%:E).
+  rewrite [in leRHS]variation_prev; last exact: itv_partition1.
+  rewrite gee_addl // sube_le0; apply: ereal_sup_ub => /=.
+  exists (variation t b f (i :: j)) => //; apply: variations_variation.
+  by rewrite /itv_partition/= ijb ij ti.
+by rewrite /variation/= big_nat_recr//= big_nil add0r distrC lte_fin.
+Unshelve. all: by end_near. Qed.
+
+Lemma neg_tv_right_continuous a x b f : a <= x -> x < b ->
+  BV a b f ->
+  f @ x^'+ --> f x ->
+  fine \o neg_tv a f @ x^'+ --> fine (neg_tv a f x).
+Proof.
+move=> ax ? bvf fcts; have xb : x <= b by exact: ltW.
+have xbfin : TV a x f \is a fin_num.
+  by apply/bounded_variationP => //; exact: bounded_variationl bvf.
+apply: fine_cvg; rewrite /neg_tv fineM // ?fin_numB ?xbfin //= EFinM.
+under eq_fun => i do rewrite EFinN.
+apply: (@cvg_trans _ (((TV a n f - (f n)%:E) * 2^-1%:E)%E @[n --> x^'+])).
+  exact: cvg_id.
+apply: cvgeMr; first by [].
+rewrite fineD; [|by []..].
+rewrite EFinB; apply: cvgeB; [by []| |].
+  apply/ fine_cvgP; split; first exists (b - x).
+  - by rewrite /= subr_gt0.
+  - move=> t /= xtbx xt; have ? : a <= t.
+      by apply: ltW; apply: (le_lt_trans ax).
+    apply/bounded_variationP => //.
+    apply: bounded_variationl bvf => //.
+    move: xtbx; rewrite distrC ger0_norm ?subr_ge0; last by exact: ltW.
+    by rewrite ltrBrDr -addrA [-_ + _]addrC subrr addr0 => /ltW.
+  by apply: total_variation_right_continuous => //; last exact: bvf.
+apply: cvg_comp; first exact: fcts.
+apply/ fine_cvgP; split; first by near=> t => //.
+by have -> : fine \o EFin = id by move=> ?; rewrite funeqE => ? /=.
+Unshelve. all: by end_near. Qed.
+
+Lemma total_variation_opp a b f : TV a b f = TV (- b) (- a) (f \o -%R).
+Proof. by rewrite /total_variation variations_opp. Qed.
+
+Lemma total_variation_left_continuous a b x f : a < x -> x <= b ->
+  f @ x^'- --> f x ->
+  BV a b f ->
+  fine \o TV a ^~ f @ x^'- --> fine (TV a x f).
+Proof.
+move=> ax xb fNcts bvf.
+apply/cvg_at_leftNP; rewrite total_variation_opp.
+have bvNf : BV (-b) (-a) (f \o -%R).
+  by case: bvf => M; rewrite -variations_opp => ?; exists M.
+have bx : - b <= - x by rewrite lerNl opprK.
+have xa : - x < - a by rewrite ltrNl opprK.
+have ? : - x <= - a by exact: ltW.
+have ? : Filter (nbhs (-x)^'+) by exact: at_right_proper_filter.
+have -> : fine (TV (-x) (-a) (f \o -%R)) =
+    fine (TV (-b) (-a) (f \o -%R)) - fine (TV (-b) (-x) (f \o -%R)).
+  apply/eqP; rewrite -subr_eq opprK addrC.
+  rewrite -fineD; last 2 first.
+    by apply/bounded_variationP => //; exact: bounded_variationl bvNf.
+    by apply/bounded_variationP => //; exact: bounded_variationr bvNf.
+  by rewrite -total_variationD.
+have /near_eq_cvg/cvg_trans : {near (- x)^'+,
+    (fun t => fine (TV (- b) (- a) (f \o -%R)) - fine (TV (- b) t (f \o -%R))) =1
+    (fine \o (TV a)^~ f) \o -%R}.
+  apply: filter_app (nbhs_right_lt xa).
+  apply: filter_app (nbhs_right_ge _).
+  near=> t => xt ta; have ? : -b <= t by exact: (le_trans bx).
+  have ? : t <= -a by exact: ltW.
+  apply/eqP; rewrite eq_sym -subr_eq opprK addrC.
+  rewrite /= [TV a _ f]total_variation_opp opprK -fineD; last first.
+    by apply/bounded_variationP => //; apply: bounded_variationr bvNf.
+    by apply/bounded_variationP => //; apply: bounded_variationl bvNf.
+  by rewrite -total_variationD.
+apply.
+apply: cvgB; first exact: cvg_cst.
+apply: (total_variation_right_continuous _ _ _ bvNf).
+- by rewrite ler_oppl opprK //.
+- by rewrite ltr_oppl opprK //.
+by apply/cvg_at_leftNP; rewrite /= opprK.
+Unshelve. all: by end_near. Qed.
+
+Lemma total_variation_continuous a b (f : R -> R) : a < b ->
+  {within `[a,b], continuous f} ->
+  BV a b f ->
+  {within `[a,b], continuous (fine \o TV a ^~ f)}.
+Proof.
+move=> ab /(@continuous_within_itvP _ _ _ _ ab) [int [l r]] bdf.
+apply/continuous_within_itvP; (repeat split) => //.
+- move=> x /[dup] xab; rewrite in_itv /= => /andP [ax xb].
+  apply/left_right_continuousP; split.
+    apply: (total_variation_left_continuous _ (ltW xb)) => //.
+    by have /left_right_continuousP [] := int x xab.
+  apply: (total_variation_right_continuous _ xb) => //; first exact: ltW.
+  by have /left_right_continuousP [] := int x xab.
+- exact: (total_variation_right_continuous _ ab).
+- exact: (total_variation_left_continuous ab).
+Qed.
+
+End variation_continuity.