tentative formalization of Vitali's lemma (#973)

* tentative formalization of Vitali's lemmas

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
 

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.
 

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.

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.