proposition: Lemma ge0_integralZl k : (forall x, D x -> 0 <= f x) -> 0 <= k -> \int[mu]_(x in D) (k * f x) = k * \int[mu]_(x in D) (f x).
proof: Proof. move=> f0; move: k => [k|_|//]; first exact: ge0_integralZl_EFin. pose g : (T -> \bar R)^nat := fun n x => n%:R%:E * f x. have mg n : measurable_fun D (g n) by apply: measurable_funeM. have g0 n x : D x -> 0 <= g n x. by move=> Dx; apply: mule_ge0; [rewrite lee_fin|exact:f0]. have nd_g x : D x -> nondecreasing_seq (g ^~ x). by move=> Dx m n mn; rewrite lee_wpmul2r ?f0// lee_fin ler_nat. pose h := fun x => limn (g^~ x). transitivity (\int[mu]_(x in D) limn (g^~ x)). apply: eq_integral => x Dx; apply/esym/cvg_lim => //. have [fx0|fx0|fx0] := ltgtP 0 (f x). - rewrite gt0_mulye//; apply/cvgeyPgey; near=> M. have M0 : (0 <= M)%R by []. rewrite /g; case: (f x) fx0 => [r r0|_|//]; last first. exists 1%N => // m /= m0. by rewrite mulry gtr0_sg// ?mul1e ?leey// ltr0n. near=> n; rewrite lee_fin -ler_pdivrMr//. near: n; exists `|ceil (M / r)|%N => // m /=. rewrite -(ler_nat R); apply: le_trans. by rewrite natr_absz ger0_norm ?ceil_ge// ceil_ge0// divr_ge0// ?ltW. - rewrite lt0_mulye//; apply/cvgeNyPleNy; near=> M; have M0 : (M <= 0)%R by []. rewrite /g; case: (f x) fx0 => [r r0|//|_]; last first. exists 1%N => // m /= m0. by rewrite mulrNy gtr0_sg// ?ltr0n// mul1e ?leNye. near=> n; rewrite lee_fin -ler_ndivrMr//. near: n; exists `|ceil (M / r)|%N => // m /=. rewrite -(ler_nat R); apply: le_trans. rewrite natr_absz ger0_norm ?ceil_ge// ceil_ge0// -mulrNN. by rewrite mulr_ge0// lerNr oppr0// ltW// invr_lt0. - rewrite -fx0 mule0 /g -fx0. under eq_fun do rewrite mule0/=. exact: cvg_cst. rewrite (monotone_convergence mu mD mg g0 nd_g). under eq_fun do rewrite /g ge0_integralZl_EFin//. have : 0 <= \int[mu]_(x in D) f x by exact: integral_ge0. rewrite le_eqVlt => /predU1P[<-|if_gt0]. by rewrite mule0; under eq_fun do rewrite mule0; rewrite lim_cst. rewrite gt0_mulye//; apply/cvg_lim => //; apply/cvgeyPgey; near=> M. have M0 : (0 <= M)%R by []. near=> n; have [ifoo|] := ltP (\int[mu]_(x in D) f x) +oo; last first. rewrite leye_eq => /eqP ->; rewrite mulry muleC gt0_mulye ?leey//. by near: n; exists 1%N => // n /= n0; rewrite gtr0_sg// ?lte_fin// ltr0n. rewrite -(@fineK _ (\int[mu]_(x in D) f x)); last first. by rewrite fin_numElt ifoo (le_lt_trans _ if_gt0). rewrite -lee_pdivr_mulr//; last first. by move: if_gt0 ifoo; case: (\int[mu]_(x in D) f x). near: n. exists `|ceil (M * (fine (\int[mu]_(x in D) f x))^-1)|%N => //. move=> n /=; rewrite -(@ler_nat R) -lee_fin; apply: le_trans. rewrite lee_fin natr_absz ger0_norm ?ceil_ge// ceil_ge0//. by rewrite mulr_ge0// ?invr_ge0//; exact/fine_ge0/integral_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