From ce1cffe6fc4fb438df118a2528d412dc4ddc3847 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 8 Aug 2023 22:56:54 +0900 Subject: [PATCH] rebase --- theories/lebesgue_measure.v | 137 +++++------------------------------- theories/measure.v | 29 ++++++++ theories/normedtype.v | 2 +- 3 files changed, 48 insertions(+), 120 deletions(-) diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 5704227d38..a859f2ac2f 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -2206,106 +2206,6 @@ Qed. End egorov. -(* PRs in progress *) -Lemma eseries_cond {R : numFieldType} (f : nat -> \bar R) P N : - (\sum_(N <= i n /=; apply: big_nat_widenl. Qed. - -Lemma eseries_mkcondl {R : numFieldType} (f : nat -> \bar R) P Q : - (\sum_(i n; rewrite big_mkcondl. Qed. - -Lemma eseries_mkcondr {R : numFieldType} (f : nat -> \bar R) P Q : - (\sum_(i n; rewrite big_mkcondr. Qed. - -Lemma eq_eseriesr (R : numFieldType) (f g : (\bar R)^nat) (P : pred nat) {N} : - (forall i, P i -> f i = g i) -> - (\sum_(N <= i efg; congr (lim _); apply/funext => n; exact: eq_bigr. Qed. - -Lemma nneseriesZl (R : realType) (f : nat -> \bar R) (P : pred nat) x N : - (forall i, P i -> 0 <= f i)%E -> - ((\sum_(N <= i f0; rewrite -limeMl//; last exact: is_cvg_nneseries. -by congr (lim _); apply/funext => /= n; rewrite ge0_sume_distrr. -Qed. - -Lemma lee_nneseries (R : realType) (u v : (\bar R)^nat) (P : pred nat) N : - (forall i, P i -> 0 <= u i)%E -> - (forall n, P n -> u n <= v n)%E -> - (\sum_(N <= i u0 Puv; apply: lee_lim. -- by apply: is_cvg_ereal_nneg_natsum_cond => n ? /u0; exact. -- apply: is_cvg_ereal_nneg_natsum_cond => n _ Pn. - by rewrite (le_trans _ (Puv _ Pn))// u0. -- by near=> n; apply: lee_sum => k; exact: Puv. -Unshelve. all: by end_near. Qed. - -Lemma bigcup_bigcup_new (I : Type) T1 T2 (F : I -> set T1) (G : T1 -> set T2) : - \bigcup_(i in \bigcup_n F n) G i = \bigcup_n \bigcup_(i in F n) G i. -Proof. -apply/seteqP; split. - by move=> x [n [m _ D'mn] h]; exists m => //; exists n. -by move=> x [n _ [m D'nm]] h; exists m => //; exists n. -Qed. - -Lemma closed_bigcup (T : topologicalType) (I : choiceType) (A : set I) - (F : I -> set T) : - finite_set A -> (forall i, A i -> closed (F i)) -> - closed (\bigcup_(i in A) F i). -Proof. -move=> finA cF; rewrite -bigsetU_fset_set//; apply: closed_bigsetU => i. -by rewrite in_fset_set// inE; exact: cF. -Qed. - -Lemma lee_addgt0Pr {R : realFieldType} (x y : \bar R) : - reflect (forall e, (0 < e)%R -> (x <= y + e%:E)%E) (x <= y)%E. -Proof. -apply/(iffP idP) => [|]. -- move: x y => [x| |] [y| |]//. - + by rewrite lee_fin => xy e e0; rewrite -EFinD lee_fin ler_paddr// ltW. - + by move=> _ e e0; rewrite leNye. -- move: x y => [x| |] [y| |]// xy; rewrite ?leey ?leNye//. - + by rewrite lee_fin; apply/ler_addgt0Pr => e e0; rewrite -lee_fin EFinD xy. - + by move: xy => /(_ _ lte01). - + by move: xy => /(_ _ lte01). - + by move: xy => /(_ _ lte01). -Qed. -(* /PRs in progress *) - -(* TODO: move to measure.v once the eseries_cond PR is merged *) -Lemma measure_sigma_sub_additive_tail d (R : realType) (T : semiRingOfSetsType d) - (mu : {measure set T -> \bar R}) (A : set T) (F : nat -> set T) N : - (forall n, measurable (F n)) -> measurable A -> - A `<=` \bigcup_(n in ~` `I_N) F n -> - (mu A <= \sum_(N <= n mF mA AF; rewrite eseries_cond eseries_mkcondr. -rewrite (@eq_eseriesr _ _ (fun n => mu (if (N <= n)%N then F n else set0))). -- apply: measure_sigma_sub_additive => //. - + by move=> n; case: ifPn. - + move: AF; rewrite bigcup_mkcond. - by under eq_bigcupr do rewrite mem_not_I. -- by move=> o _; rewrite (fun_if mu) measure0. -Qed. - -Lemma outer_measure_sigma_subadditive_tail (T : Type) (R : realType) - (mu : {outer_measure set T -> \bar R}) N (F : (set T) ^nat) : - (mu (\bigcup_(n in ~` `I_N) (F n)) <= \sum_(N <= i if n \in ~` `I_N then F n else set0). -move/le_trans; apply. -rewrite [in leRHS]eseries_cond [in leRHS]eseries_mkcondr; apply: lee_nneseries. -- by move=> k _; exact: outer_measure_ge0. -- move=> k _; rewrite fun_if; case: ifPn => Nk; first by rewrite mem_not_I Nk. - by rewrite mem_not_I (negbTE Nk) outer_measure0. -Qed. - Definition vitali_cover {R : realType} (E : set R) I (B : I -> (R * {posnum R})%type) (D : set I) := forall x, E x -> forall e : R, 0 < e -> exists i, @@ -2370,7 +2270,7 @@ have EBr2 n : E n -> scale_cball 1 (B n) `<=` (ball (0 : R^o) (r%:num + 2))%R. move: rx; rewrite /ball /= !sub0r !normrN => rx. rewrite -(subrK x y) (le_lt_trans (ler_norm_add _ _))//. rewrite addrC ltr_le_add// -(subrK (B n).1 y) -(addrA (y - _)%R). - rewrite (le_trans (ler_norm_add _ _))// (natrD _ 1%N) ler_add//. + rewrite (le_trans (ler_norm_add _ _))// (_ : 2 = 1 + 1)%R// ler_add//. rewrite (@closed_ballE _ [normedModType R of R^o]) // in Bny. by rewrite distrC (le_trans Bny)// VB1//; exact: DV. rewrite (@closed_ballE _ [normedModType R of R^o]) // in Bnx. @@ -2388,7 +2288,7 @@ have finite_set_F i : finite_set (F i). move/(infinite_set_fset M) => [/= C] CsubFi McardC. have MC : (M%:R * (1 / (2 ^ i.+1)%:R))%:E <= mu (\bigcup_(j in [set` C]) scale_cball 1 (B j)). - rewrite (measure_bigcup mu [set` C])//; last 2 first. + rewrite (measure_bigcup [the measure _ _ of mu] [set` C])//; last 2 first. by move=> ? _; exact: measurable_scale_cball. by apply: sub_trivIset tDB; by apply: (subset_trans CsubFi) => x [[]]. rewrite /= nneseries_esum//= set_mem_set// esum_fset// fsbig_finite//=. @@ -2429,7 +2329,7 @@ have mur2_fin_num_ : mu (ball (0 : R^o) (r%:num + 2))%R < +oo. by rewrite lebesgue_measure_ball// ltry. have FE : \sum_(n //. - by move=> i; apply: bigcup_measurable => *; exact: measurable_scale_cball. @@ -2438,7 +2338,7 @@ have FE : \sum_(n //. by move=> k -[] /DV /VB1. by rewrite -E_partition; apply: sub_trivIset tDB => x []. - - rewrite -bigcup_bigcup_new; apply: bigcup_measurable => k _. + - rewrite -bigcup_bigcup; apply: bigcup_measurable => k _. exact: measurable_scale_cball. apply: (@eq_eseriesr _ (fun n => mu (\bigcup_(i in F n) scale_cball 1 (B i)))). move=> i _; rewrite bigcup_mkcond measure_semi_bigcup//; last 3 first. @@ -2447,12 +2347,12 @@ have FE : \sum_(n k _. exact: measurable_scale_cball. rewrite esum_mkcond//= nneseries_esum// -fun_true//=. - by under eq_esum do rewrite (fun_if mu) (measure0 mu). + by under eq_esum do rewrite (fun_if mu) (measure0 [the measure _ _ of mu]). apply/eqP; rewrite eq_le measure_ge0 andbT. apply/lee_addgt0Pr => _ /posnumP[e]; rewrite add0e. have [N F5e] : exists N, \sum_(N <= n /=. move/(@cvgrPdist_lt _ [pseudoMetricNormedZmodType R of R^o]). - have : (0 < 5^-1 * e%:num)%R by rewrite mulr_gt0// invr_gt0// ltr0n. + have : (0 < 5%:R^-1 * e%:num)%R by rewrite mulr_gt0// invr_gt0// ltr0n. move=> /[swap] /[apply]. rewrite near_map => -[N _]/(_ _ (leqnn N)) h; exists N; move: h. rewrite sub0r normrN ger0_norm//; last first. @@ -2494,7 +2394,7 @@ have closedK : closed K. apply: closed_bigcup => //= i iN; apply: closed_bigcup => //. by move=> j Fij; exact: (@closed_ball_closed _ [normedModType R of R^o]). have ZNF5 : Z r%:num `<=` - \bigcup_(i in ~` `I_N) \bigcup_(j in F i) scale_cball 5 (B j). + \bigcup_(i in ~` `I_N) \bigcup_(j in F i) scale_cball 5%:R (B j). move=> z Zz. have Kz : ~ K z. rewrite /K => -[n /= nN [m] [[Dm _] _] Bmz]. @@ -2539,7 +2439,7 @@ have ZNF5 : Z r%:num `<=` by rewrite (le_trans Biy)// ltW. have [j [Ej Bij0 Bij5]] : exists j, [/\ E j, scale_cball 1 (B i) `&` scale_cball 1 (B j) !=set0 & - scale_cball 1 (B i) `<=` scale_cball 5 (B j)]. + scale_cball 1 (B i) `<=` scale_cball 5%:R (B j)]. have [j [Dj Bij0 Bij2 Bij5]] := Dintersect _ Vi. exists j; split => //; split => //. by move: Bij0; rewrite setIC; exact: subsetI_neq0. @@ -2551,13 +2451,13 @@ have ZNF5 : Z r%:num `<=` exists k => //= kN. by apply: BjK => x Bjx; exists k => //; exists j. by exists k => //; exists j => //; exact: Bij5. -have {ZNF5}ZNF5 : - mu (Z r%:num) <= \sum_(N <= m //. move=> n; apply: bigcup_measurable => k _. by apply: measurable_closed_ball => //; rewrite mulr_ge0// ler0n. @@ -2567,22 +2467,21 @@ have {ZNF5}ZNF5 : rewrite -[in leRHS](set_mem_set (F n)) -nneseries_esum//. rewrite bigcup_mkcond eseries_mkcond. rewrite [leRHS](_ : _ = \sum_(i x. by under [RHS]eq_bigr do rewrite (fun_if mu) measure0. apply: measure_sigma_sub_additive => //. - + move=> m; case: ifPn => // _; apply: measurable_scale_cball => //. - exact: ler0n. + + by move=> m; case: ifPn => // _; exact: measurable_scale_cball. + apply: bigcup_measurable => k _; case: ifPn => // _. - by apply: measurable_scale_cball; exact: ler0n. + exact: measurable_scale_cball. apply/(le_trans ZNF5)/ltW. move: F5e. -rewrite [in X in X -> _](@lte_pdivl_mull R 5%R e%:num%:E) ?ltr0n//. +rewrite [in X in X -> _](@lte_pdivl_mull R 5%:R e%:num%:E) ?ltr0n//. rewrite -nneseriesZl//; last by move=> *; exact: esum_ge0. move/le_lt_trans; apply. apply: lee_nneseries => //; first by move=> *; exact: esum_ge0. move=> n _. -rewrite -(set_mem_set (F n)) -nneseries_esum// -nneseries_esum// -nneseriesrM//. +rewrite -(set_mem_set (F n)) -nneseries_esum// -nneseries_esum// -nneseriesZl//. apply: lee_nneseries => // m mFn. rewrite scale_cball1 lebesgue_measure_closed_ball ?mulr_ge0 ?ler0n//. by rewrite lebesgue_measure_closed_ball// -EFinM mulrnAr. diff --git a/theories/measure.v b/theories/measure.v index 49610304fe..51cf7819ea 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -2618,6 +2618,21 @@ Qed. End more_premeasure_ring_lemmas. +Lemma measure_sigma_sub_additive_tail d (R : realType) (T : semiRingOfSetsType d) + (mu : {measure set T -> \bar R}) (A : set T) (F : nat -> set T) N : + (forall n, measurable (F n)) -> measurable A -> + A `<=` \bigcup_(n in ~` `I_N) F n -> + (mu A <= \sum_(N <= n mF mA AF; rewrite eseries_cond eseries_mkcondr. +rewrite (@eq_eseriesr _ _ (fun n => mu (if (N <= n)%N then F n else set0))). +- apply: measure_sigma_sub_additive => //. + + by move=> n; case: ifPn. + + move: AF; rewrite bigcup_mkcond. + by under eq_bigcupr do rewrite mem_not_I. +- by move=> o _; rewrite (fun_if mu) measure0. +Qed. + Section ring_sigma_content. Context d (R : realType) (T : semiRingOfSetsType d) (mu : {measure set T -> \bar R}). @@ -3354,6 +3369,20 @@ Arguments outer_measure_ge0 {R T} _. Arguments le_outer_measure {R T} _. Arguments outer_measure_sigma_subadditive {R T} _. +Lemma outer_measure_sigma_subadditive_tail (T : Type) (R : realType) + (mu : {outer_measure set T -> \bar R}) N (F : (set T) ^nat) : + (mu (\bigcup_(n in ~` `I_N) (F n)) <= \sum_(N <= i if n \in ~` `I_N then F n else set0). +move/le_trans; apply. +rewrite [in leRHS]eseries_cond [in leRHS]eseries_mkcondr; apply: lee_nneseries. +- by move=> k _; exact: outer_measure_ge0. +- move=> k _; rewrite fun_if; case: ifPn => Nk; first by rewrite mem_not_I Nk. + by rewrite mem_not_I (negbTE Nk) outer_measure0. +Qed. + Section outer_measureU. Context d (T : semiRingOfSetsType d) (R : realType). Variable mu : {outer_measure set T -> \bar R}. diff --git a/theories/normedtype.v b/theories/normedtype.v index 28725d7832..d90ad20b8d 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -5899,7 +5899,7 @@ move/(@nbhs_closedballP R M _ x) => [r xrA]. have r2k20 : 0 < minr (r%:num / 2) (k / 2) by rewrite lt_minr// !divr_gt0. exists (PosNum r2k20) => /=. by rewrite lt_minl orbC ltr_pdivr_mulr// ltr_pmulr// ltr1n. -apply/(subset_trans _ xrA)/(subset_trans _ (subset_closed_ball _)) => //. +apply/(subset_trans _ xrA)/(subset_trans _ (@subset_closed_ball _ _ _ _)) => //. by apply: le_ball; rewrite le_minl; rewrite ler_pdivr_mulr// ler_pmulr// ler1n. Qed.