proposition: Lemma sub_caratheodory : (d.-measurable).-sigma.-measurable `<=` mu^*.-cara.-measurable.
proof: Proof. suff: <<s d.-ring.-measurable >> `<=` mu^*.-cara.-measurable. by apply: subset_trans; apply: sub_smallest2r => //; exact: sub_smallest. apply: smallest_sub. split => //; [by move=> X mX; rewrite setTD; exact: measurableC | by move=> u_ mu_; exact: bigcupT_measurable]. move=> A mA; apply le_caratheodory_measurable => // X. apply lb_ereal_inf => _ [B [mB XB] <-]. rewrite -(eq_eseriesr (fun _ _ => SetRing.RmuE _ (mB _))) => //. have RmB i : measurable (B i : set rT) by exact: sub_gen_smallest. set BA := eseries (fun n => Rmu (B n `&` A)). set BNA := eseries (fun n => Rmu (B n `&` ~` A)). apply: (@le_trans _ _ (limn BA + limn BNA)); [apply: leeD|]. - rewrite (_ : BA = eseries (fun n => mu_ext mu (B n `&` A))); last first. rewrite funeqE => n; apply: eq_bigr => k _. by rewrite /= measurable_Rmu_extE //; exact: measurableI. apply: (@le_trans _ _ (mu_ext mu (\bigcup_k (B k `&` A)))). by apply: le_mu_ext; rewrite -setI_bigcupl; exact: setISS. exact: outer_measure_sigma_subadditive. - rewrite (_ : BNA = eseries (fun n => mu_ext mu (B n `\` A))); last first. rewrite funeqE => n; apply: eq_bigr => k _. by rewrite /= measurable_Rmu_extE //; exact: measurableD. apply: (@le_trans _ _ (mu_ext mu (\bigcup_k (B k `\` A)))). by apply: le_mu_ext; rewrite -setI_bigcupl; exact: setISS. exact: outer_measure_sigma_subadditive. have ? : cvg (BNA @ \oo) by exact: is_cvg_nneseries. have ? : cvg (BA @ \oo) by exact: is_cvg_nneseries. have ? : cvg (eseries (Rmu \o B) @ \oo) by exact: is_cvg_nneseries. have [def|] := boolP (lim (BA @ \oo) +? lim (BNA @ \oo)); last first. rewrite /adde_def negb_and !negbK=> /orP[/andP[BAoo BNAoo]|/andP[BAoo BNAoo]]. - suff -> : limn (eseries (Rmu \o B)) = +oo by rewrite leey. apply/eqP; rewrite -leye_eq -(eqP BAoo); apply/lee_lim => //. near=> n; apply: lee_sum => m _; apply: le_measure; rewrite /mkset; by [rewrite inE; exact: measurableI | rewrite inE | apply: subIset; left]. - suff -> : limn (eseries (Rmu \o B)) = +oo by rewrite leey. apply/eqP; rewrite -leye_eq -(eqP BNAoo); apply/lee_lim => //. by near=> n; apply: lee_sum => m _; rewrite -setDE; apply: le_measure; rewrite /mkset ?inE//; apply: measurableD. rewrite -limeD // (_ : (fun _ => _) = eseries (fun k => Rmu (B k `&` A) + Rmu (B k `&` ~` A))); last first. by rewrite funeqE => n; rewrite -big_split /=; exact: eq_bigr. apply/lee_lim => //. by apply/is_cvg_nneseries => // n _; exact: adde_ge0. near=> n; apply: lee_sum => i _; rewrite -measure_semi_additive2. - apply: le_measure; rewrite /mkset ?inE//; [|by rewrite -setIUr setUCr setIT]. by apply: measurableU; [exact:measurableI|rewrite -setDE; exact:measurableD]. - exact: measurableI. - by rewrite -setDE; exact: measurableD. - by apply: measurableU; [exact:measurableI|rewrite -setDE; exact:measurableD]. - by rewrite setIACA setICr setI0. 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)