English
For a finite measure μ and kernel κ, the product measure μ ⊗ₘ (κ.map f) equals (μ ⊗ₘ κ).map (Prod.map id f) for measurable f.
Русский
Для конечной меры μ и ядра κ верна связь μ ⊗ₘ (κ.map f) = (μ ⊗ₘ κ).map (Prod.map id f) при измеримой f.
LaTeX
$$$$\\mu \\otimes_m (\\kappa.map f) = (\\mu \\otimes_m \\kappa).map (Prod.map id~ f).$$$$
Lean4
theorem compProd_map [SFinite μ] [IsSFiniteKernel κ] {f : β → γ} (hf : Measurable f) :
μ ⊗ₘ (κ.map f) = (μ ⊗ₘ κ).map (Prod.map id f) := by
calc
μ ⊗ₘ (κ.map f)
_ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ (Kernel.id ×ₖ κ) ∘ₘ μ := by
rw [comp_assoc, Kernel.parallelComp_comp_prod, compProd_eq_comp_prod, Kernel.id_comp,
Kernel.deterministic_comp_eq_map]
_ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ (μ ⊗ₘ κ) := by rw [compProd_eq_comp_prod]
_ = (μ ⊗ₘ κ).map (Prod.map id f) := by
rw [Kernel.id, Kernel.deterministic_parallelComp_deterministic, deterministic_comp_eq_map]
