proposition: Lemma ge0_le_integral : (forall x, D x -> f1 x <= f2 x) -> \int[mu]_(x in D) f1 x <= \int[mu]_(x in D) f2 x.
proof: Proof. move=> f12; rewrite !(integral_mkcond D). 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 h12 x : h1 x <= h2 x by apply: lee_restrict. have [g1 [nd_g1 /(_ _ Logic.I)gh1]] := approximation measurableT mh1 (fun x _ => h10 _). rewrite (nd_ge0_integral_lim _ h10 (fun x => lef_at x nd_g1) gh1)//. apply: lime_le. by apply: is_cvg_sintegral => // t Dt; exact/(lef_at t nd_g1). near=> n; rewrite ge0_integralTE//; apply: ereal_sup_ub => /=. exists (g1 n) => // t; rewrite (le_trans _ (h12 _)) //. have := gh1 t. have := leey (h1 t); rewrite le_eqVlt => /predU1P[->|ftoo]. by rewrite leey. have h1tfin : h1 t \is a fin_num. by rewrite fin_numE gt_eqF/= ?lt_eqF// (lt_le_trans _ (h10 t)). have := gh1 t. rewrite -(fineK h1tfin) => /fine_cvgP[ft_near]. set u_ := (X in X --> _) => u_h1 g1h1. have <- : lim u_ = fine (h1 t) by exact/cvg_lim. rewrite lee_fin; apply: nondecreasing_cvgn_le. by move=> // a b ab; rewrite /u_ /=; exact/lefP/nd_g1. by apply/cvg_ex; eexists; exact: u_h1. 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