English
If f: α×β → γ is measurable and for almost every y with respect to ν, the slice map x ↦ f(x,y) is quasi-measure-preserving from μ to τ, then f is quasi-measure-preserving from μ×ν to τ.
Русский
Если f: α×β→γ измеримо и для почти всех y по ν отображение x↦f(x,y) сохраняет меру μ→τ, то f сохраняет меру μ×ν→τ.
LaTeX
$$QuasiMeasurePreserving f (μ × ν) τ$$
Lean4
theorem prod_of_left {α β γ} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {f : α × β → γ} {μ : Measure α}
{ν : Measure β} {τ : Measure γ} (hf : Measurable f) [SFinite μ] [SFinite ν]
(h2f : ∀ᵐ y ∂ν, QuasiMeasurePreserving (fun x => f (x, y)) μ τ) : QuasiMeasurePreserving f (μ.prod ν) τ :=
by
rw [← prod_swap]
convert
(QuasiMeasurePreserving.prod_of_right (hf.comp measurable_swap) h2f).comp
((measurable_swap.measurePreserving (ν.prod μ)).symm MeasurableEquiv.prodComm).quasiMeasurePreserving
