isProbabilityMeasure_of_indepFun — Mathlib

English

Independence of a family of measurable X_i is equivalent to independence on the product space; iIndepFun X μ holds when X_i are independent across i.

Русский

Независимость семейства X_i эквивалентна независимости на произведении пространств; iIndepFun X μ обозначает независимость по i.

LaTeX

$$$\text{IndepFun } X μ \iff μ.map (λ ω i. X_i ω) = infinitePi (λ i. μ.map (X_i))$$$

Lean4

/-- If a nonzero function is integrable and is independent of another function, then
the space is a probability space. -/
theorem isProbabilityMeasure_of_indepFun (f : Ω → E) (g : Ω → F) (hf : Integrable f μ) (h'f : ¬(∀ᵐ ω ∂μ, f ω = 0))
    (hindep : IndepFun f g μ) : IsProbabilityMeasure μ :=
  MemLp.isProbabilityMeasure_of_indepFun f g one_ne_zero ENNReal.one_ne_top (memLp_one_iff_integrable.mpr hf) h'f hindep

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