proposition: Theorem dominated_convergence : [/\ mu.-integrable D f, [sequence \int[mu]_(x in D) (g_ n x)]_n @ \oo --> 0 & [sequence \int[mu]_(x in D) (f_ n x)]_n @ \oo --> \int[mu]_(x in D) (f x) ].
proof: Proof. have [N1 [mN1 N10 subN1]] := f_f. have [N2 [mN2 N20 subN2]] := f_g. have [N3 [mN3 N30 subN3]] := integrable_ae mD ig. pose N := N1 `|` N2 `|` N3. have mN : measurable N by apply: measurableU => //; exact: measurableU. have N0 : mu N = 0. by rewrite null_set_setU// ?null_set_setU//; exact: measurableU. pose f' := f \_ (D `\` N); pose g' := g \_ (D `\` N). pose f_' := fun n => f_ n \_ (D `\` N). have f_f' x : D x -> f_' ^~ x @ \oo --> f' x. move=> Dx; rewrite /f_' /f' /restrict in_setD mem_set//=. have [/= xN|/= xN] := boolP (x \in N); first exact: cvg_cst. apply: contraPP (xN) => h; apply/negP; rewrite negbK inE; left; left. by apply: subN1 => /= /(_ Dx); exact: contra_not h. have f_g' n x : D x -> `|f_' n x| <= g' x. move=> Dx; rewrite /f_' /g' /restrict in_setD mem_set//=. have [/=|/= xN] := boolP (x \in N); first by rewrite normr0. apply: contrapT => fg; move: xN; apply/negP; rewrite negbK inE; left; right. by apply: subN2 => /= /(_ n Dx). have mu_ n : measurable_fun D (f_' n). apply/(measurable_restrict (f_ n) (measurableD mD mN) _ _).1 => //. by apply: measurable_funS (mf_ _) => // x []. have ig' : mu.-integrable D g'. apply: (integrableS measurableT) => //. apply/(integrable_mkcond g (measurableD mD mN)).1. by apply: integrableS ig => //; exact: measurableD. have finv x : D x -> g' x \is a fin_num. move=> Dx; rewrite /g' /restrict in_setD// mem_set//=. have [//|xN /=] := boolP (x \in N). apply: contrapT => fing; move: xN; apply/negP; rewrite negbK inE; right. by apply: subN3 => /= /(_ Dx). split. - have /integrableP if' : mu.-integrable D f'. exact: (dominated_integrable _ f_' _ g'). apply/integrableP; split => //. move: if' => [?]; apply: le_lt_trans. rewrite le_eqVlt; apply/orP; left; apply/eqP/ae_eq_integral => //; [exact: measurableT_comp|exact: measurableT_comp|]. exists N; split => //; rewrite -(setCK N); apply: subsetC => x Nx Dx. by rewrite /f' /restrict mem_set. - have := @dominated_cvg0 _ _ _ _ _ mD _ _ _ mu_ f_f' finv ig' f_g'. set X := (X in _ -> X @ \oo --> _). rewrite [X in X @ \oo --> _ -> _](_ : _ = X) //. apply/funext => n; apply: ae_eq_integral => //. + apply: measurableT_comp => //; apply: emeasurable_funB => //. apply/(measurable_restrict _ (measurableD _ _) _ _).1 => //. by apply: (measurable_funS mD) => // x []. + by rewrite /g_; apply: measurableT_comp => //; exact: emeasurable_funB. + exists N; split => //; rewrite -(setCK N); apply: subsetC => x /= Nx Dx. by rewrite /f_' /f' /restrict mem_set. - have := @dominated_cvg _ _ _ _ _ mD _ _ _ mu_ f_f' finv ig' f_g'. set X := (X in _ -> X @ \oo --> _). rewrite [X in X @ \oo --> _ -> _](_ : _ = X) //; last first. apply/funext => n; apply: ae_eq_integral => //. exists N; split => //; rewrite -(setCK N); apply: subsetC => x /= Nx Dx. by rewrite /f_' /restrict mem_set. set Y := (X in _ -> _ --> X); rewrite [X in _ --> X -> _](_ : _ = Y) //. apply: ae_eq_integral => //. apply/(measurable_restrict _ (measurableD _ _) _ _).1 => //. by apply: (measurable_funS mD) => // x []. exists N; split => //; rewrite -(setCK N); apply: subsetC => x /= Nx Dx. by rewrite /f' /restrict mem_set. 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