From 212fca47f2102dccf2325ee420089be1802c746e Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Thu, 6 Feb 2025 01:32:26 +0900 Subject: [PATCH] nondecreasing functions have a countable number of discontinuities (#1451) * nondecreasing functions have a countable number of discontinuities Co-authored-by: IshiguroYoshihiro Co-authored-by: Cyril Cohen --- CHANGELOG_UNRELEASED.md | 9 ++ classical/cardinality.v | 2 +- classical/classical_sets.v | 5 + classical/mathcomp_extra.v | 25 ++++ theories/lebesgue_measure.v | 4 +- theories/realfun.v | 290 +++++++++++++++++++++++++++++++++++- 6 files changed, 330 insertions(+), 5 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index b63f2eda7..9fe9b53a8 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -51,6 +51,15 @@ + lemmas `ler0_derive1_nincry`, `ger0_derive1_ndecry`, `ler0_derive1_nincrNy`, `ger0_derive1_ndecrNy` + lemmas `ltr0_derive1_decr`, `gtr0_derive1_incr` +- in `mathcomp_extra.v`: + + lemmas `size_filter_gt0`, `ltr_sum`, `ltr_sum_nat` + +- in `classical_sets.v`: + + lemma `itv_sub_in2` + +- in `realfun.v`: + + definition `discontinuity` + + lemmas `nondecreasing_fun_sum_le`, `discontinuty_countable` ### Changed diff --git a/classical/cardinality.v b/classical/cardinality.v index 9b73d1de3..cd220934a 100644 --- a/classical/cardinality.v +++ b/classical/cardinality.v @@ -1002,7 +1002,7 @@ move=> /finite_setP[m Am]; rewrite (card_fset_set Am). by rewrite (card_le_eqr Am) card_le_II. Qed. -Lemma infinite_set_fset {T : choiceType} (A : set T) (n : nat) : +Lemma infinite_set_fset {T : choiceType} (A : set T) n : infinite_set A -> exists2 B : {fset T}, [set` B] `<=` A & (#|` B| >= n)%N. Proof. diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 86b9b0ebe..4c6d2ee34 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -465,6 +465,11 @@ Lemma nat_nonempty : [set: nat] !=set0. Proof. by exists 1%N. Qed. #[global] Hint Resolve nat_nonempty : core. +Lemma itv_sub_in2 d (T : porderType d) (P : T -> T -> Prop) (i j : interval T) : + [set` j] `<=` [set` i] -> + {in i &, forall x y, P x y} -> {in j &, forall x y, P x y}. +Proof. by move=> ji + x y xj yj; apply; exact: ji. Qed. + Lemma preimage_itv T d (rT : porderType d) (f : T -> rT) (i : interval rT) (x : T) : ((f @^-1` [set` i]) x) = (f x \in i). Proof. by rewrite inE. Qed. diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 7f5eeb3af..442af2e64 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -588,3 +588,28 @@ rewrite mulr_ile1 ?andbT//. by have := xs01 x; rewrite inE xs orbT => /(_ _)/andP[]. by rewrite ih// => e xs; rewrite xs01// in_cons xs orbT. Qed. + +(* TODO: move to ssrnum *) + +Lemma size_filter_gt0 T P (r : seq T) : (size (filter P r) > 0)%N = (has P r). +Proof. by elim: r => //= x r; case: ifP. Qed. + +Lemma ltr_sum [R : numDomainType] [I : Type] (r : seq I) + [P : pred I] [F G : I -> R] : + has P r -> + (forall i : I, P i -> F i < G i) -> + \sum_(i <- r | P i) F i < \sum_(i <- r | P i) G i. +Proof. +rewrite -big_filter -[ltRHS]big_filter -size_filter_gt0. +case: filter (filter_all P r) => //= x {}r /andP[Px Pr] _ ltFG. +rewrite !big_cons ltr_leD// ?ltFG// -(all_filterP Pr) !big_filter. +by rewrite ler_sum => // i Pi; rewrite ltW ?ltFG. +Qed. + +Lemma ltr_sum_nat [R : numDomainType] [m n : nat] [F G : nat -> R] : + (m < n)%N -> (forall i : nat, (m <= i < n)%N -> F i < G i) -> + \sum_(m <= i < n) F i < \sum_(m <= i < n) G i. +Proof. +move=> lt_mn i; rewrite big_nat [ltRHS]big_nat ltr_sum//. +by apply/hasP; exists m; rewrite ?mem_index_iota leqnn lt_mn. +Qed. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 108042b88..f3b1b30d8 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -2824,7 +2824,7 @@ have {}EBr2 : \esum_(i in E) mu (closure (B i)) <= have finite_set_F i : finite_set (F i). apply: contrapT. pose M := `|ceil ((r%:num + 2) *+ 2 / (1 / (2 ^ i.+1)%:R))|.+1. - move/(infinite_set_fset M) => [/= C] CsubFi McardC. + move/(infinite_set_fset M) => [/= C CsubFi McardC]. have MC : (M%:R * (1 / (2 ^ i.+1)%:R))%:E <= mu (\bigcup_(j in [set` C]) closure (B j)). rewrite (measure_bigcup _ [set` C])//; last 2 first. @@ -3185,7 +3185,7 @@ have {}Hc : mu (\bigcup_(k in G) closure (B k) `\` by rewrite lteBlDr-?lteBlDl//; exact: muGSfin. have bigBG_fin (r : {posnum R}) : finite_set (bigB G r%:num). pose M := `|ceil (fine (mu O) / r%:num)|.+1. - apply: contrapT => /infinite_set_fset /= /(_ M)[G0 G0G'r] MG0. + apply: contrapT => /infinite_set_fset /= /(_ M)[G0 G0G'r MG0]. have : mu O < mu (\bigcup_(k in bigB G r%:num) closure (B k)). apply: (@lt_le_trans _ _ (mu (\bigcup_(k in [set` G0]) closure (B k)))). rewrite bigcup_fset measure_fbigsetU//=; last 2 first. diff --git a/theories/realfun.v b/theories/realfun.v index 235f87458..865431d67 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -4,7 +4,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum archimedean. From mathcomp Require Import matrix interval zmodp vector fieldext falgebra. From mathcomp Require Import finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality ereal reals signed. +From mathcomp Require Import cardinality contra ereal reals signed. From mathcomp Require Import topology prodnormedzmodule tvs normedtype derive. From mathcomp Require Import sequences real_interval. @@ -36,12 +36,16 @@ From mathcomp Require Import sequences real_interval. (* *) (* ``` *) (* *) -(* * Limit superior and inferior for functions: *) +(* Limit superior and inferior for functions: *) (* ``` *) (* lime_sup f a/lime_inf f a == limit sup/inferior of the extended real- *) (* valued function f at point a *) (* ``` *) (* *) +(* Discontinuities: *) +(* ``` *) +(* discontinuity f r == r is a discontinuity of function f *) +(* ``` *) (******************************************************************************) Set Implicit Arguments. @@ -2586,3 +2590,285 @@ apply/continuous_within_itvP => //; split. Qed. End variation_continuity. + +Definition discontinuity {R : realType} (f : R -> R) (r : R) := + [/\ cvg (f x @[x --> r^'-]), + cvg (f x @[x --> r^'+]) & + lim (f x @[x --> r^'-]) != lim (f x @[x --> r^'+]) ]. + +Section discontinuity_countable. +Context {R : realType}. +Variables (a b : R) (F : R -> R). +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//; last exact: (leq_trans _ ns). + rewrite !nth_iota// ?add0n; last 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). + 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 size_iota. + + 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). + rewrite nth_iota// add0n midf_le// ltW//. + have /pathP := abs.1; apply. + by rewrite (prednK sizes0). + by rewrite size_iota. +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 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 (`|floor (Fr (sval x) - Fl (sval x))^-1|)%N. + rewrite invf_plt ?posrE ?subr_gt0// -natr1 natr_absz ger0_norm; last first. + by rewrite floor_ge0 invr_ge0// subr_ge0 ltW. + by rewrite intrD1 mathcomp_extra.lt_succ_floor// realE. +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 * `|ceil (F b - F a)|).+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 => _. + apply: (@le_lt_trans _ _`|ceil (F b - F a)|%:R). + by rewrite natr_absz intr_norm ler_normr ceil_ge. + apply: (@lt_trans _ _ (m.+1%:R^-1 * #|` B|%:R)). + by rewrite ltr_pdivlMl// -natrM ltr_nat. + 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 ltr_sum_nat//; first by rewrite -cardfE (leq_trans _ mFbFaB). + move=> k; rewrite 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 inE => -[]. +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. + +End discontinuity_countable.