proposition: Lemma product_measure2E (A1 : set T1) (A2 : set T2) (mA1 : measurable A1) (mA2 : measurable A2) : (m1 \x^ m2) (A1 `*` A2) = m1 A1 * m2 A2.
proof: Proof. have mA1A2 : measurable (A1 `*` A2) by apply: measurableM. transitivity (\int[m2]_y (m1 \o ysection (A1 `*` A2)) y) => //. rewrite (_ : _ \o _ = fun y => m1 A1 * (\1_A2 y)%:E). rewrite ge0_integralZl//. - by rewrite integral_indic ?setIT ?mul1e. - exact: measurableT_comp. - by move=> y _; rewrite lee_fin. rewrite funeqE => y; rewrite indicE. have [yA2|yA2] := boolP (y \in A2); first by rewrite mule1 /= in_ysectionM. by rewrite mule0 /= notin_ysectionM. 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