Theorems · Theorem · probability

MeasureTheory.Integrable.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),
  MeasureTheory.Integrable f μ →
    (¬∀ᵐ (ω : Ω) ∂μ, f ω = 0) → ProbabilityTheory.IndepFun f g μ → MeasureTheory.IsProbabilityMeasure μ

If a nonzero function is integrable and is independent of another function, then the space is a probability space.

Defined in

Mathlib.Probability.Independence.Integrable

Cited by

3 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceNormedAddCommGroupMeasurableSpaceOpensMeasurableSpaceMeasurableSpace