proposition: Lemma monotone_convergence : \int[mu]_(x in D) (f' x) = limn (fun n => \int[mu]_(x in D) (g' n x)).
proof: Proof. rewrite integral_mkcond. under [in RHS]eq_fun do rewrite integral_mkcond -/(g _). have -> : f' \_ D = f. apply/funext => x; rewrite /f /f' /g /patch /=; case: ifPn => //=. by rewrite lim_cst. apply/eqP; rewrite eq_le; apply/andP; split; last first. have nd_int_g : nondecreasing_seq (fun n => \int[mu]_x g n x). move=> m n mn; apply: ge0_le_integral => //. by move=> *; exact: nd_g. have ub n : \int[mu]_x g n x <= \int[mu]_x f x. apply: ge0_le_integral => //. - move=> x _; apply: lime_ge => //. by apply: nearW => k; exact/g0. - apply: emeasurable_fun_cvg mg _ => x _. exact: ereal_nondecreasing_is_cvgn. - move=> x Dx; apply: lime_ge => //. near=> m; have nm : (n <= m)%N by near: m; exists n. exact/nd_g. by apply: lime_le => //; [exact:ereal_nondecreasing_is_cvgn|exact:nearW]. rewrite (@nd_ge0_integral_lim _ _ _ mu _ max_g2) //; last 2 first. - move=> t; apply: lime_ge => //. by apply: nearW => n; exact: g0. - by move=> t m n mn; exact/lefP/nd_max_g2. apply: lee_lim. - by apply: is_cvg_sintegral => // t m n mn; exact/lefP/nd_max_g2. - apply: ereal_nondecreasing_is_cvgn => // n m nm; apply: ge0_le_integral => //. by move=> *; exact/nd_g. - apply: nearW => n; rewrite ge0_integralTE//. by apply: ereal_sup_ub; exists (max_g2 n) => // t; exact: max_g2_g. 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