proposition: Lemma approximation_sfun_integrable (f : T -> \bar R): mu.-integrable E f -> exists g_ : {sfun T >-> R}^nat, [/\ forall n, mu.-integrable E (EFin \o g_ n), forall x, E x -> EFin \o g_^~ x @ \oo --> f x & (fun n => \int[mu]_(z in E) `|f z - (g_ n z)%:E|) @ \oo --> 0].
proof: Proof. move=> intf. have [//|p_ [intp pf pl1]] := sfun_dense_L1_pos (integrable_funepos mE intf). have [//|n_ [intn nf nl1]] := sfun_dense_L1_pos (integrable_funeneg mE intf). exists (fun n => p_ n - n_ n)%R; split. - move=> n; rewrite /comp; under eq_fun => ? do rewrite sfunB /= EFinB. by apply: integrableB => //; [exact: intp | exact: intn]. - move=> ? ?; rewrite /comp; under eq_fun => ? do rewrite sfunB /= EFinB. rewrite [f]funeposneg; apply: cvgeB => //;[|exact: pf|exact:nf]. exact: add_def_funeposneg. have fpn z n : f z - ((p_ n - n_ n) z)%:E = (f^\+ z - (p_ n z)%:E) - (f^\- z - (n_ n z)%:E). rewrite sfunB EFinB fin_num_oppeB // {1}[f]funeposneg -addeACA. by congr (_ _); rewrite fin_num_oppeB. case/integrableP: (intf) => mf _. have mfpn n : mu.-integrable E (fun z => f z - ((p_ n - n_ n) z)%:E). under eq_fun => ? do rewrite fpn; apply: integrableB => //. by apply: integrableB => //; [exact: integrable_funepos | exact: intp]. by apply: integrableB => //; [exact: integrable_funeneg | exact: intn]. apply/fine_cvgP; split => //. near=> N; case/integrableP: (mfpn N) => _; rewrite ge0_fin_numE //. exact: integral_ge0. apply/cvg_ballP=> _/posnumP[eps]; have e2p : (0 < eps%:num/2)%R by []. case/fine_cvgP: pl1 => + /cvg_ballP/(_ _ e2p); apply: filter_app2. case/fine_cvgP: nl1 => + /cvg_ballP/(_ _ e2p); apply: filter_app2. near=> n; rewrite /ball /=; do 3 rewrite distrC subr0. move=> finfn ne2 finfp pe2; rewrite [_%:num]splitr. rewrite (le_lt_trans _ (ltrD pe2 ne2))// (le_trans _ (ler_normD _ _))//. under [fun z => _ (f^\+ z + _)]eq_fun => ? do rewrite EFinN. under [fun z => _ (f^\- z + _)]eq_fun => ? do rewrite EFinN. have mfp : mu.-integrable E (fun z => `|f^\+ z - (p_ n z)%:E|). apply/integrable_abse/integrableB => //; first exact: integrable_funepos. exact: intp. have mfn : mu.-integrable E (fun z => `|f^\- z - (n_ n z)%:E|). apply/integrable_abse/integrableB => //; first exact: integrable_funeneg. exact: intn. rewrite -[x in (_ <= `|x|)%R]fineD // -integralD //. rewrite !ger0_norm ?fine_ge0 ?integral_ge0 ?fine_le//. - by apply: integral_fune_fin_num => //; exact/integrable_abse/mfpn. - by apply: integral_fune_fin_num => //; exact: integrableD. - apply: ge0_le_integral => //. + by apply: measurableT_comp => //; case/integrableP: (mfpn n). + by move=> x Ex; rewrite adde_ge0. + by apply: emeasurable_funD; [move: mfp | move: mfn]; case/integrableP. + by move=> ? ?; rewrite fpn; exact: lee_abs_sub. + by move=> x Ex; rewrite adde_ge0. Unshelve. all: by end_near. 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