indepFun_iff_map_prod_eq_prod_map_map

English

For a finite index set ι, independence of the family f_i is equivalent to the joint map measure equaling the product of the marginals μ map f_i.

Русский

Для конечного множества индексов ι независимость семейства f_i эквивалентна равенству меры совместного отображения и произведения маргинальных мер μ map f_i.

LaTeX

$$$iIndepFun f μ \iff μ.map (\lambda ω i, f_i ω) = π_i μ.map (f_i)$$$

Lean4

theorem indepFun_iff_map_prod_eq_prod_map_map {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} [IsFiniteMeasure μ]
    (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
    IndepFun f g μ ↔ μ.map (fun ω ↦ (f ω, g ω)) = (μ.map f).prod (μ.map g) := by
  apply indepFun_iff_map_prod_eq_prod_map_map' hf hg <;> apply IsFiniteMeasure.toSigmaFinite

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