English
The map sending a pair of probability measures (on α and β) to their product measure on α × β is measurable.
Русский
Отображение пары вероятностных мер (на α и β) в их произведение меры на α × β является измеримым.
LaTeX
$$$\\text{Measurable}\\;\\bigl( (\\mu,\\nu) \\mapsto \\mu^{\\mathrm{toMeasure}} \\;\\mathrm{prod} \\; \\nu^{\\mathrm{toMeasure}} \\bigr)$$$
Lean4
/-- The monoidal product is a measurable function from the product of probability spaces over
`α` and `β` into the type of probability spaces over `α × β`. Lemma 4.1 of [A synthetic approach to
Markov kernels, conditional independence and theorems on sufficient statistics][fritz2020]. -/
theorem measurable_fun_prod {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] :
Measurable (fun (μ : ProbabilityMeasure α × ProbabilityMeasure β) ↦ μ.1.toMeasure.prod μ.2.toMeasure) :=
by
apply Measurable.measure_of_isPiSystem_of_isProbabilityMeasure generateFrom_prod.symm isPiSystem_prod _
simp only [mem_image2, mem_setOf_eq, forall_exists_index, and_imp]
intro _ u Hu v Hv Heq
simp_rw [← Heq, Measure.prod_prod]
apply Measurable.mul
· exact (Measure.measurable_coe Hu).comp (measurable_subtype_coe.comp measurable_fst)
· exact (Measure.measurable_coe Hv).comp (measurable_subtype_coe.comp measurable_snd)
