English
The map that sends a pair of finite measures (μ, ν) to their product measure μ.toMeasure.prod ν.toMeasure is measurable.
Русский
Отображение, отправляющее пару конечных мер (μ, ν) в их произведение меры μ.toMeasure.prod ν.toMeasure, является измеримым.
LaTeX
$$$\Measurable\big(\lambda (\mu, \nu) \mapsto \mu.toMeasure \;\mathrm{prod} \; \nu.toMeasure\big)$$$
Lean4
/-- The monoidal product is a measurable function from the product of finite measures over
`α` and `β` into the type of finite measures over `α × β`. -/
theorem measurable_fun_prod {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] :
Measurable (fun (μ : FiniteMeasure α × FiniteMeasure β) ↦ μ.1.toMeasure.prod μ.2.toMeasure) :=
by
have Heval {u v} (Hu : MeasurableSet u) (Hv : MeasurableSet v) :
Measurable fun a : (FiniteMeasure α × FiniteMeasure β) ↦ a.1.toMeasure u * a.2.toMeasure v :=
Measurable.mul ((Measure.measurable_coe Hu).comp (measurable_subtype_coe.comp measurable_fst))
((Measure.measurable_coe Hv).comp (measurable_subtype_coe.comp measurable_snd))
apply Measurable.measure_of_isPiSystem generateFrom_prod.symm isPiSystem_prod _
· simp_rw [← Set.univ_prod_univ, Measure.prod_prod, Heval MeasurableSet.univ MeasurableSet.univ]
simp only [mem_image2, mem_setOf_eq, forall_exists_index, and_imp]
intro _ _ Hu _ Hv Heq
simp_rw [← Heq, Measure.prod_prod, Heval Hu Hv]
