From 6ca550189a742684619c0682c4885d022569e0b4 Mon Sep 17 00:00:00 2001 From: Neptune MM Date: Mon, 9 Nov 2026 19:51:37 +0100 Subject: [PATCH 1/3] Simply proof of discontinuity_countable --- theories/realfun.v | 299 +++++++-------------------------------------- 1 file changed, 42 insertions(+), 257 deletions(-) diff --git a/theories/realfun.v b/theories/realfun.v index 07807820c4..703b5457e5 100644 --- a/theories/realfun.v +++ b/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. @@ -2355,266 +2355,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. From 3a549207ba847f5c19928c3a6fa9cca552db3da3 Mon Sep 17 00:00:00 2001 From: Neptune MM Date: Mon, 9 Nov 2026 19:53:46 +0100 Subject: [PATCH 2/3] changelog --- CHANGELOG_UNRELEASED.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index f03eb15fa5..c576708cd8 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -63,6 +63,8 @@ + lemma `ball_open_nbhs` + lemma `metric_accessible` +- in `realfun.v`: + + lemma `nondecreasing_discontinuity`. ### Changed - in `lebesgue_integral_nonneg.v`, generalized and deprecated: @@ -105,6 +107,9 @@ ### Removed +- in `realfun.v`: + + lemma `nondecreasing_fun_sum_le`. + ### Infrastructure ### Misc From 3053780ed4e2ee6b23a0a746e4a4ea71ff6d208d Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 15 Nov 2026 19:31:53 +0900 Subject: [PATCH 3/3] nitpick --- CHANGELOG_UNRELEASED.md | 26 +++--- theories/realfun.v | 176 +++++++++++++++++++++++++++++++++++++--- 2 files changed, 178 insertions(+), 24 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index c576708cd8..07fcdbc733 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -53,29 +53,25 @@ - in `separation_axioms.v`: + lemma `separated_set1` -### Moved - -- from `pseudometric_normed_Zmodule.v` to `num_topology.v` - + lemma `ball_itv` - + new definition `seminorm_display`. - in `metric_structure.v`: + lemma `ball_open` + lemma `ball_open_nbhs` + lemma `metric_accessible` - in `realfun.v`: - + lemma `nondecreasing_discontinuity`. + + lemma `nondecreasing_discontinuity` + ### Changed - in `lebesgue_integral_nonneg.v`, generalized and deprecated: + lemma `ge0_integralZl_EFin` (no condition on `k`) - in file `function_spaces.v`, + new lemma `within_continuous_big`. -- in file `nat_topology.v`, +- in `nat_topology.v`: + new lemma `near_infty_after`. -- in file `num_topology.v`, - + new lemmas `at_rightD`, `at_leftD`, `near_at_rightD`, `near_at_leftD`, - `at_left_shift`, and `at_right_shift`. +- in `num_topology.v`; + + lemmas `at_rightD`, `at_leftD`, `near_at_rightD`, `near_at_leftD`, + `at_left_shift`, `at_right_shift` - in `realfun.v`: + lemmas `derivable_oo_LRcontinuousZ`, `derivable_oo_LRcontinuousD`, `derivable_oo_LRcontinuousN`, `derivable_oo_LRcontinuous_shift`, @@ -90,10 +86,14 @@ - in `pseudometric_structure.v`: + implicit arguments of `ball_split`, `ball_splitr`, `ball_splitl` +- moved from `pseudometric_normed_Zmodule.v` to `num_topology.v` + + lemma `ball_itv` + ### Renamed - in `lebesgue_measure.v`: + `compact_finite_measure` -> `compact_lebesgue_measure_lty` + - in `pseudometric_normed_Zmodule.v`: + `ball_open` -> `pseudo_ball_open` + `ball_open_nbhs` -> `pseudo_ball_open_nbhs` @@ -105,10 +105,10 @@ ### Deprecated -### Removed - - in `realfun.v`: - + lemma `nondecreasing_fun_sum_le`. + + lemma `nondecreasing_fun_sum_le` + +### Removed ### Infrastructure diff --git a/theories/realfun.v b/theories/realfun.v index 703b5457e5..4e76f3d8b7 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -2355,16 +2355,170 @@ 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_discontinuity x : +#[deprecated(since="mathcomp-analysis 1.20.0", note="This lemma was use to prove `discontinuity_countable` but a shorter proof has been found since.")] +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). +exact: (nondecreasing_at_left_at_right ndF). Qed. Lemma discontinuity_countable : - countable [set x | x \in (`]a, b[) /\ discontinuity F x]. + countable [set x | (x \in `]a, b[) /\ discontinuity F x]. Proof. have [ba|ab] := leP b a. apply: sub_countable (countable0 R). @@ -2372,7 +2526,7 @@ have [ba|ab] := leP b a. by rewrite bnd_simp ltNge ba. apply: sub_countable (countableP [set: rat]). apply/pcard_injP/ex_of_sigT. -have [f hf] : {f : R -> rat & +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. @@ -2387,16 +2541,16 @@ 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))). +apply: ler_lim. - 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: ndF; rewrite ?in_itv/=. +- rewrite (le_trans (ltW ax)) ?lerDl//=. + near: e; apply/(nbhs_right0P _ (fun z => z <= b)). + exact: nbhs_right_le. +- rewrite (le_trans _ (ltW yb)) ?gerBl ?andbT//=. - near: e; apply/(nbhs_left0P _ (fun z => a <= z)). - by apply: nbhs_left_ge. -- by apply: le_trans (ltW yb); rewrite gerBl. + exact: nbhs_left_ge. - 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.