tentative formalization of Vitali's theorem (#984)

* tentative formalization of Vitali's theorem --------- Co-authored-by: zstone1 <[email protected]>
math-comp · Nov 14, 2023 · e9e0b81 · e9e0b81
1 parent 1d1d9bf
commit e9e0b81
Show file tree

Hide file tree

Showing 10 changed files with 447 additions and 28 deletions.
diff --git 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`
@@ -100,6 +100,30 @@
 
 - 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`
+
+- in `normedtype.v`:
+  + lemmas `scale_ball0`, `closure_ball`, `bigcup_ballT`
 
 ### Changed
 

diff --git 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/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
@@ -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
@@ -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,273 @@ exists (B `|` C); split.
 Qed.
 
 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 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'.
+    split; [exact: ABV.1|move=> x Ax e e0].
+    have : (0 < minr e 1)%R by rewrite lt_minr// e0/=.
+    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.
+    - 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 ABV.1 B0 VB1.
+exists D; split => //.
+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.
+    by rewrite (Zr (PosNum (ltr0Sn _ n))).
+  set F := fun n => Z n%:R.
+  have : mu (\bigcup_n F n) <= \sum_(i <oo) mu (F i).
+    exact: outer_measure_sigma_subadditive.
+  rewrite eseries0; last by move=> n _; rewrite /F Zr.
+  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) 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) (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 (ABV.1 n) Bny.
+    by move=> /le_trans; apply; rewrite VB1//; exact: DV.
+  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) (r%:num + 2))%R.
+  rewrite -(set_mem_set E) -nneseries_esum// -measure_bigcup//; last 2 first.
+    by move=> *; exact: measurable_closure.
+    by apply: sub_trivIset tDB => ? [].
+  apply/le_measure; rewrite ?inE; [|exact: measurable_ball|exact: bigcup_sub].
+  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 _ [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.
+    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 [in leRHS]big_seq; apply: lee_sum => // j.
+    move=> /CsubFi[_ /andP[+ _]].
+    rewrite -lte_fin => /ltW/le_trans; apply.
+    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 => *.
+      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) (r%:num + 2))%R.
+    rewrite (le_trans _ EBr2)// -(set_mem_set E) -nneseries_esum //.
+    rewrite E_partition -measure_bigcup//=; last 2 first.
+      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.
+    - 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) (r%:num + 2))%R < +oo.
+  by rewrite lebesgue_measure_ball// ltry.
+have FE : \sum_(n <oo) \esum_(i in F n) mu (closure (B i)) =
+          mu (\bigcup_(i in E) closure (B i)).
+  rewrite E_partition bigcup_bigcup; apply/esym.
+  transitivity (\sum_(n <oo) mu (\bigcup_(i in F n) closure (B i))).
+    apply: measure_semi_bigcup => //.
+    - 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 _.
+      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.
+    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 _.
+    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 -measure_le0.
+apply/lee_addgt0Pr => _ /posnumP[e]; rewrite add0e.
+have [N F5e] : exists N, \sum_(N <= n <oo) \esum_(i in F n) mu (closure (B i)) <
+    5%:R^-1%:E * e%:num%:E.
+  pose f n := \bigcup_(i in F n) closure (B i).
+  have foo : \sum_(k <oo) (mu \o f) k < +oo.
+    rewrite /f /= [ltLHS](_ : _ =
+      \sum_(n <oo) \esum_(i in F n) mu (closure (B i))); last first.
+    apply: (@eq_eseriesr _
+        (fun k => mu (\bigcup_(i in F k) closure (B i)))) => i _.
+      rewrite measure_bigcup//=.
+      - by rewrite nneseries_esum// set_mem_set.
+      - by move=> j D'ij; exact: measurable_closure.
+      - by apply: sub_trivIset tDB => // x [[]].
+    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 _; exact: measurable_closure.
+    + by apply: sub_trivIset tDB => // x [].
+  have : \sum_(N <= k <oo) (mu \o f) k @[N --> \oo] --> 0.
+    exact: nneseries_tail_cvg.
+  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.
+  move=> /[swap] /[apply].
+  rewrite near_map => -[N _]/(_ _ (leqnn N)) h; exists N; move: h.
+  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.
+    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 _; 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.
+  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) 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.
+      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 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.
+        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//.
+        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//.
+      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)].
+    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].
+    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 <oo) \esum_(i in F m) mu (closure (5%:R *` B i)).
+  apply: (@le_trans _ _ (mu (\bigcup_(i in ~` `I_N)
+      \bigcup_(j in F i) closure (5%:R *` B j)))).
+    exact: le_outer_measure.
+  apply: (@le_trans _ _ (\sum_(N <= i <oo) mu
+                           (\bigcup_(j in F i) closure (5%:R *` B j)))).
+    apply: measure_sigma_sub_additive_tail => //.
+      move=> n; apply: bigcup_measurable => k _.
+      by apply: measurable_closure; exact: is_scale_ball.
+    apply: bigcup_measurable => k _; apply: bigcup_measurable => k' _.
+    by apply: measurable_closure; exact: is_scale_ball.
+  apply: lee_nneseries => // n _.
+  rewrite -[in leRHS](set_mem_set (F n)) -nneseries_esum// bigcup_mkcond.
+  rewrite eseries_mkcond [leRHS](_ : _ = \sum_(i <oo) mu
+      (if i \in F n then closure (5%:R *` B i) else set0)); last first.
+    congr (lim _); apply/funext => x.
+    by under [RHS]eq_bigr do rewrite (fun_if mu) measure0.
+  apply: measure_sigma_sub_additive => //.
+  + move=> m; case: ifPn => // _.
+    by apply: measurable_closure; exact: is_scale_ball.
+  + apply: bigcup_measurable => k _; case: ifPn => // _.
+    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.
+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 (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.