Total variation (math-comp#1118)

* total variation proofs

- increasing implies BV
- splitting partitions
- right/left continuity of TV
- define variation with path
- adding monotone variation
- variation using prev and next

---------

Co-authored-by: Reynald Affeldt <[email protected]>

CHANGELOG_UNRELEASED.md

@@ -59,6 +59,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
 

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.

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.
 

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.