English
Let f: α → β be measure-preserving and, for almost every a, let g_a: γ → δ be measure-preserving, with g measurable in two arguments. Then the map (a,c) ↦ (f(a), g_a(c)) is measure-preserving from μ_a × μ_c to μ_b × μ_d.
Русский
Пусть f: α → β сохраняет меру, а почти у каждого a функция g_a: γ → δ сохраняет меру, причём g(a, c) зависит измеримо. Тогда отображение (a,c) ↦ (f(a), g_a(c)) сохраняет меру от μ_a × μ_c к μ_b × μ_d.
LaTeX
$$Measurable (Prod.map f g) is MeasurePreserving from (μ_a × μ_c) to (μ_b × μ_d).$$
Lean4
/-- Let `f : α → β` be a measure-preserving map.
For a.e. all `a`, let `g a : γ → δ` be a measure-preserving map.
Also suppose that `g` is measurable as a function of two arguments.
Then the map `fun (a, c) ↦ (f a, g a c)` is a measure-preserving map
for the product measures on `α × γ` and `β × δ`.
Some authors call a map of the form `fun (a, c) ↦ (f a, g a c)` a *skew product* over `f`,
thus the choice of a name.
-/
theorem skew_product [SFinite μa] [SFinite μc] {f : α → β} (hf : MeasurePreserving f μa μb) {g : α → γ → δ}
(hgm : Measurable (uncurry g)) (hg : ∀ᵐ a ∂μa, map (g a) μc = μd) :
MeasurePreserving (fun p : α × γ => (f p.1, g p.1 p.2)) (μa.prod μc) (μb.prod μd) :=
by
have : Measurable fun p : α × γ => (f p.1, g p.1 p.2) := (hf.1.comp measurable_fst).prodMk hgm
use this
rcases eq_zero_or_neZero μa with rfl | _
· simp [← hf.map_eq]
have sf : SFinite μd := by
obtain ⟨a, ha⟩ : ∃ a, map (g a) μc = μd := hg.exists
rw [← ha]
infer_instance
-- Thus we can use the integral formula for the product measure, and compute things explicitly
ext s hs
rw [map_apply this hs, prod_apply (this hs), prod_apply hs, ← hf.lintegral_comp (measurable_measure_prodMk_left hs)]
apply lintegral_congr_ae
filter_upwards [hg] with a ha
rw [← ha, map_apply hgm.of_uncurry_left (measurable_prodMk_left hs), preimage_preimage, preimage_preimage]
