English
If f: α → β and g: γ → δ are measure-preserving from μa to μb and μc to μd respectively, then the product map (Prod.map f g) preserves the product measures: (μa × μc) ↦ (μb × μd).
Русский
Если отображения f и g сохраняют меры соответственно, то отображение Prod.map f g сохраняет произведение мер: μa × μc → μb × μd.
LaTeX
$$MeasurePreserving (Prod.map f g) (μ_a × μ_c) (μ_b × μ_d)$$
Lean4
/-- If `f : α → β` sends the measure `μa` to `μb` and `g : γ → δ` sends the measure `μc` to `μd`,
then `Prod.map f g` sends `μa.prod μc` to `μb.prod μd`. -/
protected theorem prod [SFinite μa] [SFinite μc] {f : α → β} {g : γ → δ} (hf : MeasurePreserving f μa μb)
(hg : MeasurePreserving g μc μd) : MeasurePreserving (Prod.map f g) (μa.prod μc) (μb.prod μd) :=
have : Measurable (uncurry fun _ : α => g) := hg.1.comp measurable_snd
hf.skew_product this <| ae_of_all _ fun _ => hg.map_eq
