Independence of functions implies that the measure is a probability measure #
If a nonzero function belongs to ℒ^p (in particular if it is integrable) and is independent
of another function, then the space is a probability space.
theorem
MeasureTheory.Memℒp.isProbabilityMeasure_of_indepFun
{Ω : Type u_1}
{E : Type u_2}
{F : Type u_3}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
[MeasurableSpace F]
(f : Ω → E)
(g : Ω → F)
{p : ENNReal}
(hp : p ≠ 0)
(hp' : p ≠ ⊤)
(hℒp : MeasureTheory.Memℒp f p μ)
(h'f : ¬∀ᵐ (ω : Ω) ∂μ, f ω = 0)
(hindep : ProbabilityTheory.IndepFun f g μ)
:
If a nonzero function belongs to ℒ^p and is independent of another function, then
the space is a probability space.
theorem
MeasureTheory.Integrable.isProbabilityMeasure_of_indepFun
{Ω : Type u_1}
{E : Type u_2}
{F : Type u_3}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
[MeasurableSpace F]
(f : Ω → E)
(g : Ω → F)
(hf : MeasureTheory.Integrable f μ)
(h'f : ¬∀ᵐ (ω : Ω) ∂μ, f ω = 0)
(hindep : ProbabilityTheory.IndepFun f g μ)
:
If a nonzero function is integrable and is independent of another function, then the space is a probability space.