proposition: Lemma nd_ge0_integral_lim : \int[mu]_x f x = limn (sintegral mu \o g).
proof: Proof. rewrite ge0_integralTE//. apply/eqP; rewrite eq_le; apply/andP; split; last first. apply: lime_le; first exact: is_cvg_sintegral. near=> n; apply: ereal_sup_ub; exists (g n) => //= => x. have <- : limn (EFin \o g ^~ x) = f x by apply/cvg_lim => //; exact: gf. have : EFin \o g ^~ x @ \oo --> ereal_sup (range (EFin \o g ^~ x)). by apply: ereal_nondecreasing_cvgn => p q pq /=; rewrite lee_fin; exact/nd_g. by move/cvg_lim => -> //; apply: ereal_sup_ub; exists n. have := leey (\int[mu]_x (f x)). rewrite le_eqVlt => /predU1P[|] mufoo; last first. have : \int[mu]_x (f x) \is a fin_num by rewrite ge0_fin_numE// integral_ge0. rewrite ge0_integralTE// => /ub_ereal_sup_adherent h. apply/lee_addgt0Pr => _/posnumP[e]. have {h} [/= _ [G Gf <-]] := h _ [gt0 of e%:num]. rewrite EFinN lte_subl_addr// => fGe. have : forall x, cvgn (g^~ x) -> (G x <= limn (g ^~ x))%R. move=> x cg; rewrite -lee_fin -(EFin_lim cg). by have /cvg_lim gxfx := @gf x; rewrite (le_trans (Gf _))// gxfx. move=> /(nd_sintegral_lim_lemma mu nd_g)/(leeD2r e%:num%:E). by apply: le_trans; exact: ltW. suff : limn (sintegral mu \o g) = +oo. by move=> ->; rewrite -ge0_integralTE// mufoo. apply/eqyP => r r0. have [G [Gf rG]] : exists h : {nnsfun T >-> R}, (forall x, (h x)%:E <= f x) /\ (r%:E <= sintegral mu h). have : r%:E < \int[mu]_x (f x). move: (mufoo) => /eqyP/(_ _ (addr_gt0 r0 r0)). by apply: lt_le_trans => //; rewrite lte_fin ltrDr. rewrite ge0_integralTE// => /ereal_sup_gt[x [/= G Gf Gx rx]]. by exists G; split => //; rewrite (le_trans (ltW rx)) // Gx. have : forall x, cvgn (g^~ x) -> (G x <= limn (g^~ x))%R. move=> x cg; rewrite -lee_fin -(EFin_lim cg). by have /cvg_lim gxfx := @gf x; rewrite (le_trans (Gf _)) // gxfx. by move/(nd_sintegral_lim_lemma mu nd_g) => Gg; rewrite (le_trans rG). 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