proposition: Lemma product_measure1E (A1 : set T1) (A2 : set T2) : measurable A1 -> measurable A2 -> (m1 \x m2) (A1 `*` A2) = m1 A1 * m2 A2.
proof: Proof. move=> mA1 mA2 /=; rewrite /product_measure1 /=. rewrite (eq_integral (fun x => (\1_A1 x)%:E * m2 A2)); last first. by move=> x _; rewrite indicE; have [xA1|xA1] /= := boolP (x \in A1); [rewrite in_xsectionM// mul1e|rewrite mul0e notin_xsectionM]. rewrite ge0_integralZr//; last by move=> x _; rewrite lee_fin. - by rewrite integral_indic// setIT. - exact: measurableT_comp. 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