proposition: Lemma lebesgue_regularity_inner (D : set R) (eps : R) : measurable D -> mu D < +oo -> (0 < eps)%R -> exists V : set R, [/\ compact V , V `<=` D & mu (D `\` V) < eps%:E].
proof: Proof. move=> mD finD epspos. wlog : eps epspos D mD finD / exists ab : R * R, D `<=` `[ab.1, ab.2]%classic. move=> WL; have [] := @lebesgue_nearly_bounded _ (eps / 2)%R mD finD. by rewrite divr_gt0. case=> a b /= muDabe; have [] := WL (eps / 2) _ (D `&` `[a,b]). - by rewrite divr_gt0. - exact: measurableI. - by rewrite (le_lt_trans _ finD)// le_measure// inE//; exact: measurableI. - by exists (a, b). move=> V [/= cptV VDab Dabeps2]; exists (V `&` `[a, b]); split. - apply: (subclosed_compact _ cptV) => //; apply: closedI. by apply: compact_closed => //; exact: Rhausdorff. exact: interval_closed. - by move=> ? [/VDab []]. rewrite setDIr (setU_id2r ((D `&` `[a, b]) `\` V)); last first. move=> z ; rewrite setDE setCI setCK => -[?|?]; by apply/propext; split => [[]|[[]]]. have mV : measurable V. by apply: closed_measurable; apply: compact_closed => //; exact: Rhausdorff. rewrite [eps]splitr EFinD (measureU mu) // ?lteD //. - by apply: measurableD => //; exact: measurableI. - exact: measurableD. - by rewrite eqEsubset; split => z // [[[_ + _] [_]]]. case=> -[a b] /= Dab; pose D' := `[a,b] `\` D. have mD' : measurable D' by exact: measurableD. have [] := lebesgue_regularity_outer mD' _ epspos. rewrite (@le_lt_trans _ _ (mu `[a,b]%classic))//. by rewrite le_measure ?inE//; exact: subIsetl. by rewrite /= lebesgue_measure_itv/= -EFinD -(fun_if EFin) ltry. move=> U [oU /subsetC + mDeps]; rewrite setCI setCK => nCD'. exists (`[a, b] `&` ~` U); split. - apply: (subclosed_compact _ (@segment_compact _ a b)) => //. by apply: closedI; [exact: interval_closed | exact: open_closedC]. - by move=> z [abz] /nCD'[]. - rewrite setDE setCI setIUr setCK. rewrite [_ `&` ~` _ ](iffRL (disjoints_subset _ _)) ?setCK // set0U. move: mDeps; rewrite /D' ?setDE setCI setIUr setCK [U `&` D]setIC. move => /(le_lt_trans _); apply; apply: le_measure; last by move => ?; right. by rewrite inE; apply: measurableI => //; exact: open_measurable. rewrite inE; apply: measurableU. by apply: measurableI; [exact: open_measurable|exact: measurableC]. by apply: measurableI => //; exact: open_measurable. 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