proposition: Lemma lebesgue_nearly_bounded (D : set R) (eps : R) : measurable D -> mu D < +oo -> (0 < eps)%R -> exists ab : R * R, mu (D `\` [set` `[ab.1,ab.2]]) < eps%:E.
proof: Proof. move=> mD Dfin epspos; pose Dn n := D `&` [set` `[-(n%:R), n%:R]]%R. have mDn n : measurable (Dn n) by exact: measurableI. have : mu \o Dn @ \oo --> mu (\bigcup_n Dn n). apply: nondecreasing_cvg_mu => //. - by apply: bigcup_measurable => // ? _; exact: mDn. - move=> n m nm; apply/subsetPset; apply: setIS => z /=; rewrite !in_itv/=. move=> /andP[nz zn]; rewrite (le_trans _ nz)/= ?(le_trans zn) ?ler_nat//. by rewrite lerNl opprK ler_nat. rewrite -setI_bigcupr; rewrite bigcup_itvT setIT. have finDn n : mu (Dn n) \is a fin_num. rewrite ge0_fin_numE// (le_lt_trans _ Dfin)//. by rewrite le_measure// ?inE//=; [exact: mDn|exact: subIsetl]. have finD : mu D \is a fin_num by rewrite fin_num_abs gee0_abs. rewrite -[mu D]fineK// => /fine_cvg/(_ (interior (ball (fine (mu D)) eps)))[]. exact/nbhs_interior/nbhsx_ballx. move=> n _ /(_ _ (leqnn n))/interior_subset muDN. exists (-n%:R, n%:R)%R; rewrite measureD//=. move: muDN; rewrite /ball/= /ereal_ball/= -fineB//=; last exact: finDn. rewrite -lte_fin; apply: le_lt_trans. have finDDn : mu D - mu (Dn n) \is a fin_num by rewrite ?fin_numB ?finD /= ?(finDn n). rewrite -fine_abse // gee0_abs ?sube_ge0 ?finD ?(finDn _) //. by rewrite -[_ - _]fineK // lte_fin fine. by rewrite le_measure// ?inE//; [exact: measurableI |exact: subIsetl]. 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