proposition: Lemma measurable_prod_subset_xsection (m2D_bounded : exists M, forall X, measurable X -> (m2D X < M%:E)%E) : measurable `<=` B.
proof: Proof. rewrite measurable_prod_measurableType. set C := [set A1 `*` A2 | A1 in measurable & A2 in measurable]. have CI : setI_closed C. move=> X Y [X1 mX1 [X2 mX2 <-{X}]] [Y1 mY1 [Y2 mY2 <-{Y}]]. 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 CB : C `<=` B. move=> X [X1 mX1 [X2 mX2 <-{X}]]; split; first exact: measurableM. have -> : phi (X1 `*` X2) = (fun x => m2D X2 * (\1_X1 x)%:E)%E. rewrite funeqE => x; rewrite indicE /phi /m2/= /mrestr. have [xX1|xX1] := boolP (x \in X1); first by rewrite mule1 in_xsectionM. by rewrite mule0 notin_xsectionM// set0I measure0. exact/measurable_funeM/EFin_measurable_fun. suff monoB : monotone_class setT B by exact: monotone_class_subset. split => //; [exact: CB| |exact: xsection_ndseq_closed]. move=> X Y XY [mX mphiX] [mY mphiY]; split; first exact: measurableD. have -> : phi (X `\` Y) = (fun x => phi X x - phi Y x)%E. rewrite funeqE => x; rewrite /phi/= xsectionD// /m2D measureD. - by rewrite setIidr//; exact: le_xsection. - exact: measurable_xsection. - exact: measurable_xsection. - move: m2D_bounded => [M m2M]. rewrite (lt_le_trans (m2M (xsection X x) _))// ?leey//. exact: measurable_xsection. exact: emeasurable_funB. 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