diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index d7f0405803..fa5a839d4d 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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 diff --git a/theories/realfun.v b/theories/realfun.v index 66d39f9430..c520139b26 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. @@ -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.