proposition: Lemma mu_ext_sigma_subadditive : sigma_subadditive mu^*.
proof: Proof. move=> A; have [[i ioo]|] := pselect (exists i, mu^* (A i) = +oo). rewrite (eseries_pinfty _ _ ioo) ?leey// => n _. by rewrite -ltNye (lt_le_trans _ (mu_ext_ge0 _)). rewrite -forallNE => Aoo. suff add2e (e : {posnum R}) : mu^* (\bigcup_n A n) <= \sum_(i <oo) mu^* (A i) + e%:num%:E. by apply/lee_addgt0Pr => _/posnumP[]. rewrite (le_trans _ (epsilon_trick _ _ _))//; last first. by move=> n; exact: mu_ext_ge0. pose P n (B : (set T)^nat) := measurable_cover (A n) B /\ \sum_(k <oo) mu (B k) <= mu^* (A n) + (e%:num / (2 ^ n.+1)%:R)%:E. have [G PG] : {G : ((set T)^nat)^nat & forall n, P n (G n)}. apply: (@choice _ _ P) => n; rewrite /P /mu_ext. set S := (X in ereal_inf X); move infS : (ereal_inf S) => iS. case: iS infS => [r Sr|Soo|Soo]. - have en1 : (0 < e%:num / (2 ^ n.+1)%:R)%R by []. have /(lb_ereal_inf_adherent en1) : ereal_inf S \is a fin_num by rewrite Sr. move=> [x [B [mB AnB muBx] xS]]. by exists B; split => //; rewrite muBx -Sr; exact/ltW. - by have := Aoo n; rewrite /mu^* Soo. - suff : lbound S 0 by move/lb_ereal_inf; rewrite Soo. by move=> /= _ [B [mB AnB] <-]; exact: nneseries_ge0. have muG_ge0 x : 0 <= (mu \o uncurry G) x by exact: measure_ge0. apply: (@le_trans _ _ (\esum_(i in setT) (mu \o uncurry G) i)). rewrite /mu_ext; apply: ereal_inf_lb => /=. have /card_esym/ppcard_eqP[f] := card_nat2. exists (uncurry G \o f). split => [i|]; first exact/measurable_uncurry/(PG (f i).1).1.1. apply: (@subset_trans _ (\bigcup_n \bigcup_k G n k)) => [t [i _]|]. by move=> /(cover_subset (PG i).1) -[j _ ?]; exists i => //; exists j. move=> t [i _ [j _ Bijt]]; exists (f^-1%FUN (i, j)) => //=. by rewrite invK ?inE. rewrite -(esum_pred_image (mu \o uncurry G) _ xpredT) ?[fun=> _]set_true//. by rewrite image_eq. rewrite (_ : esum _ _ = \sum_(i <oo) \sum_(j <oo ) mu (G i j)); last first. pose J : nat -> set (nat * nat) := fun i => [set (i, j) | j in setT]. rewrite (_ : setT = \bigcup_k J k); last first. by rewrite predeqE => -[a b]; split => // _; exists a => //; exists b. rewrite esum_bigcupT /=; last 2 first. - apply/trivIsetP => i j _ _ ij. rewrite predeqE => -[n m] /=; split => //= -[] [_] _ [<-{n} _]. by move=> [m' _] [] /esym/eqP; rewrite (negbTE ij). - by move=> /= [n m]; apply: measure_ge0; exact: (cover_measurable (PG n).1). rewrite -(image_id [set: nat]) -fun_true esum_pred_image//; last first. by move=> n _; exact: esum_ge0. apply: eq_eseriesr => /= j _. rewrite -(esum_pred_image (mu \o uncurry G) (pair j) predT)//=; last first. by move=> ? ? _ _; exact: (@can_inj _ _ _ snd). by congr esum; rewrite predeqE => -[a b]; split; move=> [i _ <-]; exists i. apply: lee_lim. - apply: is_cvg_nneseries => n _. by apply: nneseries_ge0 => m _; exact: (muG_ge0 (n, m)). - by apply: is_cvg_nneseries => n _; apply: adde_ge0 => //; exact: mu_ext_ge0. - by near=> n; apply: lee_sum => i _; exact: (PG i).2. Unshelve. all: by end_near. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) reals ereal signed topology normedtype sequences esum numfun HB(structures)