proposition: Lemma ge0_integralD : \int[mu]_(x in D) (f1 x + f2 x) = \int[mu]_(x in D) f1 x + \int[mu]_(x in D) f2 x.
proof: Proof. rewrite !(integral_mkcond D) erestrictD. set h1 := f1 \_ D; set h2 := f2 \_ D. have h10 x : 0 <= h1 x by apply: erestrict_ge0. have h20 x : 0 <= h2 x by apply: erestrict_ge0. have mh1 : measurable_fun setT h1 by apply/(measurable_restrict _ mD). have mh2 : measurable_fun setT h2 by apply/(measurable_restrict _ mD). have [g1 [nd_g1 gh1]] := approximation measurableT mh1 (fun x _ => h10 x). have [g2 [nd_g2 gh2]] := approximation measurableT mh2 (fun x _ => h20 x). pose g12 := fun n => add_nnsfun (g1 n) (g2 n). rewrite (@nd_ge0_integral_lim _ _ _ mu _ g12) //; last 3 first. - by move=> x; rewrite adde_ge0. - by apply: nondecreasing_seqD => // x; [exact/(lef_at x nd_g1)|exact/(lef_at x nd_g2)]. - move=> x; rewrite (_ : _ \o _ = (fun n => (g1 n x)%:E + (g2 n x)%:E))//. apply: cvgeD => //; [|exact: gh1|exact: gh2]. by apply: ge0_adde_def => //; rewrite !inE; [exact: h10|exact: h20]. under [_ \o _]eq_fun do rewrite sintegralD. rewrite (nd_ge0_integral_lim _ _ (fun x => lef_at x nd_g1)) //; last first. by move=> x; exact: gh1. rewrite (nd_ge0_integral_lim _ _ (fun x => lef_at x nd_g2)) //; last first. by move=> x; exact: gh2. rewrite limeD //. by apply: is_cvg_sintegral => // x Dx; exact/(lef_at x nd_g1). by apply: is_cvg_sintegral => // x Dx; exact/(lef_at x nd_g2). rewrite ge0_adde_def => //; rewrite inE; apply: lime_ge. - by apply: is_cvg_sintegral => // x Dx; exact/(lef_at x nd_g1). - by apply: nearW => n; exact: sintegral_ge0. - by apply: is_cvg_sintegral => // x Dx; exact/(lef_at x nd_g2). - by apply: nearW => n; exact: sintegral_ge0. 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