From 9033e920db0af923e48ea54cd8d5c69d2a94f590 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Tue, 8 Oct 2024 18:01:52 +0900 Subject: [PATCH] corollary to Vitali's theorem (#1328) * corollary to Vitali's theorem * fixes #1334 * rm deprecated --- CHANGELOG_UNRELEASED.md | 47 +++++++ theories/constructive_ereal.v | 25 ---- theories/lebesgue_measure.v | 226 ++++++++++++++++++++++++++++++++++ theories/normedtype.v | 86 ------------- theories/sequences.v | 136 ++++++++------------ 5 files changed, 322 insertions(+), 198 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 68bcd5b60..f420fa60e 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -44,6 +44,13 @@ - in `derive.v`: + lemma `exprn_derivable` +- in `sequences.v`: + + lemma `nneseries_split_cond` + + lemma `subset_lee_nneseries` + +- in `lebesgue_measure.v`: + + lemma `vitali_coverS` + + lemma `vitali_theorem_corollary` ### Changed @@ -213,6 +220,10 @@ + lemmas `expR_ge1Dx` and `expeR_ge1Dx` (remove hypothesis) + lemma `le_ln1Dx` (weaken hypothesis) +- in `sequences.v`: + + lemma `eseries_mkcond` + + lemma `nneseries_tail_cvg` + - in `derive.v`: + lemma `derivableX` @@ -228,6 +239,42 @@ + definition `fmap_proper_filter'` + definition `filter_map_proper_filter'` + definition `filter_prod_proper'` +- in `sequences.v`: + + notation `nneseries_mkcond` (was deprecated since 0.6.0) + +- in `constructive_ereal.v`: + + notation `lte_spaddr` (deprecated since 0.6) + +- in `normedtype.v`: + + notation `normmZ` (deprecated since 0.6.0) + + notation `nbhs_image_ERFin` (deprecated since 0.6.0) + + notations `ereal_limrM`, `ereal_limMr`, `ereal_limN` (deprecated since 0.6.0) + + notation `norm_cvgi_map_lim` (deprecated since 0.6.0) + + notations `ereal_cvgN`, `ereal_is_cvgN`, `ereal_cvgrM`, `ereal_is_cvgrM`, + `ereal_cvgMr`, `ereal_is_cvgMr`, `ereal_cvgM` (deprecated since 0.6.0) + + notation `cvg_dist`, lemma `__deprecated__cvg_dist` (deprecated since 0.6.0) + + notation `cvg_dist2`, lemma `__deprecated__cvg_dist2` (deprecated since 0.6.0) + + notation `cvg_dist0`, lemma `__deprecated__cvg_dist0` (deprecated since 0.6.0) + + notation `ler0_addgt0P`, lemma `__deprecated__ler0_addgt0P` (deprecated since 0.6.0) + + notation `cvg_bounded_real`, lemma `__deprecated__cvg_bounded_real` (deprecated since 0.6.0) + + notation `linear_continuous0`, lemma `__deprecated__linear_continuous0` (deprecated since 0.6.0) + +- in `constructive_ereal.v`: + + notation `gte_opp` (deprecated since 0.6.0) + + lemmas `daddooe`, `daddeoo` + + notations `desum_ninftyP`, `desum_ninfty`, `desum_pinftyP`, `desum_pinfty` (deprecated since 0.6.0) + + notation `eq_pinftyP` (deprecated since 0.6.0) + +- in `sequences.v`: + + notation `squeeze`, lemma `__deprecated__squeeze` (deprecated since 0.6.0) + + notation `cvgPpinfty`, lemma `__deprecated__cvgPpinfty` (deprecated since 0.6.0) + + notation `cvgNpinfty`, lemma `__deprecated__cvgNpinfty` (deprecated since 0.6.0) + + notation `cvgNninfty`, lemma `__deprecated__cvgNninfty` (deprecated since 0.6.0) + + notation `cvgPninfty`, lemma `__deprecated__cvgPninfty` (deprecated since 0.6.0) + + notation `ger_cvg_pinfty`, lemma `__deprecated__ger_cvg_pinfty` (deprecated since 0.6.0) + + notation `ler_cvg_ninfty`, lemma `__deprecated__ler_cvg_ninfty` (deprecated since 0.6.0) + + notation `lim_ge`, lemma `__deprecated__lim_ge` (deprecated since 0.6.0) + + notation `lim_le`, lemma `__deprecated__lim_le` (deprecated since 0.6.0) ### Infrastructure diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v index a6780aa8e..f1a0d1cee 100644 --- a/theories/constructive_ereal.v +++ b/theories/constructive_ereal.v @@ -1258,9 +1258,6 @@ Notation mine := (@Order.min ereal_display _). Notation "@ 'mine' R" := (@Order.min ereal_display R) (at level 10, R at level 8, only parsing) : function_scope. -#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `gteN`")] -Notation gte_opp := gteN (only parsing). - Module DualAddTheoryNumDomain. Section DualERealArithTh_numDomainType. @@ -1379,14 +1376,6 @@ Lemma daddNye x : x != +oo -> -oo + x = -oo. Proof. by case: x. Qed. Lemma daddeNy x : x != +oo -> x + -oo = -oo. Proof. by case: x. Qed. -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed `daddye` and generalized")] -Lemma daddooe x : x != -oo -> +oo + x = +oo. Proof. by rewrite daddye. Qed. - -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed `daddey` and generalized")] -Lemma daddeoo x : x != -oo -> x + +oo = +oo. Proof. by rewrite daddey. Qed. - Lemma dadde_Neq_pinfty x y : x != -oo -> y != -oo -> (x + y != +oo) = (x != +oo) && (y != +oo). Proof. by move: x y => [x| |] [y| |]. Qed. @@ -1447,15 +1436,6 @@ rewrite dual_sumeE eqe_oppLR /= esum_eqy => [|i]; rewrite ?eqe_oppLR //. by under eq_existsb => i do rewrite eqe_oppLR. Qed. -#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `desum_eqNyP`")] -Notation desum_ninftyP := desum_eqNyP (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `desum_eqNy`")] -Notation desum_ninfty := desum_eqNy (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `desum_eqyP`")] -Notation desum_pinftyP := desum_eqyP (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `desum_eqy`")] -Notation desum_pinfty := desum_eqy (only parsing). - Lemma dadde_ge0 x y : 0 <= x -> 0 <= y -> 0 <= x + y. Proof. rewrite dual_addeE oppe_ge0 -!oppe_le0; exact: adde_le0. Qed. @@ -1550,9 +1530,6 @@ suff: ~ x%:E < (Order.max 0 x + 1)%:E. by apply/negP; rewrite -leNgt; apply/Ax/ltr_pwDr; rewrite // le_max lexx. Qed. -#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `eqyP`")] -Notation eq_pinftyP := eqyP (only parsing). - Lemma seq_psume_eq0 (I : choiceType) (r : seq I) (P : pred I) (F : I -> \bar R) : (forall i, P i -> 0 <= F i)%E -> (\sum_(i <- r | P i) F i == 0)%E = all (fun i => P i ==> (F i == 0%E)) r. @@ -2649,8 +2626,6 @@ Arguments lee_sum_nneg_natl {R}. Arguments lee_sum_npos_natl {R}. #[global] Hint Extern 0 (is_true (0 <= `| _ |)%E) => solve [apply: abse_ge0] : core. -#[deprecated(since="mathcomp-analysis 0.6", note="Use lte_spaddre instead.")] -Notation lte_spaddr := lte_spaddre (only parsing). #[deprecated(since="mathcomp-analysis 0.6.5", note="Use leeN2 instead.")] Notation lee_opp := leeN2 (only parsing). #[deprecated(since="mathcomp-analysis 0.6.5", note="Use lteN2 instead.")] diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 21c2a5ff6..7c79837ee 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). + +Lemma 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/normedtype.v b/theories/normedtype.v index ca1f9c395..4d4b0d41e 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -904,9 +904,6 @@ Proof. by move=> nxu; rewrite normrZ normrV// normr_id mulVr. Qed. End NormedModule_numDomainType. -#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `normrZ`")] -Notation normmZ := normrZ (only parsing). - Section NormedModule_numFieldType. Variables (R : numFieldType) (V : normedModType R). @@ -993,13 +990,6 @@ Lemma cvgr_dist_lt {T} {F : set_system T} {FF : Filter F} (f : T -> V) (y : V) : f @ F --> y -> forall eps, eps > 0 -> \forall t \near F, `|y - f t| < eps. Proof. by move=> /cvgrPdist_lt. Qed. -Lemma __deprecated__cvg_dist {F : set_system V} {FF : Filter F} (y : V) : - F --> y -> forall eps, eps > 0 -> \forall y' \near F, `|y - y'| < eps. -Proof. exact: cvgr_dist_lt. Qed. -#[deprecated(since="mathcomp-analysis 0.6.0", - note="use `cvgr_dist_lt` or a variation instead")] -Notation cvg_dist := __deprecated__cvg_dist (only parsing). - Lemma cvgr_distC_lt {T} {F : set_system T} {FF : Filter F} (f : T -> V) (y : V) : f @ F --> y -> forall eps, eps > 0 -> \forall t \near F, `|f t - y| < eps. Proof. by move=> /cvgrPdistC_lt. Qed. @@ -2064,9 +2054,6 @@ End PseudoNormedZMod_numFieldType. #[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgrPdist_le` or a variation instead")] Notation cvg_distW := __deprecated__cvg_distW (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed to `norm_cvgi_lim`")] -Notation norm_cvgi_map_lim := norm_cvgi_lim (only parsing). Section NormedModule_numFieldType. Variables (R : numFieldType) (V : normedModType R). @@ -2099,10 +2086,6 @@ Unshelve. all: by end_near. Qed. End cvgr_norm_infty. -Lemma __deprecated__cvg_bounded_real {F : set_system V} {FF : Filter F} (y : V) : - F --> y -> \forall M \near +oo, \forall y' \near F, `|y'| < M. -Proof. exact: cvgr_norm_lty. Qed. - Lemma cvg_bounded {I} {F : set_system I} {FF : Filter F} (f : I -> V) (y : V) : f @ F --> y -> bounded_near f F. Proof. exact: cvgr_norm_ley. Qed. @@ -2115,9 +2098,6 @@ Arguments cvgr_norm_geNy {R V I F FF}. Arguments cvg_bounded {R V I F FF}. #[global] Hint Extern 0 (hausdorff_space _) => solve[apply: norm_hausdorff] : core. -#[deprecated(since="mathcomp-analysis 0.6.0", - note="use `cvgr_norm_lty` or a variation instead")] -Notation cvg_bounded_real := __deprecated__cvg_bounded_real (only parsing). Module Export NbhsNorm. Definition nbhs_simpl := (nbhs_simpl,@nbhs_nbhs_norm,@filter_from_norm_nbhs). @@ -2408,16 +2388,6 @@ Lemma cvgr2dist_lt {I J} {F : set_system I} {G : set_system J} \forall i \near F & j \near G, `| (y, z) - (f i, g j) | < eps. Proof. by rewrite cvgr2dist_ltP. Qed. -Lemma __deprecated__cvg_dist2 {F : set_system U} {G : set_system V} - {FF : Filter F} {FG : Filter G} (y : U) (z : V): - (F, G) --> (y, z) -> - forall eps, 0 < eps -> - \forall y' \near F & z' \near G, `|(y, z) - (y', z')| < eps. -Proof. exact: cvgr2dist_lt. Qed. -#[deprecated(since="mathcomp-analysis 0.6.0", -note="use `cvgr2dist_lt` or a variant instead")] -Notation cvg_dist2 := __deprecated__cvg_dist2 (only parsing). - End prod_NormedModule_lemmas. Arguments cvgr2dist_ltP {_ _ _ _ _ F G FF FG}. Arguments cvgr2dist_lt {_ _ _ _ _ F G FF FG}. @@ -2587,15 +2557,6 @@ Proof. by rewrite norm_cvg0P. Qed. End cvg_composition_pseudometric. -Lemma __deprecated__cvg_dist0 {U} {K : numFieldType} {V : normedModType K} - {F : set_system U} {FF : Filter F} (f : U -> V) : - (fun x => `|f x|) @ F --> (0 : K) - -> f @ F --> (0 : V). -Proof. exact: norm_cvg0. Qed. -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed to `norm_cvg0` and generalized to `pseudoMetricNormedZmodType`")] -Notation cvg_dist0 := __deprecated__cvg_dist0 (only parsing). - Section cvg_composition_normed. Context {K : numFieldType} {V : normedModType K} {T : Type}. Context (F : set_system T) {FF : Filter F}. @@ -3156,28 +3117,6 @@ Qed. End max_cts. -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed to cvgeN, and generalized to filter in Type")] -Notation ereal_cvgN := cvgeN (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed to is_cvgeN, and generalized to filter in Type")] -Notation ereal_is_cvgN := is_cvgeN (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed to cvgeMl, and generalized to filter in Type")] -Notation ereal_cvgrM := cvgeMl (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed to is_cvgeMl, and generalized to filter in Type")] -Notation ereal_is_cvgrM := is_cvgeMl (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed to cvgeMr, and generalized to filter in Type")] -Notation ereal_cvgMr := cvgeMr (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed to is_cvgeMr, and generalized to filter in Type")] -Notation ereal_is_cvgMr := is_cvgeMr (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed to cvgeM, and generalized to a realFieldType")] -Notation ereal_cvgM := cvgeM (only parsing). - Section pseudoMetricDist. Context {R : realType} {X : pseudoMetricType R}. Implicit Types r : R. @@ -4216,10 +4155,6 @@ End ereal_is_hausdorff. #[global] Hint Extern 0 (hausdorff_space _) => solve[apply: ereal_hausdorff] : core. -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed to `nbhs_image_EFin`")] -Notation nbhs_image_ERFin := nbhs_image_EFin (only parsing). - Lemma EFin_lim (R : realFieldType) (f : nat -> R) : cvgn f -> limn (EFin \o f) = (limn f)%:E. Proof. @@ -4314,13 +4249,6 @@ Proof. by move=> ? ?; apply/cvg_lim => //; apply: cvg_nnesum. Qed. End ecvg_realFieldType_proper. -#[deprecated(since="mathcomp-analysis 0.6.0", note="generalized to `limeMl`")] -Notation ereal_limrM := limeMl (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", note="generalized to `limeMr`")] -Notation ereal_limMr := limeMr (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", note="generalized to `limeN`")] -Notation ereal_limN := limeN (only parsing). - Section cvg_0_pinfty. Context {R : realFieldType} {I : Type} {a : set_system I} {FF : Filter a}. Implicit Types f : I -> R. @@ -4793,13 +4721,6 @@ Qed. End segment. -Lemma __deprecated__ler0_addgt0P (R : numFieldType) (x : R) : - reflect (forall e, e > 0 -> x <= e) (x <= 0). -Proof. exact: ler_gtP. Qed. -#[deprecated(since="mathcomp-analysis 0.6.0", - note="use `ler_gtP` instead which generalizes it to any upper bound.")] -Notation ler0_addgt0P := __deprecated__ler0_addgt0P (only parsing). - Lemma IVT (R : realType) (f : R -> R) (a b v : R) : a <= b -> {within `[a, b], continuous f} -> minr (f a) (f b) <= v <= maxr (f a) (f b) -> @@ -5486,10 +5407,6 @@ near do rewrite /= linearD (le_trans (ler_normD _ _))// -lerBrDl. by apply: cvgr0_norm_le; rewrite // subr_gt0. Unshelve. all: by end_near. Qed. -Lemma __deprecated__linear_continuous0 (f : {linear V -> W}) : - {for 0, continuous f} -> bounded_near f (nbhs (0 : V)). -Proof. exact: continuous_linear_bounded. Qed. - Lemma bounded_linear_continuous (f : {linear V -> W}) : bounded_near f (nbhs (0 : V)) -> continuous f. Proof. @@ -5527,9 +5444,6 @@ by rewrite ler_pM. Unshelve. all: by end_near. Qed. End LinearContinuousBounded. -#[deprecated(since="mathcomp-analysis 0.6.0", - note="generalized to `continuous_linear_bounded`")] -Notation linear_continuous0 := __deprecated__linear_continuous0 (only parsing). #[deprecated(since="mathcomp-analysis 0.6.0", note="generalized to `bounded_linear_continuous`")] Notation linear_bounded0 := __deprecated__linear_bounded0 (only parsing). diff --git a/theories/sequences.v b/theories/sequences.v index 056cc7d07..b09e633ba 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -2,7 +2,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix. From mathcomp Require Import interval rat archimedean. -From mathcomp Require Import boolp classical_sets functions. +From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import set_interval. Require Import reals ereal signed topology normedtype landau. @@ -113,7 +113,6 @@ Unset Strict Implicit. Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Def Num.Theory. Import numFieldNormedType.Exports. -From mathcomp Require Import mathcomp_extra. Local Open Scope classical_set_scope. Local Open Scope ring_scope. @@ -424,68 +423,6 @@ Section sequences_R_lemmas_realFieldType. Variable R : realFieldType. Implicit Types u v : R ^nat. -Lemma __deprecated__squeeze T (f g h : T -> R) (a : filter_on T) : - (\forall x \near a, f x <= g x <= h x) -> forall (l : R), - f @ a --> l -> h @ a --> l -> g @ a --> l. -Proof. exact: squeeze_cvgr. Qed. -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed to `squeeze_cvgr`")] -Notation squeeze := __deprecated__squeeze (only parsing). - -Lemma __deprecated__cvgPpinfty (u_ : R ^nat) : - u_ @ \oo --> +oo <-> forall A, \forall n \near \oo, A <= u_ n. -Proof. exact: cvgryPge. Qed. -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed to `cvgryPge`, and generalized to any filter")] -Notation cvgPpinfty := __deprecated__cvgPpinfty (only parsing). - -Lemma __deprecated__cvgNpinfty u_ : (- u_ @ \oo --> +oo) = (u_ @ \oo --> -oo). -Proof. exact/propeqP/cvgNry. Qed. -#[deprecated(since="mathcomp-analysis 0.6.0", - note="use `cvgNry` instead")] -Notation cvgNpinfty := __deprecated__cvgNpinfty (only parsing). - -Lemma __deprecated__cvgNninfty u_ : (- u_ @ \oo --> -oo) = (u_ @ \oo --> +oo). -Proof. exact/propeqP/cvgNrNy. Qed. -#[deprecated(since="mathcomp-analysis 0.6.0", - note="use `cvgNrNy` instead")] -Notation cvgNninfty := __deprecated__cvgNninfty (only parsing). - -Lemma __deprecated__cvgPninfty (u_ : R ^nat) : - u_ @ \oo --> -oo <-> forall A, \forall n \near \oo, A >= u_ n. -Proof. exact: cvgrNyPle. Qed. -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed to `cvgrNyPle`, and generalized to any filter")] -Notation cvgPninfty := __deprecated__cvgPninfty (only parsing). - -Lemma __deprecated__ger_cvg_pinfty u_ v_ : (\forall n \near \oo, u_ n <= v_ n) -> - u_ @ \oo --> +oo -> v_ @ \oo --> +oo. -Proof. exact: ger_cvgy. Qed. -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed to `ger_cvgy`, and generalized to any filter")] -Notation ger_cvg_pinfty := __deprecated__ger_cvg_pinfty (only parsing). - -Lemma __deprecated__ler_cvg_ninfty v_ u_ : (\forall n \near \oo, u_ n <= v_ n) -> - v_ @ \oo --> -oo -> u_ @ \oo --> -oo. -Proof. exact: ler_cvgNy. Qed. -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed to `ler_cvgNy`, and generalized to any filter")] -Notation ler_cvg_ninfty := __deprecated__ler_cvg_ninfty (only parsing). - -Lemma __deprecated__lim_ge x u : cvg (u @ \oo) -> - (\forall n \near \oo, x <= u n) -> x <= lim (u @ \oo). -Proof. exact: limr_ge. Qed. -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed to `limr_ge`, and generalized to any proper filter")] -Notation lim_ge := __deprecated__lim_ge (only parsing). - -Lemma __deprecated__lim_le x u : cvg (u @ \oo) -> - (\forall n \near \oo, x >= u n) -> x >= lim (u @ \oo). -Proof. exact: limr_le. Qed. -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed to `limr_le`, and generalized to any proper filter")] -Notation lim_le := __deprecated__lim_le (only parsing). - Lemma lt_lim u (M : R) : nondecreasing_seq u -> cvgn u -> M < limn u -> \forall n \near \oo, M <= u n. Proof. @@ -1297,7 +1234,7 @@ rewrite /series; near \oo => N; have xN : x < N%:R; last first. rewrite -(@is_cvg_series_restrict N.+1). by apply: (nondecreasing_is_cvgn (incr_S1 N)); eexists; apply: S1_sup. near: N; exists `|floor x|.+1 => // m; rewrite /mkset -(@ler_nat R). -move/lt_le_trans => -> //; rewrite (lt_le_trans (lt_succ_floor x))//. +move/lt_le_trans => -> //; rewrite (lt_le_trans (mathcomp_extra.lt_succ_floor x))//. by rewrite -intrD1 -natr1 lerD2r -(@gez0_abs (floor x)) ?floor_ge0// ltW. Unshelve. all: by end_near. Qed. @@ -1832,6 +1769,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 +1920,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 +2025,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 +2105,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 +2975,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 +3038,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 +3089,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.