proposition: Lemma approximation_continuous_integrable (E : set R) (f : R -> R^o): measurable E -> mu E < +oo -> mu.-integrable E (EFin \o f) -> exists g_ : (rT -> rT)^nat, [/\ forall n, continuous (g_ n), forall n, mu.-integrable E (EFin \o g_ n) & \int[mu]_(z in E) `|(f z - g_ n z)%:E| @[n --> \oo] --> 0].
proof: Proof. move=> mE Efin intf. have mf : measurable_fun E f by case/integrableP : intf => /EFin_measurable_fun. suff apxf eps : exists h : rT -> rT, (eps > 0)%R -> [/\ continuous h, mu.-integrable E (EFin \o h) & \int[mu]_(z in E) `|(f z - h z)%:E| < eps%:E]. pose g_ n := projT1 (cid (apxf n.+1%:R^-1)); exists g_; split. - by move=> n; have [] := projT2 (cid (apxf n.+1%:R^-1)). - by move=> n; have [] := projT2 (cid (apxf n.+1%:R^-1)). apply/cvg_ballP => eps epspos. have /cvg_ballP/(_ eps epspos)[N _ Nball] := @cvge_harmonic rT. exists N => //; apply: (subset_trans Nball) => n. rewrite /ball /= /ereal_ball contract0 !sub0r !normrN => /(lt_trans _); apply. rewrite ?ger0_norm; first last. - by rewrite -le_expandLR // ?inE ?normr0// expand0 integral_ge0. - by rewrite -le_expandLR // ?inE ?normr0// expand0. have [] := projT2 (cid (apxf n.+1%:R^-1)) => // _ _ ipaxfn. by rewrite -lt_expandRL ?contractK// inE contract_le1. have [|] := ltP 0%R eps; last by exists point. move: eps => _/posnumP[eps]. have [g [gfe2 ig]] : exists g : {sfun R >-> rT}, \int[mu]_(z in E) `|(f z - g z)%:E| < (eps%:num / 2)%:E /\ mu.-integrable E (EFin \o g). have [g_ [intG ?]] := approximation_sfun_integrable mE intf. move/fine_fcvg/cvg_ballP/(_ (eps%:num / 2)) => -[] // n _ Nb; exists (g_ n). have fg_fin_num : \int[mu]_(z in E) `|(f z - g_ n z)%:E| \is a fin_num. rewrite integral_fune_fin_num// integrable_abse//. by under eq_fun do rewrite EFinB; apply: integrableB => //; exact: intG. split; last exact: intG. have /= := Nb _ (leqnn n); rewrite /ball/= sub0r normrN -fine_abse// -lte_fin. by rewrite fineK ?abse_fin_num// => /le_lt_trans; apply; exact: lee_abs. have mg : measurable_fun E g. by apply: (measurable_funS measurableT) => //; exact: measurable_funP. have [M Mpos Mbd] : (exists2 M, 0 < M & forall x, `|g x| <= M)%R. have [M [_ /= bdM]] := simple_bounded g. exists (`|M| + 1)%R; first exact: ltr_pwDr. by move=> x; rewrite bdM// ltr_pwDr// ler_norm. have [] // := @measurable_almost_continuous _ _ mE _ g (eps%:num / 2 / (M *+ 2)). by rewrite divr_gt0// mulrn_wgt0. move=> A [cptA AE /= muAE ctsAF]. have [] := continuous_bounded_extension _ _ Mpos ctsAF. - exact: pseudometric_normal. - by apply: compact_closed => //; exact: Rhausdorff. - by move=> ? ?; exact: Mbd. have mA : measurable A := compact_measurable cptA. move=> h [gh ctsh hbdM]; have mh : measurable_fun E h. by apply: subspace_continuous_measurable_fun=> //; exact: continuous_subspaceT. have intg : mu.-integrable E (EFin \o h). apply: measurable_bounded_integrable => //. exists M; split; rewrite ?num_real // => x Mx y _ /=. by rewrite (le_trans _ (ltW Mx)). exists h; split => //; rewrite [eps%:num]splitr; apply: le_lt_trans. pose fgh x := `|(f x - g x)%:E| + `|(g x - h x)%:E|. apply: (@ge0_le_integral _ _ _ mu _ mE _ fgh) => //. - apply: (measurable_funS mE) => //; do 2 apply: measurableT_comp => //. exact: measurable_funB. - by move=> z _; rewrite adde_ge0. - apply: measurableT_comp => //; apply: measurable_funD => //; apply: (measurable_funS mE) => //; (apply: measurableT_comp => //); exact: measurable_funB. - move=> x _; rewrite -(subrK (g x) (f x)) -(addrA (_ + _)%R) lee_fin. by rewrite ler_normD. rewrite integralD//; first last. - by apply: integrable_abse; under eq_fun do rewrite EFinB; apply: integrableB. - by apply: integrable_abse; under eq_fun do rewrite EFinB; apply: integrableB. rewrite EFinD lteD// -(setDKU AE) integral_setU => //; first last. - by rewrite /disj_set setDKI. - rewrite setDKU //; do 2 apply: measurableT_comp => //. exact: measurable_funB. - exact: measurableD. rewrite (@ae_eq_integral _ _ _ mu A (cst 0)) //; first last. - by apply: aeW => z Az; rewrite (gh z) ?inE// subrr abse0. - apply: (measurable_funS mE) => //; do 2 apply: measurableT_comp => //. exact: measurable_funB. rewrite integral0 adde0. apply: (le_lt_trans (integral_le_bound (M *+ 2)%:E _ _ _ _)) => //. - exact: measurableD. - apply: (measurable_funS mE) => //; apply: measurableT_comp => //. exact: measurable_funB. - by rewrite lee_fin mulrn_wge0// ltW. - apply: aeW => z [Ez _]; rewrite /= lee_fin mulr2n. by rewrite (le_trans (ler_normB _ _))// lerD. by rewrite -lte_pdivl_mull ?mulrn_wgt0// muleC -EFinM. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) signed reals ereal topology normedtype sequences real_interval esum measure lebesgue_measure numfun