Distributions on two values #
This file proves a few lemmas about random variables that take at most two values.
theorem
MeasureTheory.integral_of_ae_eq_zero_or_one
{Ω : Type u_1}
{m : MeasurableSpace Ω}
{X : Ω → ℝ}
{μ : Measure Ω}
(hXmeas : AEMeasurable X μ)
(hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1)
:
If an AEMeasurable function is ae equal to 0 or 1, then its integral is equal to the
measure of the set where it equals 1.
theorem
MeasureTheory.integral_one_sub_of_ae_eq_zero_or_one
{Ω : Type u_1}
{m : MeasurableSpace Ω}
{X : Ω → ℝ}
{μ : Measure Ω}
(hXmeas : AEMeasurable X μ)
(hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1)
:
If a random variable is ae equal to 0 or 1, then one minus its expectation is equal to the
probability that it equals 0.
theorem
ProbabilityTheory.condVar_of_ae_eq_zero_or_one
{Ω : Type u_1}
{m : MeasurableSpace Ω}
{X : Ω → ℝ}
{m₀ : MeasurableSpace Ω}
(hm : m ≤ m₀)
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
(hXmeas : AEMeasurable X μ)
(hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1)
:
If a random variable is ae equal to 0 or 1, then its conditional variance is the product of
the conditional probabilities that it's equal to 0 and that it's equal to 1.
theorem
ProbabilityTheory.variance_of_ae_eq_zero_or_one
{Ω : Type u_1}
{m : MeasurableSpace Ω}
{X : Ω → ℝ}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
(hXmeas : AEMeasurable X μ)
(hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1)
:
If a random variable is ae equal to 0 or 1, then its variance is the product of
the probabilities that it's equal to 0 and that it's equal to 1.