Theorems · Theorem · probability

MeasureTheory.MemLp.isProbabilityMeasure_of_indepFun

∀ {Ω : Type u_1} {E : Type u_2} {F : Type u_3} [inst : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_1 : NormedAddCommGroup E] [inst_2 : MeasurableSpace E] [OpensMeasurableSpace E] [inst_4 : MeasurableSpace F]
  (f : Ω → E) (g : Ω → F) {p : ENNReal},
  p ≠ 0 →
    p ≠ ⊤ →
      MeasureTheory.MemLp f p μ →
        (¬∀ᵐ (ω : Ω) ∂μ, f ω = 0) → ProbabilityTheory.IndepFun f g μ → MeasureTheory.IsProbabilityMeasure μ

If a nonzero function belongs to ℒ^p and is independent of another function, then the space is a probability space.

Defined in

Mathlib.Probability.Independence.Integrable

Cited by

5 results in Mathlib

Foundations

Depth 213 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceNormedAddCommGroupMeasurableSpaceOpensMeasurableSpaceMeasurableSpace