English
Let f: α × β → γ be measurable. If for almost every x with respect to μ, the slice map y ↦ f(x,y) is quasi-measure-preserving from ν to τ, then f is quasi-measure-preserving from μ × ν to τ.
Русский
Пусть f: α×β→γ измеримо. Если для почти всех x по μ отображение y↦f(x,y) сохраняет меру ν→τ в квази-отношении, то f сохраняет меру μ×ν→τ.
LaTeX
$$QuasiMeasurePreserving f (μ × ν) τ$$
Lean4
theorem prod_of_right {f : α × β → γ} {μ : Measure α} {ν : Measure β} {τ : Measure γ} (hf : Measurable f) [SFinite ν]
(h2f : ∀ᵐ x ∂μ, QuasiMeasurePreserving (fun y => f (x, y)) ν τ) : QuasiMeasurePreserving f (μ.prod ν) τ :=
by
refine ⟨hf, ?_⟩
refine AbsolutelyContinuous.mk fun s hs h2s => ?_
rw [map_apply hf hs, prod_apply (hf hs)]; simp_rw [preimage_preimage]
rw [lintegral_congr_ae (h2f.mono fun x hx => hx.preimage_null h2s), lintegral_zero]
