English
Let μ_a and μ_c be σ-finite measures on spaces α and γ, and let f: α → β and g: γ → δ be measurable. Then the product of the pushforwards equals the pushforward of the product map: (f_*μ_a) ⊗ (g_*μ_c) = (Prod.map f g)_*(μ_a ⊗ μ_c).
Русский
Пусть μ_a и μ_c — сигма-конечные меры на пространствах α и γ, а f: α → β и g: γ → δ — измеримые отображения. Тогда произведение образов мер равно образованию произведения мер под отображением Prod.map: (f_*μ_a) ⊗ (g_*μ_c) = (Prod.map f g)_*(μ_a ⊗ μ_c).
LaTeX
$$$(f_*\mu_a) \otimes (g_*\mu_c) = (\mathrm{Prod.map}(f,g))_* (\mu_a \otimes \mu_c)$$$
Lean4
theorem map_prod_map {δ} [MeasurableSpace δ] {f : α → β} {g : γ → δ} (μa : Measure α) (μc : Measure γ) [SFinite μa]
[SFinite μc] (hf : Measurable f) (hg : Measurable g) :
(map f μa).prod (map g μc) = map (Prod.map f g) (μa.prod μc) :=
by
simp_rw [← sum_sfiniteSeq μa, ← sum_sfiniteSeq μc, map_sum hf.aemeasurable, map_sum hg.aemeasurable, prod_sum,
map_sum (hf.prodMap hg).aemeasurable]
congr
ext1 i
refine prod_eq fun s t hs ht => ?_
rw [map_apply (hf.prodMap hg) (hs.prod ht), map_apply hf hs, map_apply hg ht]
exact
prod_prod (f ⁻¹' s)
(g ⁻¹' t)
-- `prod_smul_right` needs an instance to get `SFinite (c • ν)` from `SFinite ν`,
-- hence it is placed in the `WithDensity` file, where the instance is defined.
