proposition: Lemma lebesgue_regularity_inner_sup (D : set R) : measurable D -> mu D = ereal_sup [set mu K | K in [set K | compact K /\ K `<=` D]].
proof: Proof. move=> mD; have [?|] := ltP (mu D) +oo. exact: lebesgue_regularity_innerE_bounded. have /sigma_finiteP [F [RFU Fsub ffin]] := sigma_finiteT (lebesgue_stieltjes_measure (@idfun R)). rewrite leye_eq => /eqP /[dup] + ->. have {1}-> : D = \bigcup_n (F n `&` D) by rewrite -setI_bigcupl -RFU setTI. move=> FDp; apply/esym/eq_infty => M. have : (fun n => mu (F n `&` D)) @ \oo --> +oo. rewrite -FDp; apply: nondecreasing_cvg_mu. - by move=> i; apply: measurableI => //; exact: (ffin i).1. - by apply: bigcup_measurable => i _; exact: (measurableI _ _ (ffin i).1). - by move=> n m nm; apply/subsetPset; apply: setSI; exact/subsetPset/Fsub. move/cvgey_ge => /(_ (M + 1)%R) [N _ /(_ _ (lexx N))]. have [mFN FNoo] := ffin N. have [] := @lebesgue_regularity_inner (F N `&` D) _ _ _ ltr01. - exact: measurableI. - by rewrite (le_lt_trans _ (ffin N).2)//= measureIl. move=> V [/[dup] /compact_measurable mV cptV VFND] FDV1 M1FD. rewrite (@le_trans _ _ (mu V))//; last first. apply: ereal_sup_ub; exists V => //=; split => //. exact: (subset_trans VFND (@subIsetr _ _ _)). rewrite -(@leeD2lE _ 1)// {1}addeC -EFinD (le_trans M1FD)//. rewrite /mu (@measureDI _ _ _ _ (F N `&` D) _ _ mV)/=; last exact: measurableI. rewrite ltW// lte_le_add // ?ge0_fin_numE //; last first. by rewrite measureIr//; apply: measurableI. by rewrite -setIA (le_lt_trans _ (ffin N).2)// measureIl//; exact: measurableI. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology numfun normedtype HB(structures) sequences esum measure real_interval realfun exp lebesgue_stieltjes_measure