Simplify proof of countable_discontinuity

CHANGELOG_UNRELEASED.md

@@ -10,6 +10,8 @@
     `pownMexpr_cvgn0`
   + instance `is_derive1_powRl`
 
+- in `realfun.v`:
+  + lemma `nondecreasing_discontinuity`.
 ### Changed
 
 - in `lebesgue_integral_nonneg.v`, generalized and deprecated:
@@ -39,6 +41,9 @@
 
 ### Removed
 
+- in `realfun.v`:
+  + lemma `nondecreasing_fun_sum_le`.
+
 ### Infrastructure
 
 ### Misc

theories/realfun.v

@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import boot order finmap ssralg ssrnum ssrint.
-From mathcomp Require Import archimedean interval interval_inference.
+From mathcomp Require Import rat archimedean interval interval_inference.
 #[warning="-warn-library-file-internal-analysis"]
 From mathcomp Require Import unstable.
 From mathcomp Require Import boolp classical_sets functions cardinality contra.
@@ -2354,266 +2354,51 @@ Hypothesis ndF : {in `[a, b] &, nondecreasing_fun F}.
 Let Fr z := lim (F x @[x --> z^'+]).
 Let Fl z := lim (F x @[x --> z^'-]).
 
-Lemma nondecreasing_fun_sum_le (s : seq R) :
-  itv_partition a b s ->
-  \sum_(1 <= i < size s) (Fr (nth b (a :: s) i) - Fl (nth b (a :: s) i))
-  <= F b - F a.
-Proof.
-move=> abs; have [s0|s0] := eqVneq s [::].
-  by move: abs; rewrite s0/= big_nil => /itv_partition_nil ->; rewrite subrr.
-have [s' ss'b] : exists s', s = rcons s' b.
-  move: s abs s0; apply: last_ind => // s x ih [_ +] sx0.
-  by move/eqP; rewrite last_rcons => <-; exists s.
-pose x_ : R^nat := nth b (a :: s).
-set t := map (fun n => (x_ n + x_ n.+1) / 2) (iota 0%N (size s)).
-have [path_at sizets asts] : [/\ path <%R a t, size t = size s &
-    (forall k, (k < size s)%N -> nth b (a :: s) k < nth b t k < nth b s k)].
-  split.
-  - apply/(pathP b) => -[|n].
-    + rewrite [in X in X -> _]size_map [in X in X -> _]size_iota => {}s0/=.
-      rewrite /t ss'b size_rcons/= midf_lt// -[a]/(nth b (a :: s) 0%N).
-      by have /pathP := abs.1; exact.
-    + rewrite [in X in X -> _]size_map [in X in X -> _]size_iota => ns/=.
-      rewrite !(nth_map 0%N) ?size_iota//; first exact: (leq_trans _ ns).
-      rewrite !nth_iota// ?add0n; first exact: (leq_trans _ ns).
-      rewrite (@lt_trans _ _ (x_ n.+1))// midf_lt//.
-        by have /pathP := abs.1; apply; exact: (leq_trans _ ns).
-      by have /pathP := abs.1; exact.
-  - by rewrite size_map size_iota.
-  - move=> k ks; apply/andP; split.
-      rewrite (nth_map 0%N) ?size_iota// nth_iota// add0n midf_lt//.
-      by have /pathP := abs.1; exact.
-    rewrite (nth_map 0%N _ (fun n => (x_ n + x_ n.+1) / 2)) ?size_iota//.
-    rewrite nth_iota// add0n midf_lt//.
-    by have /pathP := abs.1; exact.
-pose y_ : R^nat := nth b (a :: t).
-have ast k : (k < size s)%N -> nth b (a :: s) k < nth b t k.
-  by move=> /asts /andP[].
-have ts k : (k < size s)%N -> nth b t k < nth b s k by move=> /asts /andP[].
-have yxl i : (0 < i)%N -> (i < size (a :: s))%N -> F (y_ i) <= Fl (x_ i).
-  move=> i0 ias; apply: limr_ge.
-  - have near_subab : \forall x \near (x_ i)^'-, `]x, (x_ i)[ `<=` `[a, b].
-      near=> x; apply: subset_itvW; last exact: itv_partition_nth_le.
-      near: x; apply: nbhs_left_ge.
-      rewrite -[a]/(x_ 0%N).
-      move: abs.1.
-      by rewrite lt_path_pairwise => /pairwiseP; exact.
-    apply: nondecreasing_at_left_is_cvgr.
-      by near do apply: itv_sub_in2 ndF.
-    near=> x.
-    exists (F b) => _ /= [z zxxi <-].
-    apply: ndF.
-    + by move: z zxxi; near: x.
-    + by rewrite in_itv/= lexx andbT (itv_partition_le abs).
-    + move: zxxi; rewrite in_itv/= => /andP [_ /ltW] /le_trans; apply.
-      exact: itv_partition_nth_le.
-  - near=> x; apply: ndF.
-    + rewrite in_itv/=; apply/andP; split.
-        apply/ltW.
-        have /allP := lt_path_min path_at; apply.
-        by rewrite /y_ /= -(prednK i0)/= mem_nth// prednK// sizets.
-      apply: (@le_trans _ _ (x_ i)); last exact: itv_partition_nth_le.
-      by rewrite ltW// -(prednK i0)/= ts// prednK.
-    + rewrite in_itv/=; apply/andP; split.
-      * near: x; apply: nbhs_left_ge.
-        have /allP := lt_path_min abs.1; apply.
-        by rewrite /x_ -(prednK i0)/= mem_nth// prednK.
-      * by rewrite (@le_trans _ _ (x_ i))//; exact: itv_partition_nth_le.
-    + near: x; apply: nbhs_left_ge.
-      by rewrite -(prednK i0)/= ts// prednK.
-have xry i : (0 < i)%N -> (i < size s)%N -> Fr (x_ i) <= F (y_ i.+1).
-  move=> i0 ilts; apply: limr_le.
-  - apply: nondecreasing_at_right_is_cvgr.
-    + near=> x; apply: (@itv_sub_in2 _ _ _ `[a, b]) ndF.
-      apply: subset_itvW.
-        by apply: itv_partition_nth_ge (abs); rewrite ltnS ltnW.
-      near: x; apply: nbhs_right_le.
-      apply: (@lt_le_trans _ _ (y_ i.+1)); first exact: ast.
-      apply: (@le_trans _ _ (x_ i.+1)); first exact/ltW/ts.
-      exact: itv_partition_nth_le.
-    + near=> x.
-      exists (F (x_ i)) => _/= [z + <-] => /[!in_itv]/= /andP[xiz zx].
-      apply: ndF; last exact: ltW.
-      * rewrite in_itv/=; apply/andP; split.
-          by apply: itv_partition_nth_ge (abs); exact: (ltn_trans ilts).
-        by apply: itv_partition_nth_le (abs); exact: (ltn_trans ilts).
-      * rewrite in_itv/=; apply/andP; split.
-          apply: le_trans (ltW xiz).
-          apply: itv_partition_nth_ge (abs).
-          exact: (ltn_trans ilts).
-        apply: (le_trans (ltW zx)).
-        apply: (@le_trans _ _ (x_ i.+1)) => //.
-          near: x; apply: nbhs_right_le.
-          by have /pathP := abs.1; exact.
-        by apply: itv_partition_nth_le (abs); exact: ilts.
-  - near=> x; apply: ndF.
-    + rewrite in_itv/=; apply/andP; split.
-        apply: (@le_trans _ _ (x_ i)) => //.
-        by apply: itv_partition_nth_ge (abs); exact: (@leq_trans (size s)).
-      near: x; apply: nbhs_right_le.
-      apply: (@lt_le_trans _ _ (x_ i.+1)); last exact: itv_partition_nth_le.
-      by have /pathP := abs.1; exact.
-    + rewrite in_itv/=; apply/andP; split.
-        rewrite ltW//.
-        have /allP := lt_path_min path_at; apply.
-        by apply: mem_nth; rewrite sizets.
-      apply: (@le_trans _ _ (x_ i.+1)); first exact/ltW/ts.
-      exact: itv_partition_nth_le.
-  - by near: x; apply: nbhs_right_le; exact: ast.
-apply: (@le_trans _ _ (\sum_(1 <= i < size s) (F (y_ i.+1) - F (y_ i)))).
-  rewrite big_nat_cond [leRHS]big_nat_cond; apply: ler_sum => n.
-  rewrite andbT => /andP[n0 ns].
-  by apply: lerB; [exact: xry|rewrite yxl//= ltnS ltnW].
-have sizes0 : (0 < size s)%N.
-  by rewrite lt0n; apply: contra s0 => /eqP/size0nil ->.
-rewrite telescope_sumr// lerB//.
-- apply: ndF.
-  + rewrite in_itv/=; apply/andP; split.
-    * rewrite ltW//.
-      have /allP := lt_path_min path_at; apply.
-      rewrite -sizets /y_ -last_nth//.
-      have [ht [r ->]] : exists x t', t = rcons x t'.
-        move: t path_at sizets asts y_ ast ts yxl xry.
-        apply: last_ind => //.
-          by move=> _ /esym /= /size0nil; move/eqP : s0.
-        by move=> ht tt _ _ _ _ _ _ _ _ _; exists ht, tt.
-      by rewrite mem_rcons last_rcons mem_head.
-    * rewrite /y_ /t.
-      have /pathP := abs.1 => /(_ b).
-      move: (sizes0) => /prednK.
-      set m := (size s).-1 => <- H.
-      rewrite -[leLHS]/(nth b [seq ((x_ i + x_ i.+1) / 2) | i <- iota 0 m.+1] m).
-      rewrite (nth_map 0%N); first by rewrite size_iota.
-      rewrite nth_iota// add0n.
-      apply: (@le_trans _ _ (x_ m.+1)).
-        by rewrite midf_le// ltW// H.
-      by apply: itv_partition_nth_le abs; rewrite prednK.
-  + by rewrite in_itv/= lexx andbT; exact: itv_partition_le abs.
-  + have /eqP := abs.2.
-    rewrite (last_nth b) => <-.
-    rewrite /y_ /t.
-    move: (sizes0) => /prednK <-.
-    set m := (size s).-1.
-    rewrite -[leLHS]/(nth b [seq ((x_ i + x_ i.+1) / 2) | i <- iota 0 m.+1] m).
-    rewrite (nth_map 0%N); first by rewrite size_iota.
-    rewrite nth_iota// add0n midf_le// ltW//.
-    have /pathP := abs.1; apply.
-    by rewrite (prednK sizes0).
-have ay1 : a <= y_ 1%N by rewrite -[a]/(nth b (a :: s) 0%N) ltW// ast.
-apply: ndF => //.
-  by rewrite in_itv/= lexx andTb; exact: itv_partition_le abs.
-rewrite in_itv/=; apply/andP; split => //.
-apply: (@le_trans _ _ (x_ 1%N)); last exact: itv_partition_nth_le.
-by rewrite /y_/x_ ltW//= ts.
-Unshelve. all: end_near. Qed.
+Lemma nondecreasing_discontinuity x : 
+  x \in `]a, b[ -> discontinuity F x -> Fl x < Fr x.
+Proof.
+move=> xab [cvgl cvgr].
+rewrite /Fl /Fr lt_neqAle => -> /=.
+exact: (nondecreasing_at_left_at_right ndF xab).
+Qed.
 
 Lemma discontinuity_countable :
   countable [set x | x \in (`]a, b[) /\ discontinuity F x].
 Proof.
-have [|ab] := leP b a.
-  rewrite le_eqVlt => /predU1P[->|ba].
-    set S := (X in countable X).
-    suff Sa : S `<=` [set a] by exact/finite_set_countable/(sub_finite_set Sa).
-    move=> x; rewrite /S/= in_itv/= => [[/andP[/ltW]]].
-    by rewrite ltNge => ->.
-  set S := (X in countable X).
-  rewrite (_ : S = set0)// -subset0 => x.
-  rewrite /S/= in_itv/= => -[/andP[]] /lt_trans /[apply].
-  by rewrite ltNge ltW.
-set A : set R := [set x | _].
-pose elt_type := set_type A.
-have FrBFl (x : elt_type) : exists m, m.+1%:R ^-1 < Fr (sval x) - Fl (sval x).
-  have [Fc Fd cd] : discontinuity F (sval x) by case: x => /= r /[!inE] => -[].
-  have FlFr : Fl (sval x) <= Fr (sval x).
-    apply: (@nondecreasing_at_left_at_right _ _ a b) => //.
-    by case: x {Fc Fd cd} => x/= /[1!inE] -[].
-  have {}FlFr : Fl (sval x) < Fr (sval x) by rewrite lt_neqAle FlFr andbT.
-  exists (truncn (Fr (sval x) - Fl (sval x))^-1).
-  by rewrite invf_plt ?posrE ?subr_gt0// truncnS_gt.
-pose S m := [set x | x \in (`]a, b[) /\ m.+1%:R ^-1 < Fr x - Fl x].
-have jumpfafb m (s : seq R) : (forall i, (i < size s)%N -> nth b s i \in S m) ->
-  path <%R a s ->
-    \sum_(0 <= i < size s) (Fr (nth b s i) - Fl (nth b s i)) <= F b - F a.
-  move=> Hs pas.
-  have : itv_partition a b (rcons s b).
-    split; last by rewrite last_rcons.
-    move: s Hs pas; apply: last_ind => /=; first by rewrite ab.
-    move=> s ls _ H.
-    rewrite rcons_path => /andP[pas lasls].
-    rewrite !rcons_path pas lasls/= last_rcons.
-    have := nth_rcons b s ls (size s).
-    rewrite ltnn eq_refl => <-.
-    have := H (size s).
-    rewrite size_rcons => /(_ (ltnSn (size s))).
-    by rewrite inE => -[+ _] => /[!in_itv]/= /andP[].
-  move/nondecreasing_fun_sum_le.
-  rewrite size_rcons (big_addn 0%N _ 1%N) subn1/= big_nat/=.
-  under eq_bigr.
-    move=> i si.
-    rewrite addn1/= nth_rcons si.
-    over.
-  by rewrite -big_nat.
-have fin_S m : finite_set (S m).
-  apply: contrapT => /infinite_set_fset.
-  move=> /(_ (m.+1 * (truncn (F b - F a)).+1).+1)[B BSm mFbFaB].
-  set s := sort <=%R B.
-  have := jumpfafb m s.
-  have HsSm n : (n < size s)%N -> nth b s n \in S m.
-    move=> ns; apply/mem_set/BSm/set_mem.
-    by rewrite mem_setE -(@mem_sort _ <=%R) mem_nth.
-  move/(_ HsSm){HsSm}.
-  have Hpas : path <%R a s.
-    rewrite lt_path_sortedE; apply/andP; split.
-      apply/allP => x.
-      rewrite mem_sort => /BSm[+ _].
-      by rewrite in_itv/= => /andP[].
-    by rewrite sort_lt_sorted; exact: fset_uniq.
-  move/(_ Hpas){Hpas}.
-  contra; rewrite -ltNge => _.
-  rewrite (lt_le_trans (truncnS_gt _))//.
-  apply: (@le_trans _ _ (m.+1%:R^-1 * #|` B|%:R)).
-    by rewrite ler_pdivlMl// -natrM ler_nat ltnW.
-  rewrite card_fset_sum1 natr_sum mulr_sumr mulr1 big_tnth cardfE.
-  rewrite -(big_mkord xpredT (fun=> m.+1%:R^-1)) size_sort cardfE.
-  rewrite ler_sum_nat// => k /[!leq0n]/= kB.
-  have : nth b s k \in S m.
-    apply/mem_set/BSm => /=; rewrite -(@mem_sort _ <=%R).
-    by apply/mem_nth; rewrite size_sort cardfE.
-  by rewrite /S inE/= => -[_ /ltW].
-suff -> : A = \bigcup_m S m.
-  by apply: bigcup_countable => // n _; exact: finite_set_countable.
-rewrite eqEsubset; split.
-- move=> x Ax.
-  pose z : elt_type := exist (fun x => x \in A) x (mem_set Ax).
-  have [m Hz] := FrBFl z.
-  exists m => //.
-  by split; [move: (Ax) => -[]|exact: Hz].
-- move=> x [m _ []] /[dup] xab /[!in_itv]/= /andP[ax xb] mx.
-  split => //; split.
-  + apply: nondecreasing_at_left_is_cvgr; near=> r.
-    * apply: itv_sub_in2 ndF.
-      apply: (subset_itvW _ _ _ (ltW xb)).
-      by near: r; exact: nbhs_left_ge.
-    * exists (F x) => _/= [z zrx <-].
-      apply: ndF.
-      - apply: (subset_itvW _ _ _ (ltW xb) zrx).
-        by near: r; exact: nbhs_left_ge.
-      - exact: subset_itv_oo_cc.
-      - by move: zrx => /[!in_itv]/= /andP[_ /ltW].
-  + apply: nondecreasing_at_right_is_cvgr; near=> r.
-    * apply: itv_sub_in2 ndF.
-      apply: (subset_itvW _ _ (ltW ax)).
-      by near: r; exact: nbhs_right_le.
-    * exists (F x) => _/= [z zxr <-].
-      apply: ndF.
-      - exact: subset_itv_oo_cc.
-      - apply: (subset_itvW _ _ (ltW ax) _ zxr).
-        by near: r; exact: nbhs_right_le.
-      - by move: zxr => /[!in_itv]/= /andP[/ltW].
-  + apply/negP => /eqP Fxlr.
-    contra: mx; rewrite -leNgt => _.
-    by rewrite /Fl Fxlr subrr.
-Unshelve. all: end_near. Qed.
+have [ba|ab] := leP b a.
+  apply: sub_countable (countable0 R).
+  apply/card_le0P; rewrite -subset0 => x [/itv_boundlr_lt].
+  by rewrite bnd_simp ltNge ba.
+apply: sub_countable (countableP [set: rat]).
+apply/pcard_injP/ex_of_sigT.
+have [f hf] : {f : R -> rat & 
+    forall x, x \in `]a, b[ -> discontinuity F x -> Fl x < ratr (f x) < Fr x}.
+  apply: (@choice _ _ (fun x fx => _ -> _ -> _ < ratr fx < _)) => x.
+  case: (EM (discontinuity F x)) => dFx; last by exists 0.
+  case: (EM (x \in `]a,b[)) => xab; last by exists 0.
+  have /rat_in_itvoo[q +] := nondecreasing_discontinuity xab dFx.
+  by rewrite (in_itv (ratr _)) /=; exists q.
+exists f.
+apply/inc_inj_in/le_mono_in => x y + + xy.
+move=> /set_mem[/[dup] xab /andP[ax xb] /[dup] dFx [_ cvg_fxr _]].
+have /andP[_ fxr] := hf _ xab dFx.
+move=> /set_mem[/[dup] yab /andP[ay yb] /[dup] dFy [cvg_fyl _ _]].
+have /andP[fyl _] := hf _ yab dFy.
+rewrite -(ltr_rat R); apply: (lt_trans fxr); apply: le_lt_trans fyl.
+rewrite /Fr /Fl -fmap_at_right0E -fmap_at_left0P.
+apply: (@ler_lim _ _ _ _ _ (fun e => F (x + e)) (fun e => F (y - e))).
+- by rewrite (fmap_at_right0E x F); exact: cvg_fxr.
+- by rewrite (fmap_at_left0P y F); exact: cvg_fyl.
+near=> e; apply: ndF; rewrite ?in_itv/=; try (apply/andP; split).
+- by apply: (le_trans (ltW ax)); rewrite lerDl. 
+- near: e; apply/(nbhs_right0P _ (fun z => z <= b)).
+  by apply: nbhs_right_le.
+- near: e; apply/(nbhs_left0P _ (fun z => a <= z)).
+  by apply: nbhs_left_ge.
+- by apply: le_trans (ltW yb); rewrite gerBl.
+- rewrite lerBrDr -addrA -lerBrDl -mulr2n -mulr_natr -ler_pdivlMr//.
+  by near: e; apply: nbhs_right_le; rewrite ltr_pdivlMr// mul0r subr_gt0.
+Unshelve. all: by end_near. Qed.
 
 End discontinuity_countable.