From 94d93cc5dda24d1a6d5f6cdbe7427f82195e31e6 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Thu, 9 Nov 2023 20:40:10 +0900 Subject: [PATCH] tentative formalization of Vitali's lemma (#973) * tentative formalization of Vitali's lemmas --- CHANGELOG_UNRELEASED.md | 35 +++ classical/classical_sets.v | 47 +++- classical/mathcomp_extra.v | 10 + theories/lebesgue_measure.v | 38 ++- theories/normedtype.v | 534 ++++++++++++++++++++++++++++++++++++ theories/topology.v | 28 ++ 6 files changed, 685 insertions(+), 7 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 59c48b1a3..092b3bf78 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -49,6 +49,39 @@ - in `lebesgue_integral.v`: + lemma `abse_integralP` +- in `classical_sets.v`: + + lemma `set_cons1` + + lemma `trivIset_bigcup` + + definition `maximal_disjoint_subcollection` + + lemma `ex_maximal_disjoint_subcollection` + +- in `mathcomp_extra.v`: + + lemma `leq_ltn_expn` + +- in `lebesgue_measure.v`: + + lemma `lebesgue_measurable_ball` + + lemmas `measurable_closed_ball`, `lebesgue_measurable_closed_ball` + +- in `normedtype.v`: + + lemmas `ball0`, `ball_itv`, `closed_ball0`, `closed_ball_itv` + + definitions `cpoint`, `radius`, `is_ball` + + 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`, + `ballE`, `is_ball_closure`, `scale_ballE`, `cpoint_scale_ball`, + `radius_scale_ball` + + lemmas `vitali_lemma_finite`, `vitali_lemma_finite_cover` + + definition `vitali_collection_partition` + + lemmas `vitali_collection_partition_ub_gt0`, + `ex_vitali_collection_partition`, `cover_vitali_collection_partition`, + `disjoint_vitali_collection_partition` + + lemma `separate_closed_ball_countable` + + lemmas `vitali_lemma_infinite`, `vitali_lemma_infinite_cover` + +- in `topology.v`: + + lemmas `closure_eq0`, `separated_open_countable` + ### Changed - in `hoelder.v`: @@ -134,6 +167,8 @@ - in `lebesgue_integral.v`: + weaken an hypothesis of `integral_ae_eq` +- in `classical_sets.v`: + + `set_nil` generalized to `eqType` ### Deprecated diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 4c14d6449..da5645662 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -121,6 +121,10 @@ From mathcomp Require Import mathcomp_extra boolp. (* pblock_index D F x == index i such that i \in D and x \in F i *) (* pblock D F x := F (pblock_index D F x) *) (* *) +(* maximal_disjoint_subcollection F A B == A is a maximal (for inclusion) *) +(* disjoint subcollection of the collection *) +(* B of elements in F : I -> set T *) +(* *) (* * Upper and lower bounds: *) (* ubound A == the set of upper bounds of the set A *) (* lbound A == the set of lower bounds of the set A *) @@ -1058,9 +1062,12 @@ apply/predeqP => x; split=> [[a ? [b ? <-]]|[[a b] [? ? <-]]]/=; by [exists (a, b) | exists a => //; exists b]. Qed. -Lemma set_nil (T : choiceType) : [set` [::]] = @set0 T. +Lemma set_nil (T : eqType) : [set` [::]] = @set0 T. Proof. by rewrite predeqP. Qed. +Lemma set_cons1 (T : eqType) (x : T) : [set` [:: x]] = [set x]. +Proof. by apply/seteqP; split => y /=; rewrite ?inE => /eqP. Qed. + Lemma set_seq_eq0 (T : eqType) (S : seq T) : ([set` S] == set0) = (S == [::]). Proof. apply/eqP/eqP=> [|->]; rewrite predeqE //; case: S => // h t /(_ h). @@ -2550,6 +2557,16 @@ Lemma trivIset_preimage1_in {aT} {rT : choiceType} (D : set rT) (A : set aT) (f : aT -> rT) : trivIset D (fun x => A `&` f @^-1` [set x]). Proof. by move=> y z _ _ [x [[_ <-] [_ <-]]]. Qed. +Lemma trivIset_bigcup (I T : Type) (J : eqType) (D : J -> set I) (F : I -> set T) : + (forall n, trivIset (D n) F) -> + (forall n m i j, n != m -> D n i -> D m j -> F i `&` F j !=set0 -> i = j) -> + trivIset (\bigcup_k D k) F. +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. + 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. @@ -2777,6 +2794,34 @@ Qed. End Zorn_subset. +Definition maximal_disjoint_subcollection T I (F : I -> set T) (A B : set I) := + [/\ A `<=` B, trivIset A F & forall C, + A `<` C -> C `<=` B -> ~ trivIset C F ]. + +Section maximal_disjoint_subcollection. +Context {I T : Type}. +Variables (B : I -> set T) (D : set I). + +Let P := fun X => X `<=` D /\ trivIset X B. + +Let maxP (A : set (set I)) : + A `<=` P -> total_on A (fun x y => x `<=` y) -> P (\bigcup_(x in A) x). +Proof. +move=> AP h; split; first by apply: bigcup_sub => E /AP []. +move=> i j [x Ax] xi [y Ay] yj ij; have [xy|yx] := h _ _ Ax Ay. +- by apply: (AP _ Ay).2 => //; exact: xy. +- by apply: (AP _ Ax).2 => //; exact: yx. +Qed. + +Lemma ex_maximal_disjoint_subcollection : + { E | maximal_disjoint_subcollection B E D }. +Proof. +have /cid[E [[ED tEB] maxE]] := Zorn_bigcup maxP. +by exists E; split => // F /maxE + FD; exact: contra_not. +Qed. + +End maximal_disjoint_subcollection. + Definition premaximal T (R : T -> T -> Prop) (t : T) := forall s, R t s -> R s t. diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index ffbdc2014..9ee7661eb 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -1470,3 +1470,13 @@ Lemma ltr0_ge_norm : Proof. by move=> x y; rewrite !negrE => /ltW x0 /ltW y0; exact: ler0_ge_norm. Qed. End normr. + +Lemma leq_ltn_expn m : exists n, (2 ^ n <= m.+1 < 2 ^ n.+1)%N. +Proof. +elim: m => [|m [n /andP[h1 h2]]]; first by exists O. +have [m2n|nm2] := ltnP m.+2 (2 ^ n.+1)%N. + by exists n; rewrite m2n andbT (leq_trans h1). +exists n.+1; rewrite nm2/= -addn1. +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. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 7e6635850..798b33265 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -873,6 +873,38 @@ Qed. End lebesgue_measure_itv. +Section measurable_ball. +Variable R : realType. + +Lemma measurable_ball (x : R) e : measurable (ball x e). +Proof. by rewrite ball_itv; exact: measurable_itv. Qed. + +Lemma lebesgue_measure_ball (x r : R) : (0 <= r)%R -> + lebesgue_measure (ball x r) = (r *+ 2)%:E. +Proof. +rewrite le_eqVlt => /orP[/eqP <-|r0]. + by rewrite (ball0 _ _).2// measure0 mul0rn. +rewrite ball_itv lebesgue_measure_itv/= lte_fin ltr_subl_addr -addrA ltr_addl. +by rewrite addr_gt0 // -EFinD addrAC opprD opprK addrA subrr add0r -mulr2n. +Qed. + +Lemma measurable_closed_ball (x : R) r : measurable (closed_ball x r). +Proof. +have [r0|r0] := leP r 0; first by rewrite closed_ball0. +by rewrite closed_ball_itv. +Qed. + +Lemma lebesgue_measure_closed_ball (x r : R) : 0 <= r -> + lebesgue_measure (closed_ball x r) = (r *+ 2)%:E. +Proof. +rewrite le_eqVlt => /predU1P[<-|r0]; first by rewrite mul0rn closed_ball0. +rewrite closed_ball_itv// lebesgue_measure_itv/= lte_fin -ltr_subl_addl addrAC. +rewrite subrr add0r gtr_opp// ?mulr_gt0// -EFinD; congr (_%:E). +by rewrite opprB addrAC addrCA subrr addr0 -mulr2n. +Qed. + +End measurable_ball. + Lemma lebesgue_measure_rat (R : realType) : lebesgue_measure (range ratr : set R) = 0%E. Proof. @@ -1358,12 +1390,6 @@ move=> q; case: ifPn => // qfab; apply: is_interval_measurable => //. exact: is_interval_bigcup_ointsub. Qed. -Lemma measurable_ball (r x : R) : 0 < r -> measurable (ball x r). -Proof. -move=> ?; apply: open_measurable. -exact: (@ball_open _ [normedModType R of R^o]). -Qed. - Lemma open_measurable_subspace (D : set R) (U : set (subspace D)) : measurable D -> open U -> measurable (D `&` U). Proof. diff --git a/theories/normedtype.v b/theories/normedtype.v index 91b6f4401..46e95f5ae 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -99,6 +99,14 @@ Require Import ereal reals signed topology prodnormedzmodule. (* the Heine-Borel theorem, which states that the compact sets of R^n are *) (* the closed and bounded sets. *) (* *) +(* 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} *) +(* 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 *) +(* 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 *) +(* *) (******************************************************************************) Reserved Notation "f @`[ a , b ]" (at level 20, b at level 9, @@ -118,6 +126,7 @@ Reserved Notation "k .-lipschitz_ A f" Reserved Notation "k .-lipschitz f" (at level 2, format "k .-lipschitz f"). Reserved Notation "[ 'lipschitz' E | x 'in' A ]" (at level 0, x name, format "[ 'lipschitz' E | x 'in' A ]"). +Reserved Notation "k *` A" (at level 40, left associativity, format "k *` A"). Set Implicit Arguments. Unset Strict Implicit. @@ -5787,6 +5796,25 @@ Qed. End continuous. +Section ball_realFieldType. +Variables (R : realFieldType). + +Lemma ball0 (a r : R) : ball a r = set0 <-> r <= 0. +Proof. +split. + move=> /seteqP[+ _] => H; rewrite leNgt; apply/negP => r0. + by have /(_ (ballxx _ r0)) := H a. +move=> r0; apply/seteqP; split => // y; rewrite /ball/=. +by move/lt_le_trans => /(_ _ r0); rewrite normr_lt0. +Qed. + +Lemma ball_itv (x r : R) : (ball x r = `]x - r, x + r[%classic)%R. +Proof. +by apply/seteqP; split => y; rewrite /ball/= in_itv/= ltr_distlC. +Qed. + +End ball_realFieldType. + Section Closed_Ball. Lemma ball_open (R : numDomainType) (V : normedModType R) (x : V) (r : R) : @@ -5812,6 +5840,13 @@ Qed. Definition closed_ball (R : numDomainType) (V : pseudoMetricType R) (x : V) (e : R) := closure (ball x e). +Lemma closed_ball0 (R : realFieldType) (a r : R) : + r <= 0 -> closed_ball a r = set0. +Proof. +move=> /ball0 r0; apply/seteqP; split => // y. +by rewrite /closed_ball r0 closure0. +Qed. + 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. @@ -5845,6 +5880,13 @@ Lemma closed_ball_closed (R : realFieldType) (V : pseudoMetricType R) (x : V) (r : R) : closed (closed_ball x r). Proof. exact: closed_closure. Qed. +Lemma closed_ball_itv (R : realFieldType) (x r : R) : 0 < r -> + (closed_ball x r = `[x - r, x + r]%classic)%R. +Proof. +by move=> r0; apply/seteqP; split => y; + rewrite closed_ballE// /closed_ball_ /= in_itv/= ler_distlC. +Qed. + Lemma closed_ballR_compact (R : realType) (x e : R) : 0 < e -> compact (closed_ball x e). Proof. @@ -6103,3 +6145,495 @@ 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). + +Section center_radius. +Context {R : numDomainType} {M : pseudoMetricType R}. +Implicit Types A : set M. + +(* NB: the identifier "center" is already taken! *) +Definition cpoint A := get [set c | exists r, A = ball c r]. + +Definition radius A : {nonneg R} := + xget 0%:nng [set r | A = ball (cpoint A) r%:num]. + +Definition is_ball A := A == ball (cpoint A) (radius A)%:num. + +Definition scale_ball (k : R) A := + if is_ball A then ball (cpoint A) (k * (radius A)%:num) else set0. + +Local Notation "k *` B" := (scale_ball k B). + +Lemma sub_scale_ball A k l : k <= l -> k *` A `<=` l *` A. +Proof. +move=> kl; rewrite /scale_ball; case: ifPn=> [Aball|_]; last exact: subset_refl. +by apply: le_ball; rewrite ler_wpmul2r. +Qed. + +Lemma scale_ball1 A : is_ball A -> 1 *` A = A. +Proof. by move=> Aball; rewrite /scale_ball Aball mul1r; move/eqP in Aball. Qed. + +Lemma sub1_scale_ball A l : is_ball A -> A `<=` l.+1%:R *` A. +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. + +Section center_radius_realFieldType. +Context {R : realFieldType}. +Implicit Types x y r s : R. + +Let ball_inj_radius_gt0 x y r s : 0 < r -> ball x r = ball y s -> 0 < s. +Proof. +move=> r0 xrys; rewrite ltNge; apply/negP => /ball0 s0; move: xrys. +by rewrite s0 => /seteqP[+ _] => /(_ x); apply; exact: ballxx. +Qed. + +Let ball_inj_center x y r s : 0 < r -> ball x r = ball y s -> x = y. +Proof. +move=> r0 xrys; have s0 := ball_inj_radius_gt0 r0 xrys. +apply/eqP/negPn/negP => xy. +wlog : x y r s xrys r0 s0 xy / x < y. + move: xy; rewrite neq_lt => /orP[xy|yx]. + by move/(_ _ _ _ _ xrys); apply => //; rewrite lt_eqF. + by move/esym : xrys => /[swap] /[apply]; apply => //; rewrite lt_eqF. +move=> {}xy; have [rs|sr] := ltP r s. +- suff : ~ ball x r (y + r). + by apply; rewrite xrys /ball/= ltr_distlC !ltr_add2l -ltr_norml gtr0_norm. + by rewrite /ball/= ltr_distlC ltr_add2r (ltNge y) (ltW xy) andbF. +- suff : ~ ball y s (x - r + minr ((y - x) / 2) r). + apply; rewrite -xrys /ball/= ltr_distlC ltr_addl lt_minr r0 andbT. + rewrite divr_gt0 ?subr_gt0//= addrAC ltr_subl_addl addrCA ler_lt_add//. + by rewrite lt_minl ltr_addl r0 orbT. + have [yx2r|ryx2] := ltP ((y - x) / 2) r. + rewrite /ball/= ltr_distlC => /andP[+ _]; rewrite -(@ltr_pmul2l _ 2)//. + rewrite !mulrDr mulrCA divff// mulr1 ltNge => /negP; apply. + rewrite addrAC !addrA (addrC _ y) mulr_natl mulr2n addrA addrK. + rewrite (mulr_natl y) mulr2n -!addrA ler_add2l (ler_add (ltW _))//. + by rewrite ler_wpmul2l// ler_oppl opprK. + rewrite subrK /ball/= ltr_distlC => /andP[]. + rewrite ltr_subl_addl addrC -ltr_subl_addl -(@ltr_pmul2r _ (2^-1))//. + move=> /le_lt_trans => /(_ _ ryx2) /le_lt_trans => /(_ _ sr). + by rewrite ltr_pmulr// invf_gt1// ltNge ler1n. +Qed. + +Let ball_inj_radius x y r s : 0 < r -> ball x r = ball y s -> r = s. +Proof. +move=> r0 xrys; have s0 := ball_inj_radius_gt0 r0 xrys. +move: (xrys); rewrite (ball_inj_center r0 xrys) => {}xrys. +apply/eqP/negPn/negP; rewrite neq_lt => /orP[rs|sr]. +- suff : ball y s (y + r) by rewrite -xrys /ball/= ltr_distlC ltxx andbF. + rewrite /ball/= ltr_distlC !ltr_add2l rs andbT (lt_trans _ r0)//. + by rewrite ltr_oppl oppr0 (lt_trans r0). +- suff : ball y r (y + s) by rewrite xrys /ball/= ltr_distlC ltxx andbF. + rewrite /ball/= ltr_distlC !ltr_add2l sr andbT (lt_trans _ s0)//. + by rewrite ltr_oppl oppr0 (lt_trans s0). +Qed. + +Lemma ball_inj x y r s : 0 < r -> ball x r = ball y s -> x = y /\ r = s. +Proof. +by move=> r0 xrys; split; [exact: (ball_inj_center r0 xrys)| + exact: (ball_inj_radius r0 xrys)]. +Qed. + +Lemma radius0 : radius (@set0 R) = 0%:nng :> {nonneg R}. +Proof. +rewrite /radius/=; case: xgetP => [r _ /= /esym/ball0 r0|]/=. + by apply/val_inj/eqP; rewrite /= eq_le r0/=. +by move=> /(_ 0%:nng) /nesym /ball0. +Qed. + +Lemma is_ball0 : is_ball (@set0 R). +Proof. +rewrite /is_ball; apply/eqP/seteqP; split => // x; rewrite radius0/=. +by rewrite (ball0 _ _).2. +Qed. + +Lemma cpoint_ball x r : 0 < r -> cpoint (ball x r) = x. +Proof. +move=> r0; rewrite /cpoint; case: xgetP => [y _ [s] /(ball_inj r0)[]//|]. +by move=> /(_ x)/forallNP/(_ r). +Qed. + +Lemma radius_ball_num x r : 0 <= r -> (radius (ball x r))%:num = r. +Proof. +rewrite le_eqVlt => /orP[/eqP <-|r0]; first by rewrite (ball0 _ _).2// radius0. +rewrite /radius; case: xgetP => [y _ /(ball_inj r0)[]//|]. +by move=> /(_ (NngNum (ltW r0)))/=; rewrite cpoint_ball. +Qed. + +Lemma radius_ball x r (r0 : 0 <= r) : radius (ball x r) = NngNum r0. +Proof. by apply/val_inj => //=; rewrite radius_ball_num. Qed. + +Lemma is_ballP (A : set R) x : is_ball A -> + A x -> `|cpoint A - x| < (radius A)%:num. +Proof. by rewrite /is_ball => /eqP {1}-> /lt_le_trans; exact. Qed. + +Lemma is_ball_ball x r : is_ball (ball x r). +Proof. +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. +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. +Proof. +move=> ballA; apply/seteqP; split => [x /is_ballP|x Ax]; first exact. +by move: ballA => /eqP ->. +Qed. + +Lemma is_ball_closureP (A : set R) x : is_ball A -> + closure A x -> `|cpoint A - x| <= (radius A)%:num. +Proof. +move=> ballP cAx. +have : closed_ball (cpoint A) (radius A)%:num x by rewrite /closed_ball -ballE. +by have [r0|r0] := ltP 0 (radius A)%:num; [rewrite closed_ballE| + rewrite closed_ball0]. +Qed. + +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 scale_ballE k x r : 0 <= k -> k *` ball x r = ball x (k * r). +Proof. +move=> k0; have [r0|r0] := ltP 0 r. + apply/seteqP; split => y. + 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. +by rewrite mulr_ge0_le0. +Qed. + +Lemma cpoint_scale_ball A (k : R) : 0 < k -> is_ball A -> 0 < (radius A)%:num -> + cpoint (k *` A) = cpoint A :> R. +Proof. +move=> k0 ballA r0. +rewrite [in LHS](ballE ballA) (scale_ballE _ _ (ltW k0))// cpoint_ball//. +by rewrite mulr_gt0. +Qed. + +Lemma radius_scale_ball (A : set R) (k : R) : 0 <= k -> is_ball A -> + (radius (k *` A))%:num = k * (radius A)%:num. +Proof. +move=> k0 ballA. +by rewrite [in LHS](ballE ballA) (scale_ballE _ _ k0)// radius_ball// mulr_ge0. +Qed. + +End center_radius_realFieldType. + +Section vitali_lemma_finite. +Context {R : realType} {I : eqType}. +Variable (B : I -> set R). +Hypothesis is_ballB : forall i, is_ball (B i). +Hypothesis B_set0 : forall i, B i !=set0. + +Lemma vitali_lemma_finite (s : seq I) : + { D : seq I | [/\ + {subset D <= s}, trivIset [set` D] B & + forall i, i \in s -> exists j, [/\ j \in D, + B i `&` B j !=set0, + radius (B j) >= radius (B i) & + B i `<=` 3%:R *` B j] ] }. +Proof. +pose LE x y := radius (B x) <= radius (B y). +have LE_trans : transitive LE by move=> x y z; exact: le_trans. +wlog : s / sorted LE s. + have : sorted LE (sort LE s) by apply: sort_sorted => x y; exact: le_total. + move=> /[swap] /[apply] -[D [Ds trivIset_DB H]]; exists D; split => //. + - by move=> x /Ds; rewrite mem_sort. + - by move=> i; rewrite -(mem_sort LE) => /H. +elim: s => [_|i [/= _ _|j t]]; first by exists nil. + exists [:: i]; split => //; first by rewrite set_cons1; exact: trivIset1. + move=> _ /[1!inE] /eqP ->; exists i; split => //; first by rewrite mem_head. + - by rewrite setIid; exact: B_set0. + - exact: sub1_scale_ball. +rewrite /= => + /andP[ij jt] => /(_ jt)[u [ujt trivIset_uB H]]. +have [K|] := pselect (forall j, j \in u -> B j `&` B i = set0). + exists (i :: u); split => //. + - move=> x /[1!inE] /predU1P[->|]; first by rewrite mem_head. + by move/ujt => xjt; rewrite in_cons xjt orbT. + - move=> k l /= /[1!inE] /predU1P[->{k}|ku]. + by move=> /predU1P[->{j}//|js] /set0P; rewrite setIC K// eqxx. + by move=> /predU1P[->{l} /set0P|lu]; [rewrite K// eqxx|exact: trivIset_uB]. + - move=> k /[1!inE] /predU1P[->{k}|]. + exists i; split; [by rewrite mem_head| |exact: lexx|]. + by rewrite setIid; exact: B_set0. + exact: sub1_scale_ball. + by move/H => [l [lu lk0 kl k3l]]; exists l; split => //; rewrite inE lu orbT. +move/existsNP/cid => [k /not_implyP[ku /eqP/set0P ki0]]. +exists u; split => //. + by move=> l /ujt /[!inE] /predU1P[->|->]; rewrite ?eqxx ?orbT. +move=> _ /[1!inE] /predU1P[->|/H//]; exists k; split; [exact: ku| | |]. +- by rewrite setIC. +- apply: (le_trans ij); move/ujt : ku => /[1!inE] /predU1P[<-|kt]. + exact: lexx. + by have /allP := order_path_min LE_trans jt; apply; exact: kt. +- case: ki0 => x [Bkx Bix] y => iy. + rewrite (ballE (is_ballB k)) scale_ballE// /ball/=. + rewrite -(subrK x y) -(addrC x) opprD addrA opprB. + rewrite (le_lt_trans (ler_norm_add _ _))// -nat1r mulrDl mul1r mulr_natl. + rewrite (ltr_add (is_ballP (is_ballB k) _))// -(subrK (cpoint (B i)) y). + rewrite -(addrC (cpoint (B i))) opprD addrA opprB. + rewrite (le_lt_trans (ler_norm_add _ _))//. + apply (@lt_le_trans _ _ ((radius (B j))%:num *+ 2)); last first. + apply: ler_wmuln2r; move/ujt : ku; rewrite inE => /predU1P[<-|kt]. + exact: lexx. + by have /allP := order_path_min LE_trans jt; apply; exact: kt. + rewrite mulr2n ltr_add//. + by rewrite distrC (lt_le_trans (is_ballP (is_ballB i) _)). + by rewrite (lt_le_trans (is_ballP (is_ballB i) _)). +Qed. + +Lemma vitali_lemma_finite_cover (s : seq I) : + { D : seq I | [/\ {subset D <= s}, + trivIset [set` D] B & + cover [set` s] B `<=` cover [set` D] (scale_ball 3%:R \o B)] }. +Proof. +have [D [DV tD maxD]] := vitali_lemma_finite s. +exists D; split => // x [i Vi] cBix/=. +by have [j [Dj BiBj ij]] := maxD i Vi; move/(_ _ cBix) => ?; exists j. +Qed. + +End vitali_lemma_finite. + +Section vitali_collection_partition. +Context {R : realType} {I : eqType}. +Variables (B : I -> set R) (V : set I) (r : R). +Hypothesis is_ballB : forall i, is_ball (B i). +Hypothesis B_set0 : forall i, 0 < (radius (B i))%:num. + +Definition vitali_collection_partition n := + [set i | V i /\ r / (2 ^ n.+1)%:R < (radius (B i))%:num <= r / (2 ^ n)%:R]. + +Hypothesis VBr : forall i, V i -> (radius (B i))%:num <= r. + +Lemma vitali_collection_partition_ub_gt0 i : V i -> 0 < r. +Proof. by move=> Vi; rewrite (lt_le_trans _ (VBr Vi)). Qed. + +Notation r_gt0 := vitali_collection_partition_ub_gt0. + +Lemma ex_vitali_collection_partition i : + V i -> exists n, vitali_collection_partition n i. +Proof. +move=> Vi; pose f := floor (r / (radius (B i))%:num). +have f_ge0 : 0 <= f by rewrite floor_ge0// divr_ge0// ltW// (r_gt0 Vi). +have [m /andP[mf fm]] := leq_ltn_expn `|f|.-1. +exists m; split => //; apply/andP; split => [{mf}|{fm}]. + rewrite -(@ler_nat R) in fm. + rewrite ltr_pdivr_mulr// mulrC -ltr_pdivr_mulr//. + rewrite (lt_le_trans _ fm)// (lt_le_trans (lt_succ_floor _))//= -/f. + rewrite -natr1 ler_add2r//. + have [<-|f0] := eqVneq 0 f; first by rewrite /= ler0n. + rewrite prednK//; last by rewrite absz_gt0 eq_sym. + by rewrite natr_absz// ger0_norm. +move: m => [|m] in mf *; first by rewrite expn0 divr1 VBr. +rewrite -(@ler_nat R) in mf. +rewrite ler_pdivl_mulr// mulrC -ler_pdivl_mulr//. +have [f0|f0] := eqVneq 0 f. + by move: mf; rewrite -f0 absz0 leNgt expnS ltr_nat leq_pmulr// expn_gt0. +rewrite (le_trans mf)// prednK//; last by rewrite absz_gt0 eq_sym. +by rewrite natr_absz// ger0_norm// floor_le. +Qed. + +Lemma cover_vitali_collection_partition : + V = \bigcup_n vitali_collection_partition n. +Proof. +apply/seteqP; split => [|i [n _] []//]. +by move=> i Vi; have [n Hn] := ex_vitali_collection_partition Vi; exists n. +Qed. + +Lemma disjoint_vitali_collection_partition n m : n != m -> + vitali_collection_partition n `&` + vitali_collection_partition m = set0. +Proof. +move=> nm; wlog : n m nm / (n < m)%N. + move=> wlg; move: nm; rewrite neq_lt => /orP[nm|mn]. + by rewrite wlg// lt_eqF. + by rewrite setIC wlg// lt_eqF. +move=> {}nm; apply/seteqP; split => // i [] [Vi] /andP[rnB _] [_ /andP[_]]. +move/(lt_le_trans rnB); 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. + +End vitali_collection_partition. + +Lemma separated_closed_ball_countable + {R : realType} (I : Type) (B : I -> set R) (D : set I) : + (forall i, (radius (B i))%:num > 0) -> + trivIset D (fun i => closed_ball (cpoint (B i)) (radius (B i))%:num) -> countable D. +Proof. +move=> B0 tD. +have : trivIset D (fun i => ball (cpoint (B i)) (radius (B i))%:num). + move=> i j Di Dj BiBj; apply: tD => //. + by apply: subsetI_neq0 BiBj => //; exact: subset_closed_ball. +apply: separated_open_countable => //; first by move=> i; exact: ball_open. +by move=> i; eexists; exact: ballxx. +Qed. + +Section vitali_lemma_infinite. +Context {R : realType} {I : eqType}. +Variables (B : I -> set R) (V : set I) (r : R). +Hypothesis is_ballB : forall i, is_ball (B i). +Hypothesis Bset0 : forall i, (radius (B i))%:num > 0. +Hypothesis VBr : forall i, V i -> (radius (B i))%:num <= r. + +Let B_ := vitali_collection_partition B V r. + +Let H_ n (U : set I) := [set i | B_ n i /\ + forall j, U j -> i != j -> closure (B i) `&` closure (B j) = set0]. + +Let elt_prop (x : set I * nat * set I) := + x.1.1 `<=` V /\ + maximal_disjoint_subcollection (closure \o B) x.1.1 (H_ x.1.2 x.2). + +Let elt_type := {x | elt_prop x}. + +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_infinite : { D : set I | [/\ countable D, + D `<=` V, trivIset D (closure \o B) & + forall i, V i -> exists j, [/\ D j, + closure (B i) `&` closure (B j) !=set0, + (radius (B j))%:num >= (radius (B i))%:num / 2 & + closure (B i) `<=` closure (5%:R *` B j)] ] }. +Proof. +have [D0 [D0B0 tD0 maxD0]] := + ex_maximal_disjoint_subcollection (closure \o B) (B_ O). +have H0 : elt_prop (D0, 0%N, set0). + split; first by move=> i /D0B0[]. + split => //=. + - move=> x /= D0x; split; first exact: D0B0. + by move=> s D0s xs; move/trivIsetP : tD0; exact. + - by move=> F D0F FH0; apply: maxD0 => // i Fi; exact: (FH0 _ Fi).1. +have [v [Hv0 HvRel]] : {v : nat -> elt_type | + v 0%N = exist _ _ H0 /\ forall n, Rel (v n) (v n.+1)}. + apply: dependent_choice_Type => -[[[Dn n] Un] Hn]. + pose Hn1 := H_ n.+1 (Un `|` Dn). + have [Dn1 maxDn1] := + ex_maximal_disjoint_subcollection (closure\o B) Hn1. + suff: elt_prop (Dn1, n.+1, Un `|` Dn) by move=> H; exists (exist _ _ H). + by split => //=; case: maxDn1 => + _ _ => /subset_trans; apply => i [[]]. +pose D i := (sval (v i)).1.1. +pose U i := (sval (v i)).2. +have UE n : U n = \bigcup_(i < n) D i. + elim: n => [|n ih]; first by rewrite bigcup_mkord big_ord0 /U /sval /D Hv0. + by rewrite /U /sval/= (HvRel n).1 bigcup_mkord big_ord_recr -bigcup_mkord -ih. +pose v_ i := (sval (v i)).1.2. +have v_E n : v_ n = n. + elim: n => /= [|n]; first by rewrite /v_ /sval/= Hv0. + by move: (HvRel n).2; rewrite -!/(v_ _) => <- ->. +have maxD m : maximal_disjoint_subcollection (closure\o B) (D m) + (H_ m (\bigcup_(i < m) D i)). + by rewrite -(UE m) -[m in H_ m _]v_E /v_ /U /D; move: (v m) => [x []]. +have DH m : D m `<=` H_ m (\bigcup_(i < m) D i) by have [] := maxD m. +exists (\bigcup_k D k); split. +- apply: bigcup_countable => // n _. + apply: (@separated_closed_ball_countable R _ B) => //. + have [_ + _] := maxD n; move=> DB i j Dni Dnj. + by rewrite -!is_ball_closure//; exact: DB. +- by move=> i [n _ Dni]; have [+ _ _] := maxD n; move/(_ _ Dni) => [[]]. +- apply: trivIset_bigcup => 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. + move=> /set0P/eqP; apply: contra_notP => /eqP. + by rewrite eq_sym setIC; apply: H => //; exists m. +move=> i Vi. +have [n Bni] := ex_vitali_collection_partition Bset0 VBr Vi. +have [[j Dj BiBj]|] := + pselect (exists2 j, (\bigcup_(i < n.+1) D i) j & + closure (B i) `&` closure (B j) !=set0); last first. + move/forall2NP => H. + have {}H j : (\bigcup_(i < n.+1) D i) j -> + closure (B i) `&` closure (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 -> closure (B i) `&` closure (B j) = set0. + by move=> Dnj; apply: H; exists n => //=. + have [Dni|Dni] := pselect (D n i). + have := Dn_Bi _ Dni. + rewrite setIid => /closure_eq0 Bi0. + by have := Bset0 i; rewrite Bi0 radius0/= ltxx. + have not_tB : ~ trivIset (D n `|` [set i]) (closure \o B). + have [_ _] := maxD n. + apply. + split; first exact: subsetUl. + by move=> x; apply/Dni; apply: x; right. + by rewrite subUset; split; [exact: DH|]; 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 & + closure (B p) `&` closure (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] /not_implyP[Dni1] /not_implyP[pq pq0]. + by split => //; exact/set0P/eqP. + case: Dnpi => [Dnp|pi]. + - case: Dnqi => [Dnq|qi]. + + case: (maxD n) => _ + _. + move/trivIsetP => /(_ _ _ Dnp Dnq pq). + by move/set0P : pq0 => /eqP. + + have := Dn_Bi _ Dnp. + by rewrite setIC -qi; move/set0P : pq0 => /eqP. + - case: Dnqi => [Dnq|qi]. + + have := Dn_Bi _ Dnq. + by rewrite -pi; move/set0P : pq0 => /eqP. + + by move: pq; rewrite pi qi eqxx. +have Birn : (radius (B i))%:num <= r / (2 ^ n)%:R. + by move: Bni; by rewrite /B_ /= => -[_] /andP[]. +have Bjrn : (radius (B j))%:num > r / (2 ^ n.+1)%:R. + have : \bigcup_(i < n.+1) D i `<=` \bigcup_(i < n.+1) (B_ i). + move=> k [m/= mn] Dmk. + have [+ _ _] := maxD m. + by move/(_ _ Dmk) => -[Bmk] _; exists m. + move/(_ _ Dj) => [m/= mn1] [_] /andP[+ _]. + apply: le_lt_trans. + rewrite ler_pmul2l ?(vitali_collection_partition_ub_gt0 Bset0 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. +- rewrite (le_trans _ (ltW Bjrn))// ler_pdivr_mulr// expnSr natrM. + by rewrite invrM ?unitfE// mulrAC -mulrA (mulrA 2) divff// div1r. +- move=> x Bix. + rewrite is_ball_closure//; last first. + by rewrite (ballE (is_ballB j)) scale_ballE; [exact: is_ball_ball|]. + rewrite closed_ballE; last first. + rewrite (ballE (is_ballB j)) scale_ballE; last by []. + by rewrite radius_ball_num ?mulr_ge0// mulr_gt0. + rewrite /closed_ball_ /= cpoint_scale_ball; [|by []..]. + rewrite radius_scale_ball//. + apply: (@le_trans _ _ (2 * (radius (B i))%:num + (radius (B j))%:num)). + case: BiBj => y [Biy Bjy]. + rewrite (le_trans (ler_dist_add y _ _))// [in leRHS]addrC ler_add//. + exact: is_ball_closureP. + rewrite (le_trans (ler_dist_add (cpoint (B i)) _ _))//. + rewrite (_ : 2 = 1 + 1); last by []. + rewrite mulrDl !mul1r// ler_add; [by []| |exact: is_ball_closureP]. + by rewrite distrC; exact: is_ball_closureP. + rewrite -ler_subr_addr// -(@natr1 _ 4). + rewrite (mulrDl 4%:R) mul1r addrK (natrM _ 2 2) -mulrA ler_pmul2l//. + rewrite (le_trans Birn)// [in leRHS]mulrC -ler_pdivr_mulr//. + by rewrite -mulrA -invfM -natrM-expnSr ltW. +Qed. + +Lemma vitali_lemma_infinite_cover : { D : set I | [/\ countable D, + D `<=` V, trivIset D (closure\o B) & + cover V (closure\o B) `<=` cover D (closure \o scale_ball 5%:R \o B)] }. +Proof. +have [D [cD DV tD maxD]] := vitali_lemma_infinite. +exists D; split => // x [i Vi] cBix/=. +by have [j [Dj BiBj ij]] := maxD i Vi; move/(_ _ cBix) => ?; exists j. +Qed. + +End vitali_lemma_infinite. diff --git a/theories/topology.v b/theories/topology.v index f4eb2ae8f..693cd5bff 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -2639,6 +2639,11 @@ Proof. by under eq_fun do rewrite -meets_openr meets_globallyl. Qed. Lemma subset_closure (A : set T) : A `<=` closure A. Proof. by move=> p ??; exists p; split=> //; apply: nbhs_singleton. Qed. +Lemma closure_eq0 (A : set T) : closure A = set0 -> A = set0. +Proof. +by move=> A0; apply/seteqP; split => //; rewrite -A0; exact: subset_closure. +Qed. + Lemma closureI (A B : set T) : closure (A `&` B) `<=` closure A `&` closure B. Proof. by move=> p clABp; split=> ? /clABp [q [[]]]; exists q. Qed. @@ -6498,6 +6503,29 @@ apply: reA; rewrite /ball /= distrC ltr_distl qre andbT. by rewrite (@le_lt_trans _ _ r)// ?qre// ler_subl_addl ler_addr ltW. Qed. +Lemma separated_open_countable + {R : realType} (I : Type) (B : I -> set R) (D : set I) : + (forall i, open (B i)) -> (forall i, B i !=set0) -> + trivIset D B -> countable D. +Proof. +move=> oB B0 tB; have [f fB] : + {f : I -> rat & forall i, D i -> B i (ratr (f i))}. + apply: (@choice _ _ (fun x y => D x -> B x (ratr y))) => i. + have [r [Bir [q _ qr]]] := dense_rat (B0 _) (oB i). + by exists q => Di; rewrite qr. +have inj_f : {in D &, injective f}. + move=> i j /[!inE] Di Dj /(congr1 ratr) ratrij. + have ? : (B i `&` B j) (ratr (f i)). + by split => //; [exact: fB|rewrite ratrij; exact: fB]. + by apply/(tB _ _ Di Dj); exists (ratr (f i)). +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. + rewrite /nat_of_rat; apply: inj_comp => //; apply: inj_comp => //. + exact/bij_inj. +by exists (nat_of_rat \o f) => i j Di Dj /inj_nat_of_rat/inj_f; exact. +Qed. + Section weak_pseudoMetric. Context {R : realType} (pS : pointedType) (U : pseudoMetricType R) . Variable (f : pS -> U).