proposition: Lemma measurable_prod_subset_ysection (m1_bounded : exists M, forall X, measurable X -> (m1D 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 -> : psi (X1 `*` X2) = (fun x => m1D X1 * (\1_X2 x)%:E)%E. rewrite funeqE => y; rewrite indicE /psi /m1/= /mrestr. have [yX2|yX2] := boolP (y \in X2); first by rewrite mule1 in_ysectionM. by rewrite mule0 notin_ysectionM// set0I measure0. exact/measurable_funeM/EFin_measurable_fun. suff monoB : monotone_class setT B by exact: monotone_class_subset. split => //; [exact: CB| |exact: ysection_ndseq_closed]. move=> X Y XY [mX mphiX] [mY mphiY]; split; first exact: measurableD. rewrite (_ : psi _ = (psi X \- psi Y)%E); first exact: emeasurable_funB. rewrite funeqE => y; rewrite /psi/= ysectionD// /m1D measureD. - by rewrite setIidr//; exact: le_ysection. - exact: measurable_ysection. - exact: measurable_ysection. - have [M m1M] := m1_bounded. rewrite (lt_le_trans (m1M (ysection X y) _))// ?leey//. exact: measurable_ysection. 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