From 697cb52f3139e9689fb0eb90509ea300eb3adfcc Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 17 Jul 2023 14:59:25 +0900 Subject: [PATCH] start addressing comments by Zachary --- theories/lebesgue_measure.v | 286 ++++++++++++++++++++---------------- 1 file changed, 160 insertions(+), 126 deletions(-) diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index bc17751b72..2f76bd3125 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -2107,123 +2107,136 @@ Qed. End egorov. -Lemma properW (T : Type) (A B : set T) : A `<` B -> A `<=` B. -Proof. by case. Qed. - -Lemma properxx (T : Type) (A : set T) : ~ A `<` A. -Proof. by move=> [?]; apply. Qed. - -Section Zorn_set. -Variables (I : Type) (P : set I -> Prop). -Let T := {x : set I | P x}. +(* PR in progress *) (* NB: turning P into set (set I) and T := P does not improve much *) -Let R (A B : T) := sval A `<=` sval B. - -Lemma Zorn_set : - (forall A, total_on A R -> exists t, forall s, A s -> R s t) -> - exists t, P t /\ forall F, t `<` F -> ~ P F. -Proof. -move=> Rtot; have [| | |t tmax] := Zorn _ _ _ Rtot. +Section Zorn_subset. +Variables (T : Type) (P : set T -> Prop). +Let sigP := {x | P x}. +Let R (sA sB : sigP) := sval sA `<=` sval sB. + +Lemma Zorn_bigcup : + (forall F, total_on F R -> P (\bigcup_(x in F) sval x)) -> + exists A, P A /\ forall B, A `<` B -> ~ P B. +Proof. +move=> totR. +have {}totR F : total_on F R -> exists sB, forall sA, F sA -> R sA sB. + by move=> FR; exists (exist _ _ (totR _ FR)) => sA FsA; exact: bigcup_sup. +have [| | |sA sAmax] := Zorn _ _ _ totR. - by move=> ?; exact: subset_refl. - by move=> ? ? ?; exact: subset_trans. -- move=> [s Ps] [t Pt]; rewrite /R /= => st ts. - have {st ts}s_t : s = t by apply/seteqP. - by rewrite s_t in Ps Pt *; by rewrite (Prop_irrelevance Ps). -- exists (sval t); case: t => t Pt in tmax *; split => // F tF PF. - have [Ft] := tmax (exist _ F PF) (properW tF). - by move: tF; rewrite Ft; exact: properxx. +- by move=> [A PA] [B PB]; rewrite /R /= => AB BA; exact/eq_exist/seteqP. +- exists (sval sA); case: sA => A PA in sAmax *; split => //= B AB PB. + have [BA] := sAmax (exist _ B PB) (properW AB). + by move: AB; rewrite BA; exact: properxx. Qed. -End Zorn_set. +End Zorn_subset. -Section Zorn_incl. -Variables (I : Type) (P : set I -> Prop). -Let T := { x : set I | P x }. -Definition R (A B : T) := sval A `<=` sval B. +Section ball_extra. +Variable R : realType. -Lemma Zorn_incl : - (forall A, total_on A R -> P (\bigcup_(x in A) sval x)) -> - exists t, P t /\ forall F, t `<` F -> ~ P F. +Lemma ball_itv (x r : R) : (ball x r = `]x - r, x + r[%classic)%R. Proof. -move=> H. -have {}H A : total_on A R -> exists t, forall s, A s -> R s t. - by move=> c; exists (exist P _ (H _ c)) => s As; exact: bigcup_sup. -exact: Zorn_set H. +by apply/seteqP; split => y; rewrite /ball/= in_itv/= ltr_distlC. Qed. -End Zorn_incl. +Lemma ball0 (x : R) : ball x 0 = set0. +Proof. by rewrite ball_itv subr0 addr0 set_itvoo0. Qed. -Section closed_balls. -Variable R : realType. +Lemma measurable_ball (x : R^o) e : measurable (ball x e). +Proof. by rewrite ball_itv; exact: measurable_itv. Qed. -Lemma ball_itv (x r : R) : (ball x r = `]x - r, x + r[%classic)%R. +Lemma lebesgue_measure_ball (x r : R) : (0 <= r)%R -> + lebesgue_measure (ball x r) = (r *+ 2)%:E. Proof. -by apply/seteqP; split => y; rewrite /ball/= in_itv/= ltr_distlC. +rewrite le_eqVlt => /orP[/eqP <-|r0]; first by rewrite ball0 measure0 mul0rn. +rewrite ball_itv lebesgue_measure_itv hlength_itv/=. +rewrite lte_fin ltr_subl_addr -addrA ltr_addl addr_gt0 //. +by rewrite -EFinD addrAC opprD opprK addrA subrr add0r -mulr2n. Qed. -Lemma measurable_ball x e : measurable (@ball _ [pseudoMetricType R of R^o] x e). -Proof. by rewrite ball_itv; exact: measurable_itv. Qed. +End ball_extra. -Definition oball (c : R * {posnum R}) k := ball c.1 (k * c.2%:num). +Section scale_ball. +Variable R : realType. -(* NB: see also closed_ball *) -Definition cball k (c : R * {posnum R}) := [set x | `|c.1 - x| <= k * c.2%:num]. +Definition scale_ball k (c : R * {posnum R}) := + ball c.1 (k * c.2%:num). -Lemma trivIset_bigcup_cball (I : eqType) (B : I -> R * {posnum R}) - (D : nat -> set I) k : - (forall n, trivIset (D n) (cball k \o B)) -> - (forall n m i j, i != j -> n != m -> D n i -> D m j -> - cball k (B i) `&` cball k (B j) = set0) -> - trivIset (\bigcup_k D k) (cball k \o B). +Definition scale_cball k (c : R * {posnum R}) := + [set x | `|c.1 - x| <= k * c.2%:num]. + +Lemma scale_cball0 c : scale_cball 0 c = [set c.1]. Proof. -move=> tB H; apply/trivIsetP => i j [n _ Dni] [m _ Dmi] ij. -have [nm|nm] := eqVneq n m. - by have /trivIsetP := tB n; apply => //; rewrite nm. -exact: (H _ _ _ _ _ nm). +by apply/seteqP; split => // x; + rewrite /scale_cball/= mul0r normr_le0 subr_eq0 eq_sym => /eqP. Qed. -Lemma cball_itv k c : - (cball k c = `[c.1 - k * c.2%:num, c.1 + k * c.2%:num]%classic)%R. -Proof. by apply/seteqP; split => y; rewrite /cball/= in_itv/= ler_distlC. Qed. +Lemma scale_cball_neq0 k (c : R * {posnum R}) : 0 <= k -> scale_cball k c !=set0. +Proof. by exists c.1; rewrite /= /scale_cball /= subrr normr0 mulr_ge0. Qed. -Lemma measurable_cball k c : measurable (cball k c). -Proof. by rewrite cball_itv; exact: measurable_itv. Qed. +Lemma trivIset_bigcup_scale_cball (I : Type) (B : I -> R * {posnum R}) + (D : nat -> set I) k : + (forall n, trivIset (D n) (scale_cball k \o B)) -> + (forall n m i j, n != m -> D n i -> D m j -> + scale_cball k (B i) `&` scale_cball k (B j) !=set0 -> i = j) -> + trivIset (\bigcup_k D k) (scale_cball k \o B). +Proof. +move=> tB H; move=> i j [n _ Dni] [m _ Dmi] ij. +have [nm|nm] := eqVneq n m; first by apply: (tB m) => //; rewrite -nm. +exact: (H _ _ _ _ nm). +Qed. -Lemma cball_neq0 k (B : R * {posnum R}) : 0 <= k -> cball k B !=set0. -Proof. by exists B.1; rewrite /= /cball /= subrr normr0 mulr_ge0. Qed. +Lemma scale_cball_itv k c : + (scale_cball k c = `[c.1 - k * c.2%:num, c.1 + k * c.2%:num]%classic)%R. +Proof. by apply/seteqP; split => y; rewrite /scale_cball/= in_itv/= ler_distlC. Qed. -Lemma interior_cball_neq0 (B : R * {posnum R}) k : 0 < k -> (cball k B)^° !=set0. +Lemma interior_scale_cball_neq0 (B : R * {posnum R}) k : 0 < k -> + (scale_cball k B)^° !=set0. Proof. move=> k0. -exists B.1; rewrite /interior nbhsE/=; exists (oball B k). +exists B.1; rewrite /interior nbhsE/=; exists (scale_ball k B). - split. - apply: (@ball_open _ [normedModType R of R^o] B.1 _). - by rewrite mulr_gt0. - by rewrite /oball; apply: ballxx; rewrite mulr_gt0. + by apply: (ball_open (B.1 : R^o)); rewrite mulr_gt0. + by rewrite /scale_ball; apply: ballxx; rewrite mulr_gt0. - by move=> x /ltW/le_trans; exact. Qed. -(* NB: can be generalized *) +Lemma measurable_scale_cball k c : measurable (scale_cball k c). +Proof. by rewrite scale_cball_itv; exact: measurable_itv. Qed. + +Lemma measure_scale_cballE k c : 0 <= k -> + lebesgue_measure (scale_cball k c) = (k%:E * ((c.2)%:num *+ 2)%:E)%E. +Proof. +rewrite le_eqVlt => /predU1P[<-|]. + by rewrite mul0e scale_cball0 lebesgue_measure_set1. +move=> k0. +rewrite scale_cball_itv lebesgue_measure_itv hlength_itv/=. +rewrite lte_fin -ltr_subl_addl addrAC subrr add0r gtr_opp// ?mulr_gt0//. +rewrite -EFinD; congr (_%:E). +by rewrite opprB addrAC addrCA subrr addr0 -mulrDr -mulr2n. +Qed. + +Lemma measure_scale_cball k c : 0 <= k -> + lebesgue_measure (scale_cball k c) = (k%:E * lebesgue_measure (scale_cball 1 c))%E. +Proof. by move=> k0; rewrite !measure_scale_cballE// mul1e. Qed. + +(* NB: this can be generalized *) Lemma separated_countable (I : Type) (B : I -> R * {posnum R}) (D : set I) k : 0 < k -> - trivIset D (cball k \o B) -> countable D. + trivIset D (scale_cball k \o B) -> countable D. Proof. move=> k0 tB; have [f fB] : - {f : I -> rat & forall i, (D i /\ ratr (f i) \in cball k (B i)) \/ ~ D i}. - apply: (@choice _ _ (fun x y => (D x /\ ratr y \in cball k (B x)) \/ ~ D x)). - move=> i. - have [Di|Di] := pselect (D i); last by exists 0; right. - have [x [Bix [q _ qx]]] := @dense_rat R (interior (cball k (B i))) - (interior_cball_neq0 _ k0) (open_interior _). - by exists q; left; split => //; rewrite qx inE; exact: interior_subset. + {f : I -> rat & forall i, D i -> ratr (f i) \in scale_cball k (B i)}. + apply: (@choice _ _ (fun x y => D x -> ratr y \in scale_cball k (B x))) => i. + have [r [Bir [q _ qr]]] := dense_rat (interior_scale_cball_neq0 _ k0) + (open_interior (scale_cball k (B i))). + by exists q => Di; rewrite qr inE; exact: interior_subset. have inj_f : {in D &, injective f}. - move=> x y /[!inE] xD yD /(congr1 (@ratr R))h. - have H : ratr (f x) \in cball k (B x) `&` cball k (B y). - rewrite !inE; split. - - by have [[_]|//] := fB x; rewrite inE. - - by have [[_]|//] := fB y ; rewrite h inE. - apply: (tB x y xD yD); exists (ratr (f x)). - exact: set_mem. + move=> i j /[!inE] Di Dj /(congr1 ratr) ratrij. + have ? : ratr (f i) \in scale_cball k (B i) `&` scale_cball k (B j). + by rewrite in_setI fB//= ratrij fB. + by apply/(tB _ _ Di Dj); exists (ratr (f i)); exact: set_mem. apply/pcard_injP; have /card_bijP/cid[g bijg] := card_rat. pose nat_of_rat (q : rat) : nat := set_val (g (to_setT q)). have inj_nat_of_rat : injective nat_of_rat. @@ -2232,19 +2245,19 @@ have inj_nat_of_rat : injective nat_of_rat. by exists (nat_of_rat \o f) => i j Di Dj /inj_nat_of_rat/inj_f; exact. Qed. -End closed_balls. +End scale_ball. Section maximal_disjoint_subcollection. -Context {R : realType} {I : Type}. +Context {I : Type} {R : realType}. Variables (B : I -> R * {posnum R}). Definition maximal_disjoint_subcollection (E D : set I) := - [/\ E `<=` D, trivIset E (cball 1 \o B) & - forall F, E `<` F -> F `<=` D -> ~ trivIset F (cball 1 \o B) ]. + [/\ E `<=` D, trivIset E (scale_cball 1 \o B) & + forall F, E `<` F -> F `<=` D -> ~ trivIset F (scale_cball 1 \o B) ]. Variable D : set I. -Let P := fun X => X `<=` D /\ trivIset X (cball 1 \o B). +Let P := fun X => X `<=` D /\ trivIset X (scale_cball 1 \o B). Let T := {x : set I | P x}. Let H (A : set T) : @@ -2258,7 +2271,7 @@ Qed. Lemma ex_maximal_disjoint : { E | maximal_disjoint_subcollection E D }. Proof. -have /cid[E [[ED tEB] maxE]] := @Zorn_incl _ P H. +have /cid[E [[ED tEB] maxE]] := @Zorn_bigcup _ P H. by exists E; split => // F /maxE + FD; exact: contra_not. Qed. @@ -2275,17 +2288,19 @@ rewrite -[X in (_ <= X)%N]prednK ?expn_gt0// -[X in (_ <= X)%N]addn1 leq_add2r. by rewrite (leq_trans h2)// -subn1 leq_subRL ?expn_gt0// add1n ltn_exp2l. Qed. -Section vitali_lemma. +Section collection_partition. Context {R : realType} {I : eqType}. Variables (B : I -> R * {posnum R}) (V : set I) (r : R). + +Definition collection_partition n := + [set i | V i /\ r / (2 ^ n.+1)%:R < (B i).2%:num <= r / (2 ^ n)%:R]. + Hypothesis VBr : forall i, V i -> (B i).2%:num <= r. -Let r_gt0 i0 : V i0 -> 0 < r. +Lemma r_gt0 i0 : V i0 -> 0 < r. Proof. move=> Vi0; by rewrite (lt_le_trans _ (VBr Vi0)). Qed. -Let B_ n := [set i | V i /\ r / (2 ^ n.+1)%:R < (B i).2%:num <= r / (2 ^ n)%:R]. - -Let B_cover (i : I) : V i -> exists n, (B_ n) i. +Lemma ex_collection_partition (i : I) : V i -> exists n, (collection_partition n) i. Proof. move=> Vi; pose f := floor (r / ((B i).2)%:num). have f_ge0 : 0 <= f by rewrite floor_ge0// divr_ge0// ltW// (r_gt0 Vi). @@ -2307,8 +2322,17 @@ rewrite (le_trans mf)// prednK//; last by rewrite absz_gt0 eq_sym. by rewrite natr_absz// ger0_norm// floor_le. Qed. -(* NB: not used *) -Let B_disjoint n m : n != m -> B_ n `&` B_ m = set0. +Lemma cover_collection_partition : V = \bigcup_n collection_partition n. +Proof. +apply/seteqP; split. + move=> i Vi. + have [n Hn] := ex_collection_partition Vi. + by exists n. +by move=> i [n _] []. +Qed. + +Lemma disjoint_collection_partition n m : n != m -> + collection_partition n `&` collection_partition m = set0. Proof. rewrite neq_lt => /orP[] nm. apply/seteqP; split => // i [] [Vi] /andP[rnB _] [_ /andP[_]]. @@ -2316,29 +2340,38 @@ rewrite neq_lt => /orP[] nm. rewrite ltf_pinv ?posrE ?ltr0n ?expn_gt0// ltr_nat. by move/ltn_pexp2l => /(_ isT); rewrite ltnNge => /negP; apply. rewrite setIC; apply/seteqP; split => // i []. -rewrite /B_ /= => -[Vi] /andP[rmB _] [_ /andP[_]]. +rewrite /cover_partition /= => -[Vi] /andP[rmB _] [_ /andP[_]]. move/(lt_le_trans rmB); rewrite ltr_pmul2l//; last by rewrite (r_gt0 Vi). rewrite ltf_pinv ?posrE ?ltr0n ?expn_gt0// ltr_nat. by move/ltn_pexp2l => /(_ isT); rewrite ltnNge => /negP; apply. Qed. -Definition H_ n U := [set i | B_ n i /\ - forall s, U s -> i != s -> cball 1 (B i) `&` cball 1 (B s) = set0]. +End collection_partition. + +Section vitali_lemma. +Context {R : realType} {I : eqType}. +Variables (B : I -> R * {posnum R}) (V : set I) (r : R). +Hypothesis VBr : forall i, V i -> (B i).2%:num <= r. + +Let B_ n := collection_partition B V r n. + +Let H_ n U := [set i | B_ n i /\ + forall s, U s -> i != s -> scale_cball 1 (B i) `&` scale_cball 1 (B s) = set0]. -Definition elt_prop (x : set I * nat * set I) := +Let elt_prop (x : set I * nat * set I) := x.1.1 `<=` V /\ maximal_disjoint_subcollection B x.1.1 (H_ x.1.2 x.2). -Definition elt_type := {x | elt_prop x}. +Let elt_type := {x | elt_prop x}. -Definition Rel (x y : elt_type) := +Let Rel (x y : elt_type) := (sval y).2 = (sval x).2 `|` (sval x).1.1 /\ (sval x).1.2.+1 = (sval y).1.2. Lemma vitali_lemma : { D : set I | [/\ countable D, - D `<=` V, trivIset D (cball 1 \o B) & + D `<=` V, trivIset D (scale_cball 1 \o B) & forall i, V i -> exists j, [/\ D j, - cball 1 (B i) `&` cball 1 (B j) !=set0, + scale_cball 1 (B i) `&` scale_cball 1 (B j) !=set0, (B j).2%:num >= (B i).2%:num / 2 & - cball 1 (B i) `<=` cball 5 (B j)] ] }. + scale_cball 1 (B i) `<=` scale_cball 5 (B j)] ] }. Proof. have [D0 [D0B0 tD0 maxD0]] := ex_maximal_disjoint B (B_ O). have H0 : elt_prop (D0, 0%N, set0). @@ -2375,42 +2408,43 @@ exists (\bigcup_k D k); split. - move=> i [n _ Dni]. have [+ _ _] := maxD n. by move/(_ _ Dni) => [[]]. -- apply: trivIset_bigcup_cball => m; first by have [_ ?] := maxD m. - move=> n i j ij nm Dmi Dnj. - wlog : i j ij n m nm Dmi Dnj / (m < n)%N. - move=> wlg. - move: nm; rewrite neq_lt => /orP[mn|nm]. - by rewrite (wlg i j ij n m)// ?lt_eqF. - by rewrite setIC (wlg j i _ m n)//; [rewrite eq_sym|rewrite lt_eqF]. - move=> mn. +- apply: trivIset_bigcup_scale_cball => m; first by have [_ ?] := maxD m. + move=> n i j mn Dmi Dnj. + wlog : i j n m mn Dmi Dnj / (m < n)%N. + move=> wlg ij. + move: mn; rewrite neq_lt => /orP[mn|nm]. + by rewrite (wlg i j n m)// ?lt_eqF. + by rewrite (wlg j i m n)// ?lt_eqF// setIC. + move=> {}mn. have [_ {}H] := DH _ _ Dnj. - by rewrite setIC; apply H => //; [exists m|rewrite eq_sym]. + move=> /set0P/eqP; apply: contra_notP => /eqP. + by rewrite eq_sym setIC; apply: H => //; exists m. move=> i Vi. -have [n Bni] := B_cover Vi. +have [n Bni] := ex_collection_partition VBr Vi. have [[j Dj BiBj]|] := pselect (exists2 j, (\bigcup_(i < n.+1) D i) j & - cball 1 (B i) `&` cball 1 (B j) !=set0); last first. + scale_cball 1 (B i) `&` scale_cball 1 (B j) !=set0); last first. move/forall2NP => H. have {}H j : (\bigcup_(i < n.+1) D i) j -> - cball 1 (B i) `&` cball 1 (B j) = set0. + scale_cball 1 (B i) `&` scale_cball 1 (B j) = set0. by have [//|/set0P/negP/negPn/eqP] := H j. have H_i : (H_ n (\bigcup_(i < n) D i)) i. split => // s Hs si; apply: H => //. by move: Hs => [m /= nm Dms]; exists m => //=; rewrite (ltn_trans nm). - have Dn_Bi j : D n j -> cball 1 (B i) `&` cball 1 (B j) = set0. + have Dn_Bi j : D n j -> scale_cball 1 (B i) `&` scale_cball 1 (B j) = set0. by move=> Dnj; apply: H; exists n => //=. have [Dni|Dni] := pselect (D n i). have := Dn_Bi _ Dni. rewrite setIid => /eqP/negPn/negP/set0P. - by have := @cball_neq0 _ 1 (B i) ler01. - have not_tB : ~ trivIset (D n `|` [set i]) (cball 1 \o B). + by have := @scale_cball_neq0 _ 1 (B i) ler01. + have not_tB : ~ trivIset (D n `|` [set i]) (scale_cball 1 \o B). have [_ _] := maxD n. apply. split; first exact: subsetUl. by move=> x; apply/Dni; apply: x; right. by rewrite subUset; split => //; rewrite sub1set inE. have [p [q [pq Dnpi Dnqi pq0]]] : exists p q, [/\ p != q, - D n p \/ p = i, D n q \/ q = i & cball 1 (B p) `&` cball 1 (B q) !=set0]. + D n p \/ p = i, D n q \/ q = i & scale_cball 1 (B p) `&` scale_cball 1 (B q) !=set0]. move/trivIsetP : not_tB => /existsNP[p not_tB]; exists p. move/existsNP : not_tB => [q not_tB]; exists q. move/not_implyP : not_tB => [Dnip]. @@ -2436,7 +2470,7 @@ have Bjrn : (B j).2%:num > r / (2 ^ n.+1)%:R. have [+ _ _] := maxD m. by move/(_ _ Dmk) => -[Bmk] _; exists m. move/(_ _ Dj) => [m/= mn1] [_] /andP[+ _]. - apply: le_lt_trans; rewrite ler_pmul2l//; last by rewrite (r_gt0 Vi). + apply: le_lt_trans; rewrite ler_pmul2l//; last by rewrite (r_gt0 VBr Vi). by rewrite lef_pinv// ?posrE ?ltr0n ?expn_gt0// ler_nat leq_pexp2l. exists j; split => //. - by case: Dj => m /= mn Dm; exists m. @@ -2446,11 +2480,11 @@ exists j; split => //. apply: (@le_trans _ _ (2 * (B i).2%:num + (B j).2%:num)). case: BiBj => y [Biy Bjy]. rewrite (le_trans (ler_dist_add y _ _))// [in leRHS]addrC ler_add//. - by move: Bjy; rewrite /cball/= mul1r. + by move: Bjy; rewrite /scale_cball/= mul1r. rewrite (le_trans (ler_dist_add (B i).1 _ _))//. rewrite (_ : 2 = 1 + 1)// mulrDl !mul1r// ler_add//; last first. - by move: Bix; rewrite /cball/= mul1r. - by move: Biy; rewrite /cball/= mul1r distrC. + by move: Bix; rewrite /scale_cball/= mul1r. + by move: Biy; rewrite /scale_cball/= mul1r distrC. rewrite -ler_subr_addr// (_ : 5 = 4 + 1); last by rewrite natr1. rewrite mulrDl mul1r addrK (_ : 4 = 2 * 2); last by rewrite -natrM. rewrite -mulrA ler_pmul2l//. @@ -2459,8 +2493,8 @@ exists j; split => //. Qed. Let vitali_lemma_corollary : { D : set I | [/\ countable D, - D `<=` V, trivIset D (cball 1 \o B) & - cover V (cball 1 \o B) `<=` cover D (cball 5 \o B)] }. + D `<=` V, trivIset D (scale_cball 1 \o B) & + cover V (scale_cball 1 \o B) `<=` cover D (scale_cball 5 \o B)] }. Proof. have [D [cD DV tD maxD]] := vitali_lemma. exists D; split => // x [i Vi] cBix/=.