proposition: Lemma measurable_fun_xsection_integral (l : X -> {measure set Y -> \bar R}) (k_ : ({nnsfun [the measurableType _ of X * Y] >-> R})^nat) (ndk_ : nondecreasing_seq (k_ : (X * Y -> R)^nat)) (k_k : forall z, (k_ n z)%:E @[n --> \oo] --> k z) : (forall n r, measurable_fun [set: X] (fun x => l x (xsection (k_ n @^-1` [set r]) x))) -> measurable_fun [set: X] (fun x => \int[l x]_y k (x, y)).
proof: Proof. move=> h. rewrite (_ : (fun x => _) = (fun x => limn_esup (fun n => \int[l x]_y (k_ n (x, y))%:E))); last first. apply/funext => x. transitivity (lim (\int[l x]_y (k_ n (x, y))%:E @[n --> \oo])); last first. rewrite is_cvg_limn_esupE//. apply: ereal_nondecreasing_is_cvgn => m n mn. apply: ge0_le_integral => //. - by move=> y _; rewrite lee_fin. - exact/EFin_measurable_fun/measurableT_comp. - by move=> y _; rewrite lee_fin. - exact/EFin_measurable_fun/measurableT_comp. - by move=> y _; rewrite lee_fin; exact/lefP/ndk_. rewrite -monotone_convergence//. - by apply: eq_integral => y _; apply/esym/cvg_lim => //; exact: k_k. - by move=> n; exact/EFin_measurable_fun/measurableT_comp. - by move=> n y _; rewrite lee_fin. - by move=> y _ m n mn; rewrite lee_fin; exact/lefP/ndk_. apply: measurable_fun_limn_esup => n. rewrite [X in measurable_fun _ X](_ : _ = (fun x => \int[l x]_y (\sum_(r \in range (k_ n)) r * \1_(k_ n @^-1` [set r]) (x, y))%:E)); last first. by apply/funext => x; apply: eq_integral => y _; rewrite fimfunE. rewrite [X in measurable_fun _ X](_ : _ = (fun x => \sum_(r \in range (k_ n)) (\int[l x]_y (r * \1_(k_ n @^-1` [set r]) (x, y))%:E))); last first. apply/funext => x; rewrite -ge0_integral_fsum//. - by apply: eq_integral => y _; rewrite -fsumEFin. - move=> r. apply/EFin_measurable_fun/measurableT_comp => [//|]. exact/measurableT_comp. - by move=> m y _; rewrite nnfun_muleindic_ge0. apply: emeasurable_fun_fsum => // r. rewrite [X in measurable_fun _ X](_ : _ = fun x => r%:E * \int[l x]_y (\1_(k_ n @^-1` [set r]) (x, y))%:E); last first. apply/funext => x; under eq_integral do rewrite EFinM. have [r0|r0] := leP 0%R r. rewrite ge0_integralZl//; last by move=> *; rewrite lee_fin. exact/EFin_measurable_fun/measurableT_comp. rewrite integral0_eq; last first. by move=> y _; rewrite preimage_nnfun0// indic0 mule0. by rewrite integral0_eq ?mule0// => y _; rewrite preimage_nnfun0// indic0. apply/measurable_funeM. rewrite (_ : (fun x => _) = (fun x => l x (xsection (k_ n @^-1` [set r]) x))). exact/h. apply/funext => x; rewrite integral_indic//; last first. rewrite (_ : (fun x => _) = xsection (k_ n @^-1` [set r]) x). exact: measurable_xsection. by rewrite /xsection; apply/seteqP; split=> y/= /[!inE]. congr (l x _); apply/funext => y1/=; rewrite /xsection/= inE. by apply/propext; tauto. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology normedtype sequences esum measure numfun lebesgue_measure lebesgue_integral