proposition: Lemma ge0_integralZl_EFin k : (0 <= k)%R -> \int[mu]_(x in D) (k%:E * f1 x) = k%:E * \int[mu]_(x in D) f1 x.
proof: Proof. rewrite integral_mkcond erestrict_scale [in RHS]integral_mkcond => k0. set h1 := f1 \_ D. have h10 x : 0 <= h1 x by apply: erestrict_ge0. have mh1 : measurable_fun setT h1 by apply/(measurable_restrict _ mD). have [g [nd_g gh1]] := approximation measurableT mh1 (fun x _ => h10 x). pose kg := fun n => scale_nnsfun (g n) k0. rewrite (@nd_ge0_integral_lim _ _ _ mu (fun x => k%:E * h1 x) kg). - rewrite (_ : _ \o _ = fun n => sintegral mu (scale_nnsfun (g n) k0))//. rewrite (_ : (fun _ => _) = (fun n => k%:E * sintegral mu (g n))). rewrite limeMl //; last first. by apply: is_cvg_sintegral => // x m n mn; apply/(lef_at x nd_g). by rewrite -(nd_ge0_integral_lim mu h10) // => x; [exact/(lef_at x nd_g)|exact: gh1]. by under eq_fun do rewrite (sintegralrM mu k (g _)). - by move=> t; rewrite mule_ge0. - by move=> x m n mn; rewrite /kg ler_pM//; exact/lefP/nd_g. - move=> x. rewrite [X in X @ \oo --> _](_ : _ = (fun n => k%:E * (g n x)%:E)) ?funeqE//. by apply: cvgeMl => //; exact: gh1. 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