proposition: 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: 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_pM2l ?(vitali_collection_partition_ub_gt0 Bset0 VBr Vi)//. by rewrite lef_pV2// ?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_pdivrMr// 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_distD y _ _))// [in leRHS]addrC lerD//. exact: is_ball_closureP. rewrite (le_trans (ler_distD (cpoint (B i)) _ _))//. rewrite (_ : 2 = 1 + 1); last by []. rewrite mulrDl !mul1r// lerD; [by []| |exact: is_ball_closureP]. by rewrite distrC; exact: is_ball_closureP. rewrite -lerBrDr// -(@natr1 _ 4). rewrite (mulrDl 4%:R) mul1r addrK (natrM _ 2 2) -mulrA ler_pM2l//. rewrite (le_trans Birn)// [in leRHS]mulrC -ler_pdivrMr//. by rewrite -mulrA -invfM -natrM -expnSr ltW. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule