minor checks (wip)

CHANGELOG_UNRELEASED.md

@@ -16,35 +16,45 @@
 - in file `normedtype.v`,
   + new lemma `continuous_within_itvP`.
 
+- in `ereal.v`:
+  + lemma `ereal_supy`
+
 - 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`, `has_ubound_ereal_sup`, `sup_le`, `ereal_supy`, 
-    `path_lt_filter0`, `path_lt_filterT`, `last_filter_lt`, `last_filter`, 
-    `path_inv`, `path_lt_le_last`, `itv_partition_nil`, `itv_partition1`, 
-    `itv_partition_cons`, `itv_partitionxx`, `itv_partition_le`, 
-    `itv_partition_tail`, `itv_partition_cat`, `itv_partition_nth_size`, 
+  + new lemmas `left_right_continuousP`,
+    `nondecreasing_funN`, `nonincreasing_funN`, `last_filterP`,
+    `path_lt_filter0`, `path_lt_filterT`, `path_lt_head`, `path_lt_last_filter`,
+	`path_lt_le_last`
+
+  + 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`, `variationE`, `variation_nil`, 
+    `notin_itv_partition`, `itv_partition_rev`,
+
+  + new lemmas `variationE`, `variation_nil`,
     `variation_ge0`, `variationN`, `variation_le`, `nondecreasing_variation`, 
     `nonincreasing_variation`, `variationD`, `variation_itv_partitionLR`, 
-    `le_variation`, `variation_opp_rev`, `variation_rev_opp`, 
-    `variations_variation`, `variations_neq0`, `variationsN`, `variationsxx`, 
-    `bounded_variationxx`, `bounded_variationD`, `bounded_variationN`, 
+    `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`, `total_variationxx`, 
-    `total_variation_ge`, `total_variation_ge0`, 
-    `nondecreasing_total_variation`, `bounded_variationP`, `total_variationN`, 
-    `total_variation_le`, `total_variationD`, `neg_TV_increasing`, 
-    `total_variation_jordan_decompE`, `neg_TV_increasing_fin`, 
-    `neg_TV_bounded_variation`, `TV_right_continuous`, 
-    `neg_TV_right_continuous`, `total_variation_opp`, `TV_left_continuous`, and 
-    `TV_continuous`.
+    `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_jordan_decompE`, `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
 

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

@@ -2919,47 +2919,44 @@ Lemma continuous_within_itvP {R : realType } a b (f : R -> R) :
   {within `[a,b], continuous f} <->
   {in `]a,b[, continuous f} /\ f @ a^'+ --> f a /\ f @b^'- --> f b.
 Proof.
-move=> ab; split.
-have [aab bab] : a \in `[a, b] /\ b \in `[a, b].
-  by split; apply/andP; split => //; apply: ltW.
-have [aabC babC] : `[a, b]%classic a /\ `[a, b]%classic b.
-  by rewrite ?inE /=; split.
-move=> abf; split.
-  suff : {in `]a,b[%classic, continuous f}.
-      by move=> P ? W; by apply: P; move: W; rewrite inE /=.
-    rewrite -(@continuous_open_subspace); last exact: interval_open.
-    by move: abf; apply: continuous_subspaceW; apply: subset_itvW.
-  split; apply/cvgrPdist_lt => eps eps_gt0 /=;
-    [move/continuous_withinNx/cvgrPdist_lt/(_ _ eps_gt0) : (abf a)
-    | move/continuous_withinNx/cvgrPdist_lt/(_ _ eps_gt0) : (abf b)];
-    rewrite /dnbhs /= ?near_withinE ?near_simpl /prop_near1/nbhs /=;
-    rewrite -nbhs_subspace_in // /within /= ?nbhs_simpl near_simpl;
-    apply: filter_app; exists (b-a); rewrite /= ?subr_gt0 // => c cba + ac;
-    (apply => //; last by apply/eqP => CA; move: ac; rewrite CA ltxx);
-    apply/andP; split; apply: ltW => //; move: cba; rewrite /= ?[(`|a-c|)]distrC ger0_norm. 
-  - by rewrite ltrBlDr -addrA [-_+_]addrC subrr addr0.
-  - by apply: ltW; rewrite subr_gt0.
-  - by rewrite ltrBlDr addrC addrA ltrBrDl -ltrBrDr -addrA subrr addr0. 
-  - by apply: ltW; rewrite subr_gt0.
-case=> ctsoo [ctsL ctsR]; apply/subspace_continuousP => x /andP [].
-rewrite ?le_eqVlt => /orP + /orP; case => + []. 
-- by move=> /eqP [<-] /eqP [E]; move: ab; rewrite E ltxx.
-- move=> /eqP [<-_]; 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 []); rewrite le_eqVlt => /orP [].
-    by move=> /eqP ->; rewrite subrr normr0.
-  by move=> ?; apply.
-- move=> _ /eqP [->]; 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 []); rewrite le_eqVlt => /orP [].
-    by move=> /eqP ->; rewrite subrr normr0.
-  by move=> ?; apply.
-- move=> ax xb; have aboox : x \in `]a,b[ by apply/andP; split.
+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 apply.
-  rewrite -open_subsetE; [exact: subset_itvW| exact: interval_open].
+  suff : `]a, b[ `<=` interior `[a, b] by exact.
+  by rewrite -open_subsetE; [exact: subset_itvW| exact: interval_open].
 Qed.
 
 (* TODO: generalize to R : numFieldType *)