map_mul_eq_map_mconv_map₀ — Mathlib

English

Independence of a finite product of random variables from the rest of the family under iIndepFun.

Русский

Независимость конечного произведения от остальных переменных в семействе.

LaTeX

$$$\\forall s \\text{ finite},\\ IndepFun\\Big(\\prod_{j\\in s} f_j, \\prod_{i\\notin s} f_i\\Big)\\mu$$$

Lean4

@[to_additive]
theorem map_mul_eq_map_mconv_map₀ [IsFiniteMeasure μ] {f g : Ω → M} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
    (hfg : IndepFun f g μ) : μ.map (f * g) = (μ.map f) ∗ₘ (μ.map g) := by
  apply hfg.map_mul_eq_map_mconv_map₀' hf hg <;> apply IsFiniteMeasure.toSigmaFinite

Похожие утверждения