proposition: Lemma measurable_prod_subset_xsection_kernel : (forall x, exists M, forall X, measurable X -> kD x X < M%:E) -> measurable `<=` XY.
proof: Proof. move=> kD_ub; rewrite measurable_prod_measurableType. set C := [set A `*` B | A in measurable & B in measurable]. have CI : setI_closed C. move=> _ _ [X1 mX1 [X2 mX2 <-]] [Y1 mY1 [Y2 mY2 <-]]. exists (X1 `&` Y1); first exact: measurableI. by exists (X2 `&` Y2); [exact: measurableI|rewrite setMI]. have CT : C setT by exists setT => //; exists setT => //; rewrite setMTT. have CXY : C `<=` XY. move=> _ [A mA [B mB <-]]; split; first exact: measurableM. rewrite phiM. apply: emeasurable_funM => //; first exact/measurable_kernel/measurableI. by apply/EFin_measurable_fun; rewrite (_ : \1_ _ = mindic R mA). suff monoB : monotone_class setT XY by exact: monotone_class_subset. split => //; [exact: CXY| |exact: xsection_ndseq_closed]. move=> A B BA [mA mphiA] [mB mphiB]; split; first exact: measurableD. suff : phi (A `\` B) = (fun x => phi A x - phi B x). by move=> ->; exact: emeasurable_funB. rewrite funeqE => x; rewrite /phi/= xsectionD// measureD. - by rewrite setIidr//; exact: le_xsection. - exact: measurable_xsection. - exact: measurable_xsection. - have [M kM] := kD_ub x. rewrite (lt_le_trans (kM (xsection A x) _)) ?leey//. exact: measurable_xsection. 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