tentative formalization of Vitali's lemmas

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

@@ -1442,3 +1442,13 @@ Arguments le_bigmax_seq {d T} x {I r} i0 P.
 (* NB: PR 1079 to MathComp in progress *)
 Lemma gerBl {R : numDomainType} (x y : R) : 0 <= y -> x - y <= x.
 Proof. by move=> y0; rewrite ler_subl_addl ler_addr. Qed.
+
+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

@@ -699,26 +699,6 @@ Notation emeasurable_itv_bnd_pinfty := emeasurable_itv.
 #[deprecated(since="mathcomp-analysis 0.6.2", note="use `emeasurable_itv` instead")]
 Notation emeasurable_itv_ninfty_bnd := emeasurable_itv.
 
-Lemma measurable_fine (R : realType) (D : set (\bar R)) : measurable D ->
-  measurable_fun D fine.
-Proof.
-move=> mD _ /= B mB; rewrite [X in measurable X](_ : _ `&` _ = if 0%R \in B then
-    D `&` ((EFin @` B) `|` [set -oo; +oo]%E) else D `&` EFin @` B); last first.
-  apply/seteqP; split=> [[r [Dr Br]|[Doo B0]|[Doo B0]]|[r| |]].
-  - by case: ifPn => _; split => //; left; exists r.
-  - by rewrite mem_set//; split => //; right; right.
-  - by rewrite mem_set//; split => //; right; left.
-  - by case: ifPn => [_ [Dr [[s + [sr]]|[]//]]|_ [Dr [s + [sr]]]]; rewrite sr.
-  - by case: ifPn => [/[!inE] B0 [Doo [[]//|]] [//|_]|B0 [Doo//] []].
-  - by case: ifPn => [/[!inE] B0 [Doo [[]//|]] [//|_]|B0 [Doo//] []].
-case: ifPn => B0; apply/measurableI => //; last exact: measurable_image_EFin.
-by apply: measurableU; [exact: measurable_image_EFin|exact: measurableU].
-Qed.
-#[global] Hint Extern 0 (measurable_fun _ fine) =>
-  solve [exact: measurable_fine] : core.
-#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_fine` instead")]
-Notation measurable_fun_fine := measurable_fine.
-
 Section lebesgue_measure_itv.
 Variable R : realType.
 
@@ -873,6 +853,58 @@ 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 measurable_fine (R : realType) (D : set (\bar R)) : measurable D ->
+  measurable_fun D fine.
+Proof.
+move=> mD _ /= B mB; rewrite [X in measurable X](_ : _ `&` _ = if 0%R \in B then
+    D `&` ((EFin @` B) `|` [set -oo; +oo]%E) else D `&` EFin @` B); last first.
+  apply/seteqP; split=> [[r [Dr Br]|[Doo B0]|[Doo B0]]|[r| |]].
+  - by case: ifPn => _; split => //; left; exists r.
+  - by rewrite mem_set//; split => //; right; right.
+  - by rewrite mem_set//; split => //; right; left.
+  - by case: ifPn => [_ [Dr [[s + [sr]]|[]//]]|_ [Dr [s + [sr]]]]; rewrite sr.
+  - by case: ifPn => [/[!inE] B0 [Doo [[]//|]] [//|_]|B0 [Doo//] []].
+  - by case: ifPn => [/[!inE] B0 [Doo [[]//|]] [//|_]|B0 [Doo//] []].
+case: ifPn => B0; apply/measurableI => //; last exact: measurable_image_EFin.
+by apply: measurableU; [exact: measurable_image_EFin|exact: measurableU].
+Qed.
+#[global] Hint Extern 0 (measurable_fun _ fine) =>
+  solve [exact: measurable_fine] : core.
+#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_fine` instead")]
+Notation measurable_fun_fine := measurable_fine.
+
 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.