From f063e176d7e3ce50450ac49557eeb674f347ac92 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 22 Jun 2023 22:08:45 +0900 Subject: [PATCH 1/4] tentative formalization of Vitali's theorem --- CHANGELOG_UNRELEASED.md | 21 +++ classical/classical_sets.v | 14 ++ theories/lebesgue_measure.v | 299 ++++++++++++++++++++++++++++++++++++ theories/measure.v | 29 ++++ theories/normedtype.v | 45 +++++- theories/reals.v | 4 + theories/sequences.v | 24 ++- 7 files changed, 433 insertions(+), 3 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index fc8dc4bb6f..7d64630d4c 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -100,6 +100,27 @@ - in `measure.v`: + lemma `probability_setC` +- in `classical_sets.v`: + + lemmas `mem_not_I`, `trivIsetT_bigcup` + +- in `lebesgue_measure.v`: + + definition `vitali_cover` + + lemma `vitali_theorem` + +- in `measure.v`: + + lemma `measure_sigma_sub_additive_tail` + + lemma `outer_measure_sigma_subadditive_tail` + +- in `normedtype.v`: + + lemma `open_subball` + + lemma `closed_disjoint_closed_ball` + + lemma `is_scale_ball` + +- in `reals.v`: + + lemmas `ceilN`, `floorN` + +- in `sequences.v`: + + lemma `nneseries_tail_cvg` ### Changed diff --git a/classical/classical_sets.v b/classical/classical_sets.v index da56456627..169bbd94ce 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -1124,6 +1124,9 @@ Proof. by move=> k; apply/val_inj. Qed. Lemma IIordK {n} : cancel (@IIord n) ordII. Proof. by move=> k; apply/val_inj. Qed. +Lemma mem_not_I N n : (n \in ~` `I_N) = (N <= n). +Proof. by rewrite in_setC /mkset /in_mem /mem /= /in_set asboolb -leqNgt. Qed. + End InitialSegment. Lemma setT_unit : [set: unit] = [set tt]. @@ -2567,6 +2570,17 @@ have [nm|nm] := eqVneq n m; first by apply: (tB m) => //; rewrite -nm. exact: (H _ _ _ _ nm). Qed. +Lemma trivIsetT_bigcup T1 T2 (I : eqType) (D : I -> set T1) (F : T1 -> set T2) : + trivIset setT D -> + trivIset (\bigcup_i D i) F -> + trivIset setT (fun i => \bigcup_(t in D i) F t). +Proof. +move=> D0 h i j _ _ [t [[m Dim Fmt] [n Djn Fnt]]]. +have mn : m = n by apply: h => //; [exists i|exists j|exists t]. +rewrite {}mn {m} in Dim Fmt *. +by apply: D0 => //; exists n. +Qed. + Definition cover T I D (F : I -> set T) := \bigcup_(i in D) F i. Lemma coverE T I D (F : I -> set T) : cover D F = \bigcup_(i in D) F i. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 798b332654..6a10776268 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -35,6 +35,9 @@ Require Export lebesgue_stieltjes_measure. (* of equivalence between emeasurable and the sigma-algebras generated open *) (* rays and closed rays. *) (* *) +(* vitali_cover A B V == V is a Vitali cover of A, here B is a *) +(* collection of non-empty closed balls *) +(* *) (******************************************************************************) Set Implicit Arguments. @@ -2137,3 +2140,299 @@ exists (B `|` C); split. Qed. End egorov. + +Definition vitali_cover {R : realType} (E : set R) I + (B : I -> set R) (D : set I) := + forall x, E x -> forall e : R, 0 < e -> exists i, + [/\ D i, B i x & (radius (B i))%:num < e]. + +Section vitali_theorem. +Context {R : realType} (A : set R) (B : nat -> set R). +Hypothesis is_ballB : forall i, is_ball (B i). +Hypothesis B0 : forall i, (0 < (radius (B i))%:num)%R. +Notation mu := (@lebesgue_measure R). +Local Open Scope ereal_scope. + +Lemma vitali_theorem (V : set nat) : vitali_cover A B V -> + exists D, [/\ countable D, D `<=` V, trivIset D (closure \o B) & + mu (A `\` \bigcup_(k in D) closure (B k)) = 0]. +Proof. +move=> ABV. +wlog VB1 : V ABV / forall i, V i -> ((radius (B i))%:num <= 1)%R. + move=> wlg. + pose V' := V `\` [set i | (radius (B i))%:num > 1]%R. + have : vitali_cover A B V'. + move=> x Ax e e0. + have : (0 < minr e 1)%R by rewrite lt_minr// e0/=. + move/(ABV x Ax) => [i [Vi ix ie]]. + exists i; split => //. + - split => //=; rewrite ltNge; apply/negP/negPn. + by rewrite (le_trans (ltW ie))// le_minl lexx orbT. + - by rewrite (lt_le_trans ie)// le_minl lexx. + move/wlg. + have V'B1 i : V' i -> ((radius (B i))%:num <= 1)%R. + by move=> [Vi /=]; rewrite ltNge => /negP/negPn. + move/(_ V'B1) => [D [cD DV' tD h]]. + by exists D; split => //; apply: (subset_trans DV') => ? []. +have [D [cD DV tDB Dintersect]] := vitali_lemma_infinite is_ballB B0 VB1. +exists D; split => //. +pose Z r := (A `\` \bigcup_(k in D) closure (B k)) `&` ball (0%R : R^o) r. +suff: forall r : {posnum R}, mu (Z r%:num) = 0. + move=> Zr; have {}Zr n : mu (Z n%:R) = 0. + move: n => [|n]; first by rewrite /Z (ball0 _ _).2// setI0 measure0. + by rewrite (Zr (PosNum (ltr0Sn _ n))). + set F := fun n => Z n%:R. + have : mu (\bigcup_n F n) <= \sum_(i n _; rewrite /F Zr. + rewrite /F -setI_bigcupr (_ : \bigcup__ _ = setT) ?setIT//. + by rewrite le_eqVlt ltNge measure_ge0 orbF => /eqP. + apply/seteqP; split => // x _. + have [x0|x0] := ltP 0%R x. + exists `|ceil x|.+1 => //. + rewrite /ball /= sub0r normrN gtr0_norm// (le_lt_trans (ceil_ge _))//. + by rewrite -natr1 natr_absz -abszE gtz0_abs// ?ceil_gt0// ltr_spaddr. + exists `|ceil (- x)|.+1 => //. + rewrite /ball /= sub0r normrN ler0_norm// (le_lt_trans (ceil_ge _))//. + rewrite -natr1 natr_absz -abszE gez0_abs ?ceil_ge0// 1?ler_oppr ?oppr0//. + by rewrite ltr_spaddr. +move=> r. +pose E := [set i | D i /\ closure (B i) `&` ball (0%R : R^o) r%:num !=set0]. +pose F := vitali_collection_partition B E 1. +have E_partition : E = \bigcup_n (F n). + by rewrite -cover_vitali_collection_partition// => i [] /DV /VB1. +have EBr2 n : E n -> closure (B n) `<=` (ball (0 : R^o) (r%:num + 2))%R. + move=> [Dn] [x] => -[Bnx rx] y /= Bny. + move: rx; rewrite /ball /= !sub0r !normrN => rx. + rewrite -(subrK x y) (le_lt_trans (ler_norm_add _ _))//. + rewrite addrC ltr_le_add// -(subrK (cpoint (B n)) y) -(addrA (y - _)%R). + rewrite (le_trans (ler_norm_add _ _))// (_ : 2 = 1 + 1)%R// ler_add//. + rewrite distrC; have := is_ball_closureP (is_ballB n) Bny. + by move=> /le_trans; apply; rewrite VB1//; exact: DV. + have := is_ball_closureP (is_ballB n) Bnx. + by move=> /le_trans; apply; rewrite VB1//; exact: DV. +have {}EBr2 : \esum_(i in E) mu (closure (B i)) <= + mu (ball (0 : R^o) (r%:num + 2))%R. + rewrite -(set_mem_set E) -nneseries_esum// -measure_bigcup//; last 2 first. + by move=> *; rewrite is_ball_closure//; exact: measurable_closed_ball. + by apply: sub_trivIset tDB => ? []. + apply/le_measure; rewrite ?inE; [|exact: measurable_ball|exact: bigcup_sub]. + apply: bigcup_measurable => *. + by rewrite is_ball_closure//; exact: measurable_closed_ball. +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. + have MC : (M%:R * (1 / (2 ^ i.+1)%:R))%:E <= + mu (\bigcup_(j in [set` C]) closure (B j)). + rewrite (measure_bigcup [the measure _ _ of mu] [set` C])//; last 2 first. + by move=> ? _; rewrite is_ball_closure//; exact: measurable_closed_ball. + by apply: sub_trivIset tDB; by apply: (subset_trans CsubFi) => x [[]]. + rewrite /= nneseries_esum//= set_mem_set// esum_fset// fsbig_finite//=. + rewrite set_fsetK. + apply: (@le_trans _ _ (\sum_(i0 <- C) (1 / (2 ^ i.+1)%:R)%:E)). + under eq_bigr do rewrite -(mul1r (_ / _)) EFinM. + rewrite -ge0_sume_distrl// EFinM lee_wpmul2r// sumEFin lee_fin. + by rewrite -(natr_sum _ _ _ (cst 1%N)) ler_nat -card_fset_sum1. + rewrite big_seq_cond [in leRHS]big_seq_cond; apply: lee_sum => // j. + rewrite andbT => /CsubFi[_ /andP[+ _]]. + rewrite -lte_fin => /ltW/le_trans; apply. + rewrite is_ball_closure// lebesgue_measure_closed_ball// lee_fin mulr2n. + by rewrite ler_addr. + have CFi : mu (\bigcup_(j in [set` C]) closure (B j)) <= + mu (\bigcup_(j in F i) closure (B j)). + apply: le_measure => //; rewrite ?inE. + - rewrite bigcup_fset; apply: bigsetU_measurable => *. + by rewrite is_ball_closure//; exact: measurable_closed_ball. + - apply: bigcup_measurable => *. + by rewrite is_ball_closure//; exact: measurable_closed_ball. + - apply: bigcup_sub => j Cj. + exact/(@bigcup_sup _ _ _ _ (closure \o B))/CsubFi. + have Fir2 : mu (\bigcup_(j in F i) closure (B j)) <= + mu (ball (0 : R^o) (r%:num + 2))%R. + rewrite (le_trans _ EBr2)// -(set_mem_set E) -nneseries_esum //. + rewrite E_partition -measure_bigcup//=; last 2 first. + by move=> *; rewrite is_ball_closure//; exact: measurable_closed_ball. + apply: trivIset_bigcup => //. + by move=> n; apply: sub_trivIset tDB => ? [[]]. + by move=> n m i0 j nm [[Di0 _] _] [[Dj _] _]; exact: tDB. + apply: le_measure; rewrite ?inE. + - apply: bigcup_measurable => *; rewrite is_ball_closure//. + exact: measurable_closed_ball. + - apply: bigcup_measurable => *; rewrite is_ball_closure//. + exact: measurable_closed_ball. + - by move=> /= x [n Fni Bnx]; exists n => //; exists i. + have {CFi Fir2} := le_trans MC (le_trans CFi Fir2). + apply/negP; rewrite -ltNge lebesgue_measure_ball// lte_fin. + rewrite -(natr1 _ `| _ |%N) natr_absz ger0_norm ?ceil_ge0// -ltr_pdivr_mulr//. + by rewrite -ltr_subl_addr (lt_le_trans _ (ceil_ge _))// ltr_subl_addr ltr_addl. +have mur2_fin_num_ : mu (ball (0 : R^o) (r%:num + 2))%R < +oo. + by rewrite lebesgue_measure_ball// ltry. +have FE : \sum_(n //. + - move=> i; apply: bigcup_measurable => *. + by rewrite is_ball_closure//; exact: measurable_closed_ball. + - apply: trivIsetT_bigcup => //. + apply/trivIsetP => i j _ _ ij. + by apply: disjoint_vitali_collection_partition => // k -[] /DV /VB1. + by rewrite -E_partition; apply: sub_trivIset tDB => x []. + - rewrite -bigcup_bigcup; apply: bigcup_measurable => k _. + by rewrite is_ball_closure//; exact: measurable_closed_ball. + apply: (@eq_eseriesr _ (fun n => mu (\bigcup_(i in F n) closure (B i)))). + move=> i _; rewrite bigcup_mkcond measure_semi_bigcup//; last 3 first. + move=> j; case: ifPn => // _. + by rewrite is_ball_closure//; exact: measurable_closed_ball. + by apply/(trivIset_mkcond _ _).1; apply: sub_trivIset tDB => x [[]]. + rewrite -bigcup_mkcond; apply: bigcup_measurable => k _. + by rewrite is_ball_closure//; exact: measurable_closed_ball. + rewrite esum_mkcond//= nneseries_esum// -fun_true//=. + 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 mu (\bigcup_(i in F k) closure (B i)))) => i _. + rewrite measure_bigcup//=. + - by rewrite nneseries_esum// set_mem_set. + - move=> j D'ij; rewrite is_ball_closure//. + exact: measurable_closed_ball. + - by apply: sub_trivIset tDB => // x [[]]. + rewrite FE (@le_lt_trans _ _ (mu (ball (0 : R^o) (r%:num + 2))%R))//. + rewrite (le_trans _ EBr2)// measure_bigcup//=. + + by rewrite nneseries_esum// set_mem_set. + + by move=> i _; rewrite is_ball_closure//; exact: measurable_closed_ball. + + by apply: sub_trivIset tDB => // x []. + have : \sum_(N <= k \oo] --> 0. + exact: nneseries_tail_cvg. + rewrite /f /=. + move/fine_fcvg => /=. + move/(@cvgrPdist_lt _ [pseudoMetricNormedZmodType R of R^o]). + 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. + by rewrite fine_ge0//; exact: nneseries_ge0. + rewrite -lte_fin; apply: le_lt_trans. + set X : \bar R := (X in fine X). + have Xoo : X < +oo. + apply: le_lt_trans foo. + by rewrite (nneseries_split N)// lee_addr//; exact: sume_ge0. + rewrite fineK ?ge0_fin_numE//; last exact: nneseries_ge0. + apply: lee_nneseries => //; first by move=> i _; exact: esum_ge0. + move=> n Nn; rewrite measure_bigcup//=. + - by rewrite nneseries_esum// set_mem_set. + - by move=> i _; rewrite is_ball_closure//; exact: measurable_closed_ball. + - by apply: sub_trivIset tDB => x [[]]. +pose K := \bigcup_(i in `I_N) \bigcup_(j in F i) closure (B j). +have closedK : closed K. + apply: closed_bigcup => //= i iN; apply: closed_bigcup => //. + by move=> j Fij; exact: closed_closure. +have ZNF5 : Z r%:num `<=` + \bigcup_(i in ~` `I_N) \bigcup_(j in F i) closure (5%:R *` B j). + move=> z Zz. + have Kz : ~ K z. + rewrite /K => -[n /= nN [m] [[Dm _] _] Bmz]. + by case: Zz => -[_ + _]; apply; exists m. + have [i [Vi Biz Bir BiK0]] : exists i, [/\ V i, (closure (B i)) z, + (closure (B i)) `<=` ball (0%R : R^o) r%:num & + closure (B i) `&` K = set0]. + case: Zz => -[Az notDBz]; rewrite /ball/= sub0r normrN => rz. + have [d dzr zdK0] : exists2 d : {posnum R}, + (d%:num < r%:num - `|z|)%R & closed_ball z d%:num `&` K = set0. + move: rz; rewrite -subr_gt0. + move=> /(@closed_disjoint_closed_ball _ [normedModType R of R^o] + _ _ _ closedK Kz). + by case=> d drz zdK; exists d. + have N0_gt0 : (0 < d%:num / 2 :> R)%R by rewrite divr_gt0. + have [i [Vi Biz BiN0]] := ABV _ Az _ N0_gt0. + exists i; split => //. + exact: subset_closure. + move=> y Biy; rewrite /ball/= sub0r normrN -(@subrK _ (cpoint (B i)) y). + rewrite (le_lt_trans (ler_norm_add _ _))//. + rewrite (@le_lt_trans _ _ (d%:num/2 + `|cpoint (B i)|)%R)//. + rewrite ler_add2r// distrC. + have /le_trans := is_ball_closureP (is_ballB i) Biy. + by apply; exact: ltW. + rewrite -(@subrK _ z (cpoint (B i))). + rewrite (@le_lt_trans _ _ (d%:num / 2 + `|cpoint (B i) - z| + `|z|)%R)//. + by rewrite -[leRHS]addrA ler_add2l//; exact: ler_norm_add. + rewrite (@le_lt_trans _ _ (d%:num + `|z|)%R)//. + rewrite [in leRHS](splitr d%:num) -!addrA ler_add2l// ler_add2r//. + have /ltW/le_trans := is_ballP (is_ballB i) Biz. + by apply; exact: ltW. + by move: dzr; rewrite -ltr_subr_addr. + apply: subsetI_eq0 zdK0 => // y Biy. + rewrite (@closed_ballE _ [normedModType R of R^o])//= /closed_ball_/=. + rewrite -(@subrK _ (cpoint (B i)) z) -(addrA (z - _)%R). + rewrite (le_trans (ler_norm_add _ _))// [in leRHS](splitr d%:num) ler_add//. + rewrite distrC. + have /ltW/le_trans := is_ballP (is_ballB i) Biz. + by apply; exact: ltW. + have /le_trans := is_ball_closureP (is_ballB i) Biy. + by apply; exact: ltW. + have [j [Ej Bij0 Bij5]] : exists j, [/\ E j, + closure (B i) `&` closure (B j) !=set0 & + closure (B i) `<=` closure (5%:R *` B j)]. + have [j [Dj Bij0 Bij2 Bij5]] := Dintersect _ Vi. + exists j; split => //; split => //. + by move: Bij0; rewrite setIC; exact: subsetI_neq0. + have BjK : ~ (closure (B j) `<=` K). + move=> BjK; move/eqP : BiK0. + by apply/negP/set0P; move: Bij0; exact: subsetI_neq0. + have [k NK Fkj] : (\bigcup_(i in ~` `I_N) F i) j. + move: Ej; rewrite E_partition => -[k _ Fkj]. + exists k => //= kN. + by apply: BjK => x Bjx; exists k => //; exists j. + by exists k => //; exists j => //; exact: Bij5. +have {}ZNF5 : mu (Z r%:num) <= + \sum_(N <= m //. + move=> n; apply: bigcup_measurable => k _. + rewrite is_ball_closure//; first exact: measurable_closed_ball. + exact: is_scale_ball. + apply: bigcup_measurable => k _; apply: bigcup_measurable => k' _. + rewrite is_ball_closure//; first exact: measurable_closed_ball. + exact: is_scale_ball. + apply: lee_nneseries => // n _. + 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 => // _. + rewrite is_ball_closure//; first exact: measurable_closed_ball. + exact: is_scale_ball. + + apply: bigcup_measurable => k _; case: ifPn => // _. + rewrite is_ball_closure//; first exact: measurable_closed_ball. + exact: is_scale_ball. +apply/(le_trans ZNF5)/ltW. +move: F5e. +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// -nneseriesZl//. +apply: lee_nneseries => // m mFn. +rewrite is_ball_closure//; last exact: is_scale_ball. +rewrite lebesgue_measure_closed_ball// [in leRHS](ballE (is_ballB m)). +by rewrite lebesgue_measure_closed_ball// -EFinM mulrnAr radius_scale_ball. +Qed. + +End vitali_theorem. diff --git a/theories/measure.v b/theories/measure.v index 48b6813f9a..6f2af413e0 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -2620,6 +2620,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}). @@ -3403,6 +3418,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 46e95f5aeb..0681143e82 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -5847,7 +5847,7 @@ move=> /ball0 r0; apply/seteqP; split => // y. by rewrite /closed_ball r0 closure0. Qed. -Lemma closed_ballxx (R: numDomainType) (V : pseudoMetricType R) (x : V) +Lemma closed_ballxx (R : numDomainType) (V : pseudoMetricType R) (x : V) (e : R) : 0 < e -> closed_ball x e x. Proof. by move=> ?; exact/subset_closure/ballxx. Qed. @@ -5916,6 +5916,39 @@ Lemma subset_closed_ball (R : realFieldType) (V : pseudoMetricType R) (x : V) (r : R) : ball x r `<=` closed_ball x r. Proof. exact: subset_closure. Qed. +Lemma open_subball {R : realFieldType} {M : normedModType R} (A : set M) (x : M) + k : open A -> A x -> 0 < k -> + exists2 e : {posnum R}, e%:num < k & ball x e%:num `<=` A. +Proof. +move=> aA Ax k0; have : nbhs x A by rewrite nbhsE/=; exists A. +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 _ _ _ _)) => //. +by apply: le_ball; rewrite le_minl; rewrite ler_pdivr_mulr// ler_pmulr// ler1n. +Qed. + +Lemma closed_disjoint_closed_ball {R : realFieldType} {M : normedModType R} + (K : set M) z (k : R) : closed K -> ~ K z -> 0 < k -> + exists2 d : {posnum R}, d%:num < k & closed_ball z d%:num `&` K = set0. +Proof. +move=> cK Kz k0. +have [e ek zeK] : exists2 e : {posnum R}, e%:num < k & ball z e%:num `<=` ~` K. + by apply: open_subball => //; rewrite openC. +have e20 : 0 < e%:num / 2 by rewrite divr_gt0. +have e2e : e%:num / 2 < e%:num by rewrite ltr_pdivr_mulr// ltr_pmulr// ltr1n. +exists (e%:num / 2)%:pos; first by rewrite /= (lt_trans _ ek). +move/subsets_disjoint : zeK; rewrite setCK. +apply: subsetI_eq0 => //=. +have := @closed_ball_subset _ M z _ _ e20 e2e. +by rewrite closed_ballE. +Qed. +(*NB: make it a near lemma? + Lemma near_closed_disjoint_closed_ball {R : realType} {X : pseudoMetricType R} + (K : set X) z : closed K -> ~ K z -> + \forall d \near 0^'+, closed_ball z d `&` K = set0.*) + Lemma locally_compactR (R : realType) : locally_compact [set: R]. Proof. move=> x _; rewrite withinET; exists (closed_ball x 1). @@ -6322,6 +6355,16 @@ move=> k0 ballA. by rewrite [in LHS](ballE ballA) (scale_ballE _ _ k0)// radius_ball// mulr_ge0. Qed. +Lemma is_scale_ball (A : set R) (k : R) : is_ball A -> is_ball (k *` A). +Proof. +move=> Aball. +have [k0|k0] := leP 0 k. + by rewrite (ballE Aball) (scale_ballE _ _ k0); exact: is_ball_ball. +rewrite (_ : _ *` _ = set0); first exact: is_ball0. +apply/seteqP; split => // x. +by rewrite /scale_ball Aball (ball0 _ _).2// nmulr_rle0. +Qed. + End center_radius_realFieldType. Section vitali_lemma_finite. diff --git a/theories/reals.v b/theories/reals.v index b0fb595438..2762e36dc3 100644 --- a/theories/reals.v +++ b/theories/reals.v @@ -765,6 +765,10 @@ Proof. by rewrite /ceil ler_oppl -floor_ge_int// -ler_oppr mulrNz opprK. Qed. Lemma ceil_lt_int x (z : int) : (z%:~R < x) = (z < ceil x). Proof. by rewrite ltNge ceil_ge_int -ltNge. Qed. +Lemma ceilN x : ceil (- x) = - floor x. Proof. by rewrite /ceil opprK. Qed. + +Lemma floorN x : floor (- x) = - ceil x. Proof. by rewrite /ceil opprK. Qed. + End CeilTheory. (* -------------------------------------------------------------------- *) diff --git a/theories/sequences.v b/theories/sequences.v index 9f3325ebb8..14072a89ef 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -1789,8 +1789,6 @@ Lemma __deprecated__ereal_cvgD (R : realFieldType) (f g : (\bar R)^nat) a b : a +? b -> f --> a -> g --> b -> f \+ g --> a + b. Proof. exact: cvgeD. Qed. -Section nneseries_split. - Lemma __deprecated__ereal_cvgB (R : realFieldType) (f g : (\bar R)^nat) a b : a +? - b -> f --> a -> g --> b -> f \- g --> a - b. Proof. exact: cvgeB. Qed. @@ -1858,6 +1856,8 @@ rewrite ltninfty_adde_def// inE (@lt_le_trans _ _ 0)//. by apply: lime_ge => //; exact: nearW. Qed. +Section nneseries_split. + Let near_eq_lim (R : realFieldType) (f g : nat -> \bar R) : cvg g -> {near \oo, f =1 g} -> lim f = lim g. Proof. @@ -1881,6 +1881,26 @@ Unshelve. all: by end_near. Qed. End nneseries_split. +Lemma nneseries_tail_cvg (R : realType) (f : (\bar R)^nat) : + \sum_(k (forall k, 0 <= f k) -> + \sum_(N <= k \oo] --> 0. +Proof. +move=> foo f0. +have : cvg (fun n => \sum_(0 <= k < n) f k). + by apply: ereal_nondecreasing_is_cvgn; exact: lee_sum_nneg_natr. +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). + 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 big_mkord -(nneseries_split N)//; exact/eqP/esym/cvg_lim. +by rewrite ge0_adde_def//= ?inE; [exact: nneseries_ge0|exact: sume_ge0]. +Qed. + Lemma nneseriesD (R : realType) (f g : nat -> \bar R) (P : pred nat) : (forall i, P i -> 0 <= f i) -> (forall i, P i -> 0 <= g i) -> \sum_(i Date: Sat, 11 Nov 2023 20:15:02 +0900 Subject: [PATCH 2/4] replace a lemma by its near version Co-authored-by: zstone1 --- theories/lebesgue_measure.v | 13 +++++++--- theories/normedtype.v | 50 +++++++++++++++---------------------- 2 files changed, 29 insertions(+), 34 deletions(-) diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 6a10776268..5d133704ff 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -2348,10 +2348,15 @@ have ZNF5 : Z r%:num `<=` case: Zz => -[Az notDBz]; rewrite /ball/= sub0r normrN => rz. have [d dzr zdK0] : exists2 d : {posnum R}, (d%:num < r%:num - `|z|)%R & closed_ball z d%:num `&` K = set0. - move: rz; rewrite -subr_gt0. - move=> /(@closed_disjoint_closed_ball _ [normedModType R of R^o] - _ _ _ closedK Kz). - by case=> d drz zdK; exists d. + have [d/= d0 dzK] := (@closed_disjoint_closed_ball _ + [normedModType R of R^o] _ _ closedK Kz). + have rz0 : (0 < minr ((r%:num - `|z|) / 2) (d / 2))%R. + by rewrite lt_minr (divr_gt0 d0)//= andbT divr_gt0// subr_gt0. + exists (PosNum rz0) => /=. + by rewrite lt_minl ltr_pdivr_mulr// ltr_pmulr ?subr_gt0// ltr1n. + apply: dzK => //=. + rewrite sub0r normrN gtr0_norm// lt_minl (ltr_pdivr_mulr d d)//. + by rewrite ltr_pmulr// ltr1n orbT. have N0_gt0 : (0 < d%:num / 2 :> R)%R by rewrite divr_gt0. have [i [Vi Biz BiN0]] := ABV _ Az _ N0_gt0. exists i; split => //. diff --git a/theories/normedtype.v b/theories/normedtype.v index 0681143e82..d909e1e7a2 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -5916,38 +5916,28 @@ Lemma subset_closed_ball (R : realFieldType) (V : pseudoMetricType R) (x : V) (r : R) : ball x r `<=` closed_ball x r. Proof. exact: subset_closure. Qed. -Lemma open_subball {R : realFieldType} {M : normedModType R} (A : set M) (x : M) - k : open A -> A x -> 0 < k -> - exists2 e : {posnum R}, e%:num < k & ball x e%:num `<=` A. -Proof. -move=> aA Ax k0; have : nbhs x A by rewrite nbhsE/=; exists A. -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. +Lemma open_subball {R : realFieldType} {M : normedModType R} (A : set M) + (x : M) : open A -> A x -> \forall e \near 0^'+, ball x e `<=` A. +Proof. +move=> aA Ax. +have /(@nbhs_closedballP R M _ x)[r xrA]: nbhs x A by rewrite nbhsE/=; exists A. +near=> e. apply/(subset_trans _ xrA)/(subset_trans _ (@subset_closed_ball _ _ _ _)) => //. -by apply: le_ball; rewrite le_minl; rewrite ler_pdivr_mulr// ler_pmulr// ler1n. -Qed. +by apply: le_ball; near: e; apply: nbhs_right_le. +Unshelve. all: by end_near. Qed. Lemma closed_disjoint_closed_ball {R : realFieldType} {M : normedModType R} - (K : set M) z (k : R) : closed K -> ~ K z -> 0 < k -> - exists2 d : {posnum R}, d%:num < k & closed_ball z d%:num `&` K = set0. -Proof. -move=> cK Kz k0. -have [e ek zeK] : exists2 e : {posnum R}, e%:num < k & ball z e%:num `<=` ~` K. - by apply: open_subball => //; rewrite openC. -have e20 : 0 < e%:num / 2 by rewrite divr_gt0. -have e2e : e%:num / 2 < e%:num by rewrite ltr_pdivr_mulr// ltr_pmulr// ltr1n. -exists (e%:num / 2)%:pos; first by rewrite /= (lt_trans _ ek). -move/subsets_disjoint : zeK; rewrite setCK. -apply: subsetI_eq0 => //=. -have := @closed_ball_subset _ M z _ _ e20 e2e. -by rewrite closed_ballE. -Qed. -(*NB: make it a near lemma? - Lemma near_closed_disjoint_closed_ball {R : realType} {X : pseudoMetricType R} - (K : set X) z : closed K -> ~ K z -> - \forall d \near 0^'+, closed_ball z d `&` K = set0.*) + (K : set M) z : closed K -> ~ K z -> + \forall d \near 0^'+, closed_ball z d `&` K = set0. +Proof. +rewrite -openC => /open_subball /[apply]; move=> [e /= e0]. +move=> /(_ (e / 2)) /= ; rewrite sub0r normrN gtr0_norm ?divr_gt0//. +rewrite ltr_pdivr_mulr// ltr_pmulr// ltr1n => /(_ erefl isT). +move/subsets_disjoint; rewrite setCK => ze2K0. +exists (e / 2); first by rewrite /= divr_gt0. +move=> x /= + x0; rewrite sub0r normrN gtr0_norm// => xe. +by move: ze2K0; apply: subsetI_eq0 => //=; exact: closed_ball_subset. +Qed. Lemma locally_compactR (R : realType) : locally_compact [set: R]. Proof. @@ -5957,7 +5947,7 @@ by split; [apply: closed_ballR_compact | apply: closed_ball_closed]. Qed. Lemma subset_closure_half (R : realFieldType) (V : pseudoMetricType R) (x : V) - (r : R) : 0 < r -> closed_ball x (r/2) `<=` ball x r. + (r : R) : 0 < r -> closed_ball x (r / 2) `<=` ball x r. Proof. move:r => _/posnumP[r] z /(_ (ball z ((r%:num/2)%:pos)%:num)) []. exact: nbhsx_ballx. From ed779130f0cb3ebbc5ae01f4dc095e963f199531 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 11 Nov 2023 22:47:58 +0900 Subject: [PATCH 3/4] fix --- theories/lebesgue_measure.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 5d133704ff..dabc6589c2 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -2264,7 +2264,7 @@ have finite_set_F i : finite_set (F i). - by move=> /= x [n Fni Bnx]; exists n => //; exists i. have {CFi Fir2} := le_trans MC (le_trans CFi Fir2). apply/negP; rewrite -ltNge lebesgue_measure_ball// lte_fin. - rewrite -(natr1 _ `| _ |%N) natr_absz ger0_norm ?ceil_ge0// -ltr_pdivr_mulr//. + rewrite -(@natr1 _ `| _ |%N) natr_absz ger0_norm ?ceil_ge0// -ltr_pdivr_mulr//. by rewrite -ltr_subl_addr (lt_le_trans _ (ceil_ge _))// ltr_subl_addr ltr_addl. have mur2_fin_num_ : mu (ball (0 : R^o) (r%:num + 2))%R < +oo. by rewrite lebesgue_measure_ball// ltry. From c46eb2e955530a62cebeef690f6fe6a06b6d1a18 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 13 Nov 2023 10:41:26 +0900 Subject: [PATCH 4/4] fix vitali_cover, minor factorizations --- CHANGELOG_UNRELEASED.md | 5 +- theories/charge.v | 6 +- theories/lebesgue_integral.v | 4 +- theories/lebesgue_measure.v | 159 ++++++++++++++--------------------- theories/measure.v | 23 ++--- theories/normedtype.v | 34 +++++++- theories/real_interval.v | 1 - 7 files changed, 113 insertions(+), 119 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 7d64630d4c..e242107e1d 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -68,7 +68,7 @@ + definition `scale_ball`, notation notation ``` *` ``` + lemmas `sub_scale_ball`, `scale_ball1`, `sub1_scale_ball` + lemmas `ball_inj`, `radius0`, `cpoint_ball`, `radius_ball_num`, - `radius_ball`, `is_ballP`, `is_ball_ball`, `scale_ball0`, + `radius_ball`, `is_ballP`, `is_ball_ball`, `scale_ball_set0`, `ballE`, `is_ball_closure`, `scale_ballE`, `cpoint_scale_ball`, `radius_scale_ball` + lemmas `vitali_lemma_finite`, `vitali_lemma_finite_cover` @@ -122,6 +122,9 @@ - in `sequences.v`: + lemma `nneseries_tail_cvg` +- in `normedtype.v`: + + lemmas `scale_ball0`, `closure_ball`, `bigcup_ballT` + ### Changed - in `hoelder.v`: diff --git a/theories/charge.v b/theories/charge.v index ef648500cf..f1cebbc9f2 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -880,7 +880,7 @@ rewrite jordan_decomp// /jordan_pos /jordan_neg /measure_of_charge/=. rewrite /cscale/= /crestr0/= mem_set// EFinN mulN1e oppeK. have mAP : measurable (A `&` P) by exact: measurableI. suff : mu (A `&` P) = 0 by move/(nu_mu _ mAP); rewrite /crestr => ->. -by apply/eqP; rewrite eq_le measure_ge0// andbT -muA0 le_measure// inE. +by apply/eqP; rewrite -measure_le0 -muA0 le_measure// inE. Qed. Lemma jordan_neg_dominates (mu : {measure set T -> \bar R}) : @@ -892,7 +892,7 @@ rewrite /cscale/= /crestr0/= mem_set//. have mAN : measurable (A `&` N) by exact: measurableI. suff : mu (A `&` N) = 0. by move=> /(nu_mu _ mAN); rewrite /crestr => ->; rewrite mule0. -by apply/eqP; rewrite eq_le measure_ge0// andbT -muA0 le_measure// inE. +by apply/eqP; rewrite -measure_le0 -muA0 le_measure// inE. Qed. End jordan_decomposition. @@ -1361,7 +1361,7 @@ have [P [N [[mP posP] [mN negN] PNX PN0]]] := Hahn_decomposition sigma. pose AP := A `&` P. have mAP : measurable AP by exact: measurableI. have muAP_gt0 : 0 < mu AP. - rewrite lt_neqAle measure_ge0// andbT eq_sym. + rewrite lt0e measure_ge0// andbT. apply/eqP/(@contra_not _ _ (nu_mu _ mAP))/eqP; rewrite gt_eqF//. rewrite (@lt_le_trans _ _ (sigma AP))//. rewrite (@lt_le_trans _ _ (sigma A))//; last first. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index f614b61d1e..2fd8600015 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -3522,7 +3522,7 @@ move=> mf; split=> [iDf0|Df0]. exists (D `&` [set x | f x != 0]); split; [exact: emeasurable_neq| |by move=> t /= /not_implyP [Dt /eqP ft0]]. have muDf a : (0 < a)%R -> mu (D `&` [set x | a%:E <= `|f x|]) = 0. - move=> a0; apply/eqP; rewrite eq_le measure_ge0 ?andbT. + move=> a0; apply/eqP; rewrite -measure_le0. by have := le_integral_abse mu mD mf a0; rewrite iDf0 pmule_rle0 ?lte_fin. rewrite [X in mu X](_ : _ = \bigcup_n (D `&` [set x | `|f x| >= n.+1%:R^-1%:E])); last first. @@ -4333,7 +4333,7 @@ have mE j : measurable (E j). rewrite /E; apply: emeasurable_fun_le => //. by apply/(emeasurable_funD msf)/measurableT_comp => //; case: mg. have muE j : mu (E j) = 0. - apply/eqP; rewrite eq_le measure_ge0// andbT. + apply/eqP; rewrite -measure_le0. have fg0 : \int[mu]_(x in E j) (f \- g) x = 0. rewrite integralB//; last 2 first. by apply: integrableS itf => //; exact: subIsetl. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index dabc6589c2..594b396d66 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -2143,12 +2143,12 @@ End egorov. Definition vitali_cover {R : realType} (E : set R) I (B : I -> set R) (D : set I) := + (forall i, is_ball (B i)) /\ forall x, E x -> forall e : R, 0 < e -> exists i, [/\ D i, B i x & (radius (B i))%:num < e]. Section vitali_theorem. Context {R : realType} (A : set R) (B : nat -> set R). -Hypothesis is_ballB : forall i, is_ball (B i). Hypothesis B0 : forall i, (0 < (radius (B i))%:num)%R. Notation mu := (@lebesgue_measure R). Local Open Scope ereal_scope. @@ -2162,9 +2162,9 @@ wlog VB1 : V ABV / forall i, V i -> ((radius (B i))%:num <= 1)%R. move=> wlg. pose V' := V `\` [set i | (radius (B i))%:num > 1]%R. have : vitali_cover A B V'. - move=> x Ax e e0. + split; [exact: ABV.1|move=> x Ax e e0]. have : (0 < minr e 1)%R by rewrite lt_minr// e0/=. - move/(ABV x Ax) => [i [Vi ix ie]]. + move=> /(ABV.2 x Ax)[i [Vi ix ie]]. exists i; split => //. - split => //=; rewrite ltNge; apply/negP/negPn. by rewrite (le_trans (ltW ie))// le_minl lexx orbT. @@ -2172,61 +2172,53 @@ wlog VB1 : V ABV / forall i, V i -> ((radius (B i))%:num <= 1)%R. move/wlg. have V'B1 i : V' i -> ((radius (B i))%:num <= 1)%R. by move=> [Vi /=]; rewrite ltNge => /negP/negPn. - move/(_ V'B1) => [D [cD DV' tD h]]. + move=> /(_ V'B1)[D [cD DV' tD h]]. by exists D; split => //; apply: (subset_trans DV') => ? []. -have [D [cD DV tDB Dintersect]] := vitali_lemma_infinite is_ballB B0 VB1. +have [D [cD DV tDB Dintersect]] := vitali_lemma_infinite ABV.1 B0 VB1. exists D; split => //. -pose Z r := (A `\` \bigcup_(k in D) closure (B k)) `&` ball (0%R : R^o) r. +pose Z r := (A `\` \bigcup_(k in D) closure (B k)) `&` ball (0%R:R) r. suff: forall r : {posnum R}, mu (Z r%:num) = 0. move=> Zr; have {}Zr n : mu (Z n%:R) = 0. - move: n => [|n]; first by rewrite /Z (ball0 _ _).2// setI0 measure0. + move: n => [|n]; first by rewrite /Z (ball0 _ _).2// setI0. by rewrite (Zr (PosNum (ltr0Sn _ n))). set F := fun n => Z n%:R. have : mu (\bigcup_n F n) <= \sum_(i n _; rewrite /F Zr. - rewrite /F -setI_bigcupr (_ : \bigcup__ _ = setT) ?setIT//. - by rewrite le_eqVlt ltNge measure_ge0 orbF => /eqP. - apply/seteqP; split => // x _. - have [x0|x0] := ltP 0%R x. - exists `|ceil x|.+1 => //. - rewrite /ball /= sub0r normrN gtr0_norm// (le_lt_trans (ceil_ge _))//. - by rewrite -natr1 natr_absz -abszE gtz0_abs// ?ceil_gt0// ltr_spaddr. - exists `|ceil (- x)|.+1 => //. - rewrite /ball /= sub0r normrN ler0_norm// (le_lt_trans (ceil_ge _))//. - rewrite -natr1 natr_absz -abszE gez0_abs ?ceil_ge0// 1?ler_oppr ?oppr0//. - by rewrite ltr_spaddr. + by rewrite /F -setI_bigcupr bigcup_ballT setIT measure_le0 => /eqP. move=> r. -pose E := [set i | D i /\ closure (B i) `&` ball (0%R : R^o) r%:num !=set0]. +pose E := [set i | D i /\ closure (B i) `&` ball (0%R:R) r%:num !=set0]. pose F := vitali_collection_partition B E 1. have E_partition : E = \bigcup_n (F n). by rewrite -cover_vitali_collection_partition// => i [] /DV /VB1. -have EBr2 n : E n -> closure (B n) `<=` (ball (0 : R^o) (r%:num + 2))%R. +have EBr2 n : E n -> closure (B n) `<=` (ball (0:R) (r%:num + 2))%R. move=> [Dn] [x] => -[Bnx rx] y /= Bny. move: rx; rewrite /ball /= !sub0r !normrN => rx. rewrite -(subrK x y) (le_lt_trans (ler_norm_add _ _))//. rewrite addrC ltr_le_add// -(subrK (cpoint (B n)) y) -(addrA (y - _)%R). rewrite (le_trans (ler_norm_add _ _))// (_ : 2 = 1 + 1)%R// ler_add//. - rewrite distrC; have := is_ball_closureP (is_ballB n) Bny. + rewrite distrC; have := is_ball_closureP (ABV.1 n) Bny. by move=> /le_trans; apply; rewrite VB1//; exact: DV. - have := is_ball_closureP (is_ballB n) Bnx. + have := is_ball_closureP (ABV.1 n) Bnx. by move=> /le_trans; apply; rewrite VB1//; exact: DV. +have measurable_closure (C : set R) : is_ball C -> measurable (closure C). + by move=> ballC; rewrite is_ball_closure//; exact: measurable_closed_ball. +move: ABV => [is_ballB ABV]. have {}EBr2 : \esum_(i in E) mu (closure (B i)) <= - mu (ball (0 : R^o) (r%:num + 2))%R. + mu (ball (0:R) (r%:num + 2))%R. rewrite -(set_mem_set E) -nneseries_esum// -measure_bigcup//; last 2 first. - by move=> *; rewrite is_ball_closure//; exact: measurable_closed_ball. + by move=> *; exact: measurable_closure. by apply: sub_trivIset tDB => ? []. apply/le_measure; rewrite ?inE; [|exact: measurable_ball|exact: bigcup_sub]. - apply: bigcup_measurable => *. - by rewrite is_ball_closure//; exact: measurable_closed_ball. + by apply: bigcup_measurable => *; exact: measurable_closure. 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. have MC : (M%:R * (1 / (2 ^ i.+1)%:R))%:E <= mu (\bigcup_(j in [set` C]) closure (B j)). - rewrite (measure_bigcup [the measure _ _ of mu] [set` C])//; last 2 first. - by move=> ? _; rewrite is_ball_closure//; exact: measurable_closed_ball. + rewrite (measure_bigcup _ [set` C])//; last 2 first. + by move=> ? _; exact: measurable_closure. by apply: sub_trivIset tDB; by apply: (subset_trans CsubFi) => x [[]]. rewrite /= nneseries_esum//= set_mem_set// esum_fset// fsbig_finite//=. rewrite set_fsetK. @@ -2234,66 +2226,60 @@ have finite_set_F i : finite_set (F i). under eq_bigr do rewrite -(mul1r (_ / _)) EFinM. rewrite -ge0_sume_distrl// EFinM lee_wpmul2r// sumEFin lee_fin. by rewrite -(natr_sum _ _ _ (cst 1%N)) ler_nat -card_fset_sum1. - rewrite big_seq_cond [in leRHS]big_seq_cond; apply: lee_sum => // j. - rewrite andbT => /CsubFi[_ /andP[+ _]]. + rewrite big_seq [in leRHS]big_seq; apply: lee_sum => // j. + move=> /CsubFi[_ /andP[+ _]]. rewrite -lte_fin => /ltW/le_trans; apply. - rewrite is_ball_closure// lebesgue_measure_closed_ball// lee_fin mulr2n. - by rewrite ler_addr. + rewrite (is_ball_closure (is_ballB _))// lebesgue_measure_closed_ball//. + by rewrite lee_fin mulr2n ler_addr. have CFi : mu (\bigcup_(j in [set` C]) closure (B j)) <= mu (\bigcup_(j in F i) closure (B j)). apply: le_measure => //; rewrite ?inE. - rewrite bigcup_fset; apply: bigsetU_measurable => *. - by rewrite is_ball_closure//; exact: measurable_closed_ball. - - apply: bigcup_measurable => *. - by rewrite is_ball_closure//; exact: measurable_closed_ball. + exact: measurable_closure. + - by apply: bigcup_measurable => *; exact: measurable_closure. - apply: bigcup_sub => j Cj. exact/(@bigcup_sup _ _ _ _ (closure \o B))/CsubFi. have Fir2 : mu (\bigcup_(j in F i) closure (B j)) <= - mu (ball (0 : R^o) (r%:num + 2))%R. + mu (ball (0:R) (r%:num + 2))%R. rewrite (le_trans _ EBr2)// -(set_mem_set E) -nneseries_esum //. rewrite E_partition -measure_bigcup//=; last 2 first. - by move=> *; rewrite is_ball_closure//; exact: measurable_closed_ball. + by move=> ? _; exact: measurable_closure. apply: trivIset_bigcup => //. by move=> n; apply: sub_trivIset tDB => ? [[]]. by move=> n m i0 j nm [[Di0 _] _] [[Dj _] _]; exact: tDB. apply: le_measure; rewrite ?inE. - - apply: bigcup_measurable => *; rewrite is_ball_closure//. - exact: measurable_closed_ball. - - apply: bigcup_measurable => *; rewrite is_ball_closure//. - exact: measurable_closed_ball. + - by apply: bigcup_measurable => *; exact: measurable_closure. + - by apply: bigcup_measurable => *; exact: measurable_closure. - by move=> /= x [n Fni Bnx]; exists n => //; exists i. have {CFi Fir2} := le_trans MC (le_trans CFi Fir2). apply/negP; rewrite -ltNge lebesgue_measure_ball// lte_fin. rewrite -(@natr1 _ `| _ |%N) natr_absz ger0_norm ?ceil_ge0// -ltr_pdivr_mulr//. by rewrite -ltr_subl_addr (lt_le_trans _ (ceil_ge _))// ltr_subl_addr ltr_addl. -have mur2_fin_num_ : mu (ball (0 : R^o) (r%:num + 2))%R < +oo. +have mur2_fin_num_ : mu (ball (0:R) (r%:num + 2))%R < +oo. by rewrite lebesgue_measure_ball// ltry. have FE : \sum_(n //. - - move=> i; apply: bigcup_measurable => *. - by rewrite is_ball_closure//; exact: measurable_closed_ball. + - by move=> i; apply: bigcup_measurable => *; exact: measurable_closure. - apply: trivIsetT_bigcup => //. apply/trivIsetP => i j _ _ ij. by apply: disjoint_vitali_collection_partition => // k -[] /DV /VB1. by rewrite -E_partition; apply: sub_trivIset tDB => x []. - rewrite -bigcup_bigcup; apply: bigcup_measurable => k _. - by rewrite is_ball_closure//; exact: measurable_closed_ball. + exact: measurable_closure. apply: (@eq_eseriesr _ (fun n => mu (\bigcup_(i in F n) closure (B i)))). move=> i _; rewrite bigcup_mkcond measure_semi_bigcup//; last 3 first. - move=> j; case: ifPn => // _. - by rewrite is_ball_closure//; exact: measurable_closed_ball. + by move=> j; case: ifPn => // _; exact: measurable_closure. by apply/(trivIset_mkcond _ _).1; apply: sub_trivIset tDB => x [[]]. rewrite -bigcup_mkcond; apply: bigcup_measurable => k _. - by rewrite is_ball_closure//; exact: measurable_closed_ball. + exact: measurable_closure. rewrite esum_mkcond//= nneseries_esum// -fun_true//=. by under eq_esum do rewrite (fun_if mu) (measure0 [the measure _ _ of mu]). -apply/eqP; rewrite eq_le measure_ge0 andbT. +apply/eqP; rewrite -measure_le0. apply/lee_addgt0Pr => _ /posnumP[e]; rewrite add0e. -have [N F5e] : exists N, - \sum_(N <= n mu (\bigcup_(i in F k) closure (B i)))) => i _. rewrite measure_bigcup//=. - by rewrite nneseries_esum// set_mem_set. - - move=> j D'ij; rewrite is_ball_closure//. - exact: measurable_closed_ball. + - by move=> j D'ij; exact: measurable_closure. - by apply: sub_trivIset tDB => // x [[]]. - rewrite FE (@le_lt_trans _ _ (mu (ball (0 : R^o) (r%:num + 2))%R))//. + rewrite FE (@le_lt_trans _ _ (mu (ball (0 : R) (r%:num + 2))%R))//. rewrite (le_trans _ EBr2)// measure_bigcup//=. + by rewrite nneseries_esum// set_mem_set. - + by move=> i _; rewrite is_ball_closure//; exact: measurable_closed_ball. + + by move=> i _; exact: measurable_closure. + by apply: sub_trivIset tDB => // x []. have : \sum_(N <= k \oo] --> 0. exact: nneseries_tail_cvg. - rewrite /f /=. - move/fine_fcvg => /=. + rewrite /f /= => /fine_fcvg /=. move/(@cvgrPdist_lt _ [pseudoMetricNormedZmodType R of R^o]). - have : (0 < 5%:R^-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. - by rewrite fine_ge0//; exact: nneseries_ge0. + rewrite sub0r normrN ger0_norm//; last by rewrite fine_ge0// nneseries_ge0. rewrite -lte_fin; apply: le_lt_trans. set X : \bar R := (X in fine X). have Xoo : X < +oo. @@ -2330,7 +2313,7 @@ have [N F5e] : exists N, apply: lee_nneseries => //; first by move=> i _; exact: esum_ge0. move=> n Nn; rewrite measure_bigcup//=. - by rewrite nneseries_esum// set_mem_set. - - by move=> i _; rewrite is_ball_closure//; exact: measurable_closed_ball. + - by move=> i _; exact: measurable_closure. - by apply: sub_trivIset tDB => x [[]]. pose K := \bigcup_(i in `I_N) \bigcup_(j in F i) closure (B j). have closedK : closed K. @@ -2343,8 +2326,7 @@ have ZNF5 : Z r%:num `<=` rewrite /K => -[n /= nN [m] [[Dm _] _] Bmz]. by case: Zz => -[_ + _]; apply; exists m. have [i [Vi Biz Bir BiK0]] : exists i, [/\ V i, (closure (B i)) z, - (closure (B i)) `<=` ball (0%R : R^o) r%:num & - closure (B i) `&` K = set0]. + closure (B i) `<=` ball (0%R:R) r%:num & closure (B i) `&` K = set0]. case: Zz => -[Az notDBz]; rewrite /ball/= sub0r normrN => rz. have [d dzr zdK0] : exists2 d : {posnum R}, (d%:num < r%:num - `|z|)%R & closed_ball z d%:num `&` K = set0. @@ -2357,33 +2339,28 @@ have ZNF5 : Z r%:num `<=` apply: dzK => //=. rewrite sub0r normrN gtr0_norm// lt_minl (ltr_pdivr_mulr d d)//. by rewrite ltr_pmulr// ltr1n orbT. - have N0_gt0 : (0 < d%:num / 2 :> R)%R by rewrite divr_gt0. + have N0_gt0 : (0 < d%:num / 2)%R by rewrite divr_gt0. have [i [Vi Biz BiN0]] := ABV _ Az _ N0_gt0. exists i; split => //. exact: subset_closure. move=> y Biy; rewrite /ball/= sub0r normrN -(@subrK _ (cpoint (B i)) y). rewrite (le_lt_trans (ler_norm_add _ _))//. - rewrite (@le_lt_trans _ _ (d%:num/2 + `|cpoint (B i)|)%R)//. + rewrite (@le_lt_trans _ _ (d%:num / 2 + `|cpoint (B i)|)%R)//. rewrite ler_add2r// distrC. - have /le_trans := is_ball_closureP (is_ballB i) Biy. - by apply; exact: ltW. + by rewrite (le_trans (is_ball_closureP (is_ballB i) Biy))// ltW. rewrite -(@subrK _ z (cpoint (B i))). rewrite (@le_lt_trans _ _ (d%:num / 2 + `|cpoint (B i) - z| + `|z|)%R)//. by rewrite -[leRHS]addrA ler_add2l//; exact: ler_norm_add. rewrite (@le_lt_trans _ _ (d%:num + `|z|)%R)//. rewrite [in leRHS](splitr d%:num) -!addrA ler_add2l// ler_add2r//. - have /ltW/le_trans := is_ballP (is_ballB i) Biz. - by apply; exact: ltW. + by rewrite (le_trans (ltW (is_ballP (is_ballB i) Biz)))// ltW. by move: dzr; rewrite -ltr_subr_addr. apply: subsetI_eq0 zdK0 => // y Biy. rewrite (@closed_ballE _ [normedModType R of R^o])//= /closed_ball_/=. rewrite -(@subrK _ (cpoint (B i)) z) -(addrA (z - _)%R). rewrite (le_trans (ler_norm_add _ _))// [in leRHS](splitr d%:num) ler_add//. - rewrite distrC. - have /ltW/le_trans := is_ballP (is_ballB i) Biz. - by apply; exact: ltW. - have /le_trans := is_ball_closureP (is_ballB i) Biy. - by apply; exact: ltW. + by rewrite distrC (le_trans (ltW (is_ballP (is_ballB i) Biz)))// ltW. + by rewrite (le_trans (is_ball_closureP (is_ballB i) Biy))// ltW. have [j [Ej Bij0 Bij5]] : exists j, [/\ E j, closure (B i) `&` closure (B j) !=set0 & closure (B i) `<=` closure (5%:R *` B j)]. @@ -2395,8 +2372,7 @@ have ZNF5 : Z r%:num `<=` by apply/negP/set0P; move: Bij0; exact: subsetI_neq0. have [k NK Fkj] : (\bigcup_(i in ~` `I_N) F i) j. move: Ej; rewrite E_partition => -[k _ Fkj]. - exists k => //= kN. - by apply: BjK => x Bjx; exists k => //; exists j. + by exists k => //= kN; apply: BjK => x Bjx; exists k => //; exists j. by exists k => //; exists j => //; exact: Bij5. have {}ZNF5 : mu (Z r%:num) <= \sum_(N <= m //. move=> n; apply: bigcup_measurable => k _. - rewrite is_ball_closure//; first exact: measurable_closed_ball. - exact: is_scale_ball. + by apply: measurable_closure; exact: is_scale_ball. apply: bigcup_measurable => k _; apply: bigcup_measurable => k' _. - rewrite is_ball_closure//; first exact: measurable_closed_ball. - exact: is_scale_ball. + by apply: measurable_closure; exact: is_scale_ball. apply: lee_nneseries => // n _. - 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 => // _. - rewrite is_ball_closure//; first exact: measurable_closed_ball. - exact: is_scale_ball. + by apply: measurable_closure; exact: is_scale_ball. + apply: bigcup_measurable => k _; case: ifPn => // _. - rewrite is_ball_closure//; first exact: measurable_closed_ball. - exact: is_scale_ball. -apply/(le_trans ZNF5)/ltW. -move: F5e. -rewrite [in X in X -> _](@lte_pdivl_mull R 5%:R e%:num%:E) ?ltr0n//. + by apply: measurable_closure; exact: is_scale_ball. +apply/(le_trans ZNF5). +move/ltW: F5e; rewrite [in X in X -> _](@lee_pdivl_mull R 5%:R) ?ltr0n//. rewrite -nneseriesZl//; last by move=> *; exact: esum_ge0. -move/le_lt_trans; apply. -apply: lee_nneseries => //; first by move=> *; exact: esum_ge0. +apply: le_trans; apply: lee_nneseries => //; first by move=> *; exact: esum_ge0. move=> n _. rewrite -(set_mem_set (F n)) -nneseries_esum// -nneseries_esum// -nneseriesZl//. apply: lee_nneseries => // m mFn. -rewrite is_ball_closure//; last exact: is_scale_ball. -rewrite lebesgue_measure_closed_ball// [in leRHS](ballE (is_ballB m)). -by rewrite lebesgue_measure_closed_ball// -EFinM mulrnAr radius_scale_ball. +rewrite (ballE (is_ballB m))// closure_ball lebesgue_measure_closed_ball//. +rewrite scale_ballE// closure_ball lebesgue_measure_closed_ball//. +by rewrite -EFinM mulrnAr. Qed. End vitali_theorem. diff --git a/theories/measure.v b/theories/measure.v index 6f2af413e0..1dfdeecfa3 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -2483,8 +2483,8 @@ have mfD i X : X \in decomp D -> measurable (((f^-1)%FUN i).2 `&` X : set T). apply: (@le_trans _ _ (\sum_(i X /[!(andbT,in_fset_set)]; last exact: decomp_finite_set. + rewrite [leLHS]big_seq [leRHS]big_seq. + rewrite lee_sum// => X /[!in_fset_set]; last exact: decomp_finite_set. move=> XD; have Xm := decomp_measurable Dm XD. by apply: muS => // [i|]; [exact: mfD|exact: DXsub]. apply: lee_lim => /=; do ?apply: is_cvg_nneseries=> //. @@ -3038,9 +3038,7 @@ Lemma measureIr : mu (A `&` B) <= mu B. Proof. by rewrite le_measure ?inE//; apply: measurableI. Qed. Lemma subset_measure0 : A `<=` B -> mu B = 0 -> mu A = 0. -Proof. -by move=> AB B0; apply/eqP; rewrite eq_le measure_ge0// -B0 le_measure// inE. -Qed. +Proof. by move=> ? B0; apply/eqP; rewrite -measure_le0 -B0 le_measure ?inE. Qed. End content_semiRingOfSetsType. @@ -3245,8 +3243,7 @@ Variable mu : {content set T -> \bar R}. Lemma negligibleP A : measurable A -> mu.-negligible A <-> mu A = 0. Proof. move=> mA; split => [[B [mB mB0 AB]]|mA0]; last by exists A; split. -apply/eqP; rewrite eq_le measure_ge0 // andbT -mB0. -by apply: (le_measure mu) => //; rewrite in_setE. +by apply/eqP; rewrite -measure_le0 -mB0 le_measure ?inE. Qed. Lemma negligible_set0 : mu.-negligible set0. @@ -3266,8 +3263,7 @@ Lemma negligibleI A B : Proof. move=> [N [mN N0 AN]] [M [mM M0 BM]]; exists (N `&` M); split => //. - exact: measurableI. -- apply/eqP; rewrite eq_le measure_ge0 andbT -N0 le_measure// inE//. - exact: measurableI. +- by apply/eqP; rewrite -measure_le0 -N0 le_measure ?inE//; exact: measurableI. - exact: setISS. Qed. @@ -3287,8 +3283,8 @@ Lemma negligibleU A B : Proof. move=> [N [mN N0 AN]] [M [mM M0 BM]]; exists (N `|` M); split => //. - exact: measurableU. -- apply/eqP; rewrite eq_le measure_ge0 andbT. - rewrite -N0 -[leRHS]adde0 -M0 -bigsetU_bigcup2; apply: le_trans. +- apply/eqP; rewrite -measure_le0 -N0 -[leRHS]adde0 -M0 -bigsetU_bigcup2. + apply: le_trans. + apply: (@content_sub_additive _ _ _ _ _ (bigcup2 N M) 2%N) => //. * by move=> [|[|[|]]]. * apply: bigsetU_measurable => // i _; rewrite /bigcup2. @@ -3319,8 +3315,7 @@ move=> mF; exists (\bigcup_k sval (cid (mF k))); split. rewrite eseries0// => k _. have [mFk mFk0 ?] := svalP (cid (mF k)). rewrite measureD//=. - + rewrite mFk0 sub0e eqe_oppLRP oppe0. - apply/eqP; rewrite eq_le measure_ge0 andbT. + + rewrite mFk0 sub0e eqe_oppLRP oppe0; apply/eqP; rewrite -measure_le0. rewrite -[leRHS]mFk0 le_measure//= ?inE//; apply: measurableI => //. by apply: bigsetU_measurable => i _; case: cid => // A []. + by apply: bigsetU_measurable => i _; case: cid => // A []. @@ -3365,7 +3360,7 @@ Instance ae_properfilter_algebraOfSetsType d {T : algebraOfSetsType d} Proof. move=> muT; split=> [|]; last exact: ae_filter_ringOfSetsType. rewrite /almost_everywhere setC0 => /(measure_negligible measurableT). -by apply/eqP; rewrite eq_le negb_and measure_ge0 orbF -ltNge. +by move/eqP; rewrite -measure_le0 leNgt => /negP. Qed. End ae. diff --git a/theories/normedtype.v b/theories/normedtype.v index d909e1e7a2..b9a1a28c03 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -101,9 +101,10 @@ Require Import ereal reals signed topology prodnormedzmodule. (* *) (* cpoint A == the center of the set A if it is an open ball *) (* radius A == the radius of the set A if it is an open ball *) -(* radius A has type {nonneg R} *) +(* Radius A has type {nonneg R} with R a numDomainType. *) (* is_ball A == boolean predicate that holds when A is an open ball *) (* k *` A == open ball with center cpoint A and radius k * radius A *) +(* if A is an open ball and set0 o.w. *) (* vitali_collection_partition B V r n == subset of indices of V such the *) (* the ball B i has a radius between r/2^n+1 and r/2^n *) (* *) @@ -338,6 +339,18 @@ Proof. by case: V => ? [? ? ? ? ? ? []]. Qed. End pseudoMetricnormedzmodule_lemmas. +Lemma bigcup_ballT {R : realType} : \bigcup_n ball (0%R : R) n%:R = setT. +Proof. +apply/seteqP; split => // x _; have [x0|x0] := ltP 0%R x. + exists `|ceil x|.+1 => //. + rewrite /ball /= sub0r normrN gtr0_norm// (le_lt_trans (ceil_ge _))//. + by rewrite -natr1 natr_absz -abszE gtz0_abs// ?ceil_gt0// ltr_spaddr. +exists `|ceil (- x)|.+1 => //. +rewrite /ball /= sub0r normrN ler0_norm// (le_lt_trans (ceil_ge _))//. +rewrite -natr1 natr_absz -abszE gez0_abs ?ceil_ge0// 1?ler_oppr ?oppr0//. +by rewrite ltr_spaddr. +Qed. + (** neighborhoods *) Section Nbhs'. @@ -6201,6 +6214,14 @@ Proof. by move/scale_ball1 => {1}<-; apply: sub_scale_ball; rewrite ler1n. Qed. End center_radius. Notation "k *` B" := (scale_ball k B) : classical_set_scope. +Lemma scale_ball0 {R : realFieldType} (A : set R) r : (r <= 0)%R -> + r *` A = set0. +Proof. +move=> r0; apply/seteqP; split => // x. +rewrite /scale_ball; case: ifPn => // ballA. +by rewrite ((ball0 _ _).2 _)// mulr_le0_ge0. +Qed. + Section center_radius_realFieldType. Context {R : realFieldType}. Implicit Types x y r s : R. @@ -6297,7 +6318,7 @@ have [r0|/ball0 ->] := ltP 0 r; last exact: is_ball0. by apply/eqP; rewrite cpoint_ball// (radius_ball _ (ltW r0)). Qed. -Lemma scale_ball0 (k : R) : k *` set0 = set0 :> set R. +Lemma scale_ball_set0 (k : R) : k *` set0 = set0 :> set R. Proof. by rewrite /scale_ball is_ball0// radius0/= mulr0 ball0. Qed. Lemma ballE (A : set R) : is_ball A -> A = ball (cpoint A) (radius A)%:num. @@ -6319,6 +6340,13 @@ Lemma is_ball_closure (A : set R) : is_ball A -> closure A = closed_ball (cpoint A) (radius A)%:num. Proof. by move=> ballA; rewrite /closed_ball -ballE. Qed. +Lemma closure_ball (c r : R) : closure (ball c r) = closed_ball c r. +Proof. +have [r0|r0] := leP r 0. + by rewrite closed_ball0// ((ball0 _ _).2 r0) closure0. +by rewrite (is_ball_closure (is_ball_ball _ _)) cpoint_ball// radius_ball ?ltW. +Qed. + Lemma scale_ballE k x r : 0 <= k -> k *` ball x r = ball x (k * r). Proof. move=> k0; have [r0|r0] := ltP 0 r. @@ -6326,7 +6354,7 @@ move=> k0; have [r0|r0] := ltP 0 r. rewrite /scale_ball is_ball_ball//= cpoint_ball//. by rewrite (radius_ball_num _ (ltW _)). by rewrite /scale_ball is_ball_ball cpoint_ball// radius_ball_num// ltW. -rewrite ((ball0 _ _).2 r0) scale_ball0; apply/esym/ball0. +rewrite ((ball0 _ _).2 r0) scale_ball_set0; apply/esym/ball0. by rewrite mulr_ge0_le0. Qed. diff --git a/theories/real_interval.v b/theories/real_interval.v index f82b5db342..b22f52486e 100644 --- a/theories/real_interval.v +++ b/theories/real_interval.v @@ -430,4 +430,3 @@ case: b => /=. - by move/ltW; rewrite ler_norml => /andP[-> ->]. - by rewrite ltr_norml => /andP[-> /ltW->]. Qed. -