theorem
ProbabilityTheory.condVar_of_ae_eq_zero_or_one
{Ω : Type u_1}
{m₀ m : MeasurableSpace Ω}
{X : Ω → ℝ}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
(hm : m ≤ m₀)
(hXmeas : MeasureTheory.AEStronglyMeasurable X μ)
(hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1)
:
Conditional variance of a Bernoulli random variable.
If a random variable is ae equal to 0 or 1, then we can compute its conditional variance as the
conditional probability that it's equal to 0 times the conditional probability that it's equal to
1.