From ed7d39ef88b311eafa58f4322382befe08984c46 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 26 Sep 2024 13:31:15 +0900 Subject: [PATCH] corollary to Vitali's theorem --- CHANGELOG_UNRELEASED.md | 13 +++ theories/lebesgue_measure.v | 226 ++++++++++++++++++++++++++++++++++++ theories/sequences.v | 69 +++++++---- 3 files changed, 286 insertions(+), 22 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index f938fac2e..81aec2833 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -15,6 +15,12 @@ - in `realfun.v`: + lemmas `cvg_pinftyP`, `cvg_ninftyP` +- in `sequences.v`: + + lemma `nneseries_split_cond` + + lemma `subset_lee_nneseries` + +- in `lebesgue_measure.v`: + + lemma `vitali_theorem_corollary` ### Changed @@ -22,10 +28,17 @@ ### Generalized +- in `sequences.v`: + + lemma `eseries_mkcond` + + lemma `nneseries_tail_cvg` + ### Deprecated ### Removed +- in `sequences.v`: + + notation `nneseries_mkcond` (was deprecated since 0.6.0) + ### Infrastructure ### Misc diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 21c2a5ff6..32f62f869 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -2963,3 +2963,229 @@ by rewrite -EFinM mulrnAr. Qed. End vitali_theorem. + +Section vitali_theorem_corollary. +Context {R : realType} (A : set R) (B : nat -> set R). + +Let vitali_coverS (F : set nat) (O : set R) : open O -> A `<=` O -> + vitali_cover A B F -> vitali_cover A B (F `&` [set k | B k `<=` O]). +Proof. +move=> oO AO [Bball ABF]; split => // x Ax r r0. +have [d xdO] : exists d : {posnum R}, ball x d%:num `<=` O. + have [/= d d0 dxO] := open_subball oO (AO _ Ax). + have d20 : (0 < d / 2)%R by rewrite divr_gt0. + exists (PosNum d20) => z xdz. + apply: (dxO (PosNum d20)%:num) => //=. + by rewrite sub0r normrN gtr0_norm// gtr_pMr// invf_lt1// ltr1n. +pose rd2 : R := minr r (d%:num / 2)%R. +have rd2_gt0 : (0 < rd2)%R by rewrite lt_min r0//= divr_gt0. +have [k [Vk Bkr Bkd]] := ABF _ Ax _ rd2_gt0. +exists k => //; split => //; last by rewrite (lt_le_trans Bkd)// ge_min// lexx. +split => //=. +apply: subset_trans xdO => /= z Bkz. +rewrite /ball/= -(addrKA (- cpoint (B k))). +rewrite (le_lt_trans (ler_normB _ _))//= -(addrC z). +rewrite (splitr d%:num) ltrD//. + rewrite distrC (lt_le_trans (is_ballP _ _))//. + by rewrite (le_trans (ltW Bkd))// ge_min lexx orbT. +rewrite distrC (lt_le_trans (is_ballP _ _))//. +by rewrite (le_trans (ltW Bkd))// ge_min lexx orbT. +Qed. + +Let vitali_cover_mclosure (F : set nat) k : + vitali_cover A B F -> (R.-ocitv.-measurable).-sigma.-measurable (closure (B k)). +Proof. +case => + _ => /(_ k)/ballE ->. +by rewrite closure_ball; exact: measurable_closed_ball. +Qed. + +Let vitali_cover_measurable (F : set nat) k : + vitali_cover A B F -> (R.-ocitv.-measurable).-sigma.-measurable (B k). +Proof. by case => + _ => /(_ k)/ballE ->; exact: measurable_ball. Qed. + +Let vitali_cover_ballE (F : set nat) n : + vitali_cover A B F -> B n = (ball (cpoint (B n)) (radius (B n))%:num). +Proof. by case => + _ => /(_ n)/ballE. Qed. + +Hypothesis B0 : forall i, (0 < (radius (B i))%:num)%R. +Notation mu := (@lebesgue_measure R). +Local Open Scope ereal_scope. + +Let bigB (G : set nat) c := G `&` [set k | (radius (B k))%:num >= c]%R. + +Let bigBS (G : set nat) r : bigB G r `<=` G. +Proof. by move=> i []. Qed. + +Let bigB0 (G : set nat) : bigB G 0%R = G. +Proof. by apply/seteqP; split => [//|x Gx]; split => //=. Qed. + +(* references: + - https://angyansheng.github.io/notes/measure-theory-xvi + - https://math.stackexchange.com/questions/4606604/a-proof-of-vitalis-covering-theorem + - https://math-wiki.com/images/2/2f/88341leb_fund_thm.pdf (p.9) +*) +Lemma vitali_theorem_corollary (F : set nat) : + mu A < +oo%E -> vitali_cover A B F -> + forall e, (e > 0)%R -> exists G' : {fset nat}, [/\ [set` G'] `<=` F, + trivIset [set` G'] (closure \o B) & + ((wlength idfun)^* (A `\` \big[setU/set0]_(k <- G') closure (B k)))%mu + < e%:E]. +Proof. +move=> muAfin ABF e e0. +have [O [oO AO OAoo]] : + exists O : set R, [/\ open O, A `<=` O & mu O < mu A + 1 < +oo]. + have /(outer_measure_open_le A) : (0 < 1 / 2 :> R)%R by rewrite divr_gt0. + move=> [O [oA AO OAe]]; exists O; split => //. + rewrite lte_add_pinfty ?ltry// andbT. + rewrite (le_lt_trans OAe)// lteD2lE ?ge0_fin_numE ?outer_measure_ge0//. + by rewrite lte_fin ltr_pdivrMr// mul1r ltr1n. +pose F' := F `&` [set k | B k `<=` O]. +have ABF' : vitali_cover A B F' by exact: vitali_coverS. +have [G [cG GV' tB mAG0]] := vitali_theorem B0 ABF'. +have muGSfin C : C `<=` G -> mu (\bigcup_(k in C) closure (B k)) \is a fin_num. + move=> CG; rewrite ge0_fin_numE// (@le_lt_trans _ _ (mu O))//; last first. + by move: OAoo => /andP[OA]; exact: lt_trans. + rewrite (@le_trans _ _ (mu (\bigcup_(k in G) B k)))//; last first. + by rewrite le_outer_measure//; apply: bigcup_sub => i /GV'[]. + rewrite bigcup_mkcond [in leRHS]bigcup_mkcond measure_bigcup//=; last 2 first. + by move=> i _; case: ifPn => // iG; exact: vitali_cover_mclosure ABF. + by apply/(trivIset_mkcond _ _).1; apply: sub_trivIset tB. + rewrite measure_bigcup//=; last 2 first. + by move=> i _; case: ifPn => // _; exact: vitali_cover_measurable ABF. + apply/(trivIset_mkcond _ _).1/trivIsetP => /= i j Gi Gj ij. + move/trivIsetP : tB => /(_ _ _ Gi Gj ij). + by apply: subsetI_eq0; exact: subset_closure. + apply: lee_nneseries => // n _. + case: ifPn => [/set_mem nC|]; last by rewrite measure0. + rewrite (vitali_cover_ballE _ ABF) ifT; last exact/mem_set/CG. + by rewrite closure_ball lebesgue_measure_closed_ball// lebesgue_measure_ball. +have muGfin : mu (\bigcup_(k in G) closure (B k)) \is a fin_num. + by rewrite -(bigB0 G) muGSfin. +have [c Hc] : exists c : {posnum R}, + mu (\bigcup_(k in bigB G c%:num) closure (B k)) > + mu (\bigcup_(k in G) closure (B k)) - e%:E. + have : \sum_(N <= k \oo] --> 0%E. + have : \sum_(0 <= i i _; exact: vitali_cover_mclosure ABF. + by move/(@nneseries_tail_cvg _ _ (mem G)); exact. + move/fine_cvgP => [_] /cvgrPdist_lt /(_ _ e0)[n _ /=] nGe. + have [c nc] : exists c : {posnum R}, forall k, + (c%:num > (radius (B k))%:num)%R -> (k >= n)%N. + pose x := (\big[minr/(radius (B 0))%:num]_(i < n.+1) (radius (B i))%:num)%R. + have x_gt0 : (0 < x)%R by exact: lt_bigmin. + exists (PosNum x_gt0) => k /=; apply: contraPleq => kn. + apply/negP; rewrite -leNgt; apply/bigmin_leP => /=; right. + by exists (widen_ord (@leqnSn _) (Ordinal kn)). + exists c. + suff: mu (\bigcup_(k in G `\` bigB G c%:num) closure (B k)) < e%:E. + rewrite EFinN lteBlDl// -lteBlDr//; last exact: muGSfin. + apply: le_lt_trans. + pose setDbigB := (\bigcup_(k in G) closure (B k)) `\` + (\bigcup_(k in bigB G c%:num) closure (B k)). + have ? : setDbigB `<=` \bigcup_(k in G `\` bigB G c%:num) closure (B k). + move=> /= x [[k Gk Bkx]]. + rewrite -[X in X -> _]/((~` _) x) setC_bigcup => abs. + by exists k => //; split=> // /abs. + apply: (@le_trans _ _ (mu setDbigB)); last first. + rewrite le_measure ?inE//. + by apply: measurableD; + apply: bigcup_measurable => k _; exact: vitali_cover_mclosure ABF. + by apply: bigcup_measurable => k _; exact: vitali_cover_mclosure ABF. + rewrite measureD//=; last 3 first. + by apply: bigcup_measurable => k _; exact: vitali_cover_mclosure ABF. + by apply: bigcup_measurable => k _; exact: vitali_cover_mclosure ABF. + by rewrite -ge0_fin_numE. + rewrite leeB// le_measure ?inE//. + by apply: measurableI; + apply: bigcup_measurable => k _; exact: vitali_cover_mclosure ABF. + by apply: bigcup_measurable => k _; exact: vitali_cover_mclosure ABF. + apply: (@le_lt_trans _ _ (normr (0 - + fine (\sum_(n <= k /=. + rewrite sub0r normrN ger0_norm/=; last by rewrite fine_ge0// nneseries_ge0. + rewrite fineK//; last first. + move: muGfin; rewrite measure_bigcup//=; last first. + by move=> i _; exact: vitali_cover_mclosure ABF. + do 2 (rewrite ge0_fin_numE//; last exact: nneseries_ge0). + apply: le_lt_trans. + by rewrite [leRHS](nneseries_split_cond 0%N n)// add0n leeDr// sume_ge0. + rewrite measure_bigcup//=; last 2 first. + by move=> i _; exact: vitali_cover_mclosure ABF. + by apply: sub_trivIset tB; exact: subDsetl. + rewrite [in leRHS]eseries_cond. + suff: forall i, i \in G `\` bigB G c%:num -> (n <= i)%N. + move=> GG'n; apply: subset_lee_nneseries => //= m mGG'. + by rewrite GG'n// andbT; case/set_mem: mGG' => /mem_set ->. + move=> i iGG'; rewrite nc//. + by move/set_mem: iGG' => [Gi] /not_andP[//|/negP]; rewrite -ltNge. +have {}Hc : mu (\bigcup_(k in G) closure (B k) `\` + \bigcup_(k in bigB G c%:num) closure (B k)) < e%:E. + rewrite measureD//=; first last. + - by rewrite -ge0_fin_numE. + - by apply: bigcup_measurable => k _; exact: vitali_cover_mclosure ABF. + - by apply: bigcup_measurable => k _; exact: vitali_cover_mclosure ABF. + rewrite setIidr; last exact: bigcup_subset. + 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. + 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. + by move=> k _; exact: vitali_cover_mclosure ABF. + by apply: sub_trivIset tB => x /G0G'r[]. + apply: (@lt_le_trans _ _ (\sum_(i <- G0) r%:num%:E)%R). + rewrite sumEFin big_const_seq iter_addr addr0 -mulr_natr. + apply: (@lt_le_trans _ _ (r%:num * M%:R)%:E); last first. + by rewrite lee_fin ler_wpM2l// ler_nat count_predT. + rewrite EFinM -lte_pdivrMl// muleC -(@fineK _ (mu O)); last first. + by rewrite ge0_fin_numE//; case/andP: OAoo => ?; exact: lt_trans. + rewrite -EFinM /M lte_fin (le_lt_trans (ceil_ge _))//. + rewrite -natr1 natr_absz ger0_norm ?ltrDl//. + by rewrite -ceil_ge0// (@lt_le_trans _ _ 0%R)// divr_ge0// fine_ge0. + rewrite big_seq [in leRHS]big_seq. + apply: lee_sum => //= i /G0G'r [iG rBi]. + rewrite -[leRHS]fineK//; last first. + rewrite (vitali_cover_ballE _ ABF). + by rewrite closure_ball lebesgue_measure_closed_ball. + rewrite (vitali_cover_ballE _ ABF) closure_ball. + by rewrite lebesgue_measure_closed_ball// fineK// lee_fin mulr2n ler_wpDl. + rewrite le_measure? inE//; last exact: bigcup_subset. + - by apply: bigcup_measurable => k _; exact: vitali_cover_mclosure ABF. + - by apply: bigcup_measurable => k _; exact: vitali_cover_mclosure ABF. + apply/negP; rewrite -leNgt. + apply: (@le_trans _ _ (mu (\bigcup_(k in bigB G r%:num) B k))). + rewrite measure_bigcup//; last 2 first. + by move=> k _; exact: vitali_cover_mclosure ABF. + exact: sub_trivIset tB. + rewrite /= measure_bigcup//; last 2 first. + by move=> k _; exact: vitali_cover_measurable ABF. + apply/trivIsetP => /= i j [Gi ri] [Gj rj] ij. + move/trivIsetP : tB => /(_ _ _ Gi Gj ij). + by apply: subsetI_eq0 => //=; exact: subset_closure. + rewrite /= lee_nneseries// => n _. + rewrite (vitali_cover_ballE _ ABF)// closure_ball. + by rewrite lebesgue_measure_closed_ball// lebesgue_measure_ball. + rewrite le_measure? inE//. + + by apply: bigcup_measurable => k _; exact: vitali_cover_measurable ABF. + + exact: open_measurable. + + by apply: bigcup_sub => i [/GV'[? ?] cBi]. +exists (fset_set (bigB G c%:num)); split. +- by move=> /= k; rewrite in_fset_set// inE /bigB /= => -[] /GV'[]. +- by apply: sub_trivIset tB => k/=; rewrite in_fset_set// inE /bigB /= => -[]. +- pose UG : set R := \bigcup_(k in G) closure (B k). + rewrite bigsetU_fset_set//. + apply: (@le_lt_trans _ _ ((wlength idfun)^*%mu (A `\`UG) + + mu (UG `\` \bigcup_(k in bigB G c%:num) closure (B k)))); last first. + by rewrite -[(wlength idfun)^*%mu]/mu mAG0 add0e. + apply: (@le_trans _ _ ((wlength idfun)^*%mu + (A `&` (UG `\` \bigcup_(k in bigB G c%:num) closure (B k))) + + (wlength idfun)^*%mu (A `\` UG))); last first. + by rewrite addeC leeD2l// le_outer_measure. + apply: (le_trans _ (outer_measureU2 _ _ _)) => //=; apply: le_outer_measure. + rewrite !(setDE A) -setIUr; apply: setIS. + by rewrite setDE setUIl setUv setTI -setCI; exact: subsetC. +Qed. + +End vitali_theorem_corollary. diff --git a/theories/sequences.v b/theories/sequences.v index 056cc7d07..bbc70e95f 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -1832,6 +1832,21 @@ move=> u0 Puv; apply: lee_lim. - by near=> n; apply: lee_sum => k; exact: Puv. Unshelve. all: by end_near. Qed. +Lemma subset_lee_nneseries (R : realType) (u : (\bar R)^nat) (P Q : pred nat) + (N : nat) : + (forall i, Q i -> 0 <= u i) -> + (forall i, P i -> Q i) -> + \sum_(N <= i Pu PQ; apply: lee_lim. +- apply: ereal_nondecreasing_is_cvgn => a b ab. + by apply: lee_sum_nneg_natr => // n Mn /PQ; exact: Pu. +- apply: ereal_nondecreasing_is_cvgn => a b ab. + by apply: lee_sum_nneg_natr => // n Mn; exact: Pu. +- near=> n; apply: lee_sum_nneg_subset => //. + by move=> i; rewrite inE => /andP[iP iQ]; exact: Pu. +Unshelve. all: by end_near. Qed. + Lemma lee_npeseries (R : realType) (u v : (\bar R)^nat) (P : pred nat) : (forall i, P i -> u i <= 0) -> (forall n, P n -> v n <= u n) -> \sum_(i //; exact: nearW. Qed. +Lemma eseries_mkcond [R : realFieldType] [P : pred nat] (f : nat -> \bar R) N : + \sum_(N <= i n /=; apply: big_mkcond. Qed. + Section nneseries_split. Let near_eq_lim (R : realFieldType) (f g : nat -> \bar R) : @@ -1964,8 +1983,19 @@ rewrite -lim_shift_cst; last by rewrite (@lt_le_trans _ _ 0)// f0// leq_addr. by rewrite f0// (leq_trans _ Nnp)// -addnS leq_addr. Unshelve. all: by end_near. Qed. +Lemma nneseries_split_cond (R : realType) (f : nat -> \bar R) N n (P : pred nat) : + (forall k, P k -> 0 <= f k)%E -> + \sum_(N <= k NPf; rewrite eseries_mkcond [X in _ = (_ + X)]eseries_mkcond. +rewrite big_mkcond/= (nneseries_split n)// => k Nk. +by case: ifPn => //; exact: NPf. +Qed. + End nneseries_split. Arguments nneseries_split {R f} _ _. +Arguments nneseries_split_cond {R f} _ _ _. Lemma nneseries_recl (R : realType) (f : nat -> \bar R) : (forall k, 0 <= f k) -> \sum_(k f0; rewrite [LHS](nneseries_split _ 1)// add0n. by rewrite /index_iota subn0/= big_cons big_nil addr0. Qed. -Lemma nneseries_tail_cvg (R : realType) (f : (\bar R)^nat) : - \sum_(k (forall k, 0 <= f k) -> - \sum_(N <= k \oo] --> 0. +Lemma nneseries_tail_cvg (R : realType) (f : (\bar R)^nat) P : + (\sum_(0 <= k (forall k, P k -> 0 <= f k) -> + \sum_(N <= k \oo] --> 0)%E. Proof. move=> foo f0. -have : cvg (\sum_(0 <= k < n) f k @[n --> \oo]). - by apply: ereal_nondecreasing_is_cvgn; exact: lee_sum_nneg_natr. +have : cvg (\sum_(0 <= k < n | P k) f k @[n --> \oo]). + apply: ereal_nondecreasing_is_cvgn. + by apply: lee_sum_nneg_natr => n _; exact: f0. move/cvg_ex => [[l fl||/cvg_lim fnoo]] /=; last 2 first. - by move/cvg_lim => fpoo; rewrite fpoo// in foo. - - have : 0 <= \sum_(k _](_ : _ = fun N => l%:E - \sum_(0 <= k < N) f k). +rewrite [X in X @ _ --> _](_ : _ = fun N => l%:E - \sum_(0 <= k < N | P k) f k). apply/cvgeNP; rewrite oppe0. under eq_fun => ? do rewrite oppeD// oppeK addeC. exact/cvge_sub0. apply/funext => N; apply/esym/eqP; rewrite sube_eq//. - by rewrite addeC -nneseries_split//; exact/eqP/esym/cvg_lim. + by rewrite addeC -nneseries_split_cond//; exact/eqP/esym/cvg_lim. by rewrite ge0_adde_def//= ?inE; [exact: nneseries_ge0|exact: sume_ge0]. Qed. @@ -2057,10 +2088,6 @@ have : limn u <= M%:E by apply lime_le => //; near=> m; apply/ltW/Mu. by move/(lt_le_trans Ml); rewrite ltxx. Unshelve. all: by end_near. Qed. -Lemma eseries_mkcond [R : realFieldType] [P : pred nat] (f : nat -> \bar R) : - \sum_(i n /=; apply: big_mkcond. Qed. - End sequences_ereal. #[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeyPge` or a variant instead")] @@ -2141,8 +2168,6 @@ Notation nneseries0 := eseries0 (only parsing). Notation eq_nneseries := eq_eseriesr (only parsing). #[deprecated(since="analysis 0.6.0", note="Use eseries_pred0 instead.")] Notation nneseries_pred0 := eseries_pred0 (only parsing). -#[deprecated(since="analysis 0.6.0", note="Use eseries_mkcond instead.")] -Notation nneseries_mkcond := eseries_mkcond (only parsing). Arguments nneseries_split {R f} _ _. @@ -3013,11 +3038,11 @@ have : cvg (a @ \oo). have [n rne] : exists n, 2 * (r n)%:num < e. pose eps := e / 2. have [n n1e] : exists n, n.+1%:R^-1 < eps. - exists `|ceil eps^-1|%N. + exists `|ceil eps^-1|%N. rewrite -ltf_pV2 ?(posrE,divr_gt0)// invrK -addn1 natrD. - rewrite natr_absz gtr0_norm. - by rewrite (le_lt_trans (ceil_ge _)) // ltrDl. - by rewrite -ceil_gt0 invr_gt0 divr_gt0. + rewrite natr_absz gtr0_norm. + by rewrite (le_lt_trans (ceil_ge _)) // ltrDl. + by rewrite -ceil_gt0 invr_gt0 divr_gt0. exists n.+1; rewrite -ltr_pdivlMl //. have /lt_trans : (r n.+1)%:num < n.+1%:R^-1. have [_ ] : P n.+1 (a n, r n) (a n.+1, r n.+1) by apply: (Pf (n, ar n)). @@ -3076,11 +3101,11 @@ Unshelve. all: by end_near. Qed. (* TODO: to be changed once PR#1107 is integrated, and the following put in evt.v *) -(* Definition bounded_top (K: realType) (E : normedModType K) (B : set E) := -forall (U : set E), nbhs 0 U -> +(* Definition bounded_top (K: realType) (E : normedModType K) (B : set E) := +forall (U : set E), nbhs 0 U -> (exists (k:K), B `<=` (fun (x:E) => (k *: x) ) @` U). -Definition pointwise_bounded (K : realType) (V : normedModType K) (W : normedModType K) +Definition pointwise_bounded (K : realType) (V : normedModType K) (W : normedModType K) (F : set (V -> W)) := bounded_top F {ptws V -> W}. Definition uniform_bounded (K : realType) (V : normedModType K) (W : normedModType K) @@ -3127,7 +3152,7 @@ have ContraBaire : exists i, not (dense (O i)). - by move=> x; rewrite setI0. - by exists point. - exact: openT. - have /contra_not/(_ dOinf) : (forall i, open(O i) /\ dense (O i)) -> dense (O_inf). + have /contra_not/(_ dOinf) : (forall i, open (O i) /\ dense (O i)) -> dense (O_inf). exact: Baire. move=> /asboolPn /existsp_asboolPn[n /and_asboolP /nandP Hn]. by exists n; case: Hn => /asboolPn.