indepFun_iff_indepSet_preimage — Mathlib

English

If f and g are random variables, independence is equivalent to equality of the joint map measure with the product of their marginals: μ∘(f,g) = (μ∘f) × (μ∘g).

Русский

Независимость случайных величин f и g эквивалентна равенству меры совместного отображения и произведения маргинальных мер: μ∘(f,g) = (μ∘f) × (μ∘g).

LaTeX

$$$IndepFun f g μ \iff μmap(f,g) = (μmap f) . (μmap g)$$$

Lean4

theorem indepFun_iff_indepSet_preimage {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
    [IsZeroOrProbabilityMeasure μ] (hf : Measurable f) (hg : Measurable g) :
    IndepFun f g μ ↔ ∀ s t, MeasurableSet s → MeasurableSet t → IndepSet (f ⁻¹' s) (g ⁻¹' t) μ := by
  simp only [IndepFun, IndepSet, Kernel.indepFun_iff_indepSet_preimage hf hg]

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