English
If a random variable X is almost surely confined between a and b and Is Probability measure μ, then Var(X) ≤ ((b−a)/2)^2.
Русский
Если X практически всегда лежит в интервале [a,b] при распределении μ, то Var(X) ≤ ((b−a)/2)^2.
LaTeX
$$$\operatorname{Var}[X;\, \mu] \le \left(\frac{b-a}{2}\right)^2$$$
Lean4
/-- **Popoviciu's inequality on variances**
The variance of a random variable `X` satisfying `a ≤ X ≤ b` almost everywhere is at most
`((b - a) / 2) ^ 2`. -/
theorem variance_le_sq_of_bounded [IsProbabilityMeasure μ] {a b : ℝ} {X : Ω → ℝ} (h : ∀ᵐ ω ∂μ, X ω ∈ Set.Icc a b)
(hX : AEMeasurable X μ) : variance X μ ≤ ((b - a) / 2) ^ 2 :=
calc
_ ≤ (b - μ[X]) * (μ[X] - a) := variance_le_sub_mul_sub h hX
_ = ((b - a) / 2) ^ 2 - (μ[X] - (b + a) / 2) ^ 2 := by ring
_ ≤ ((b - a) / 2) ^ 2 := sub_le_self _ (sq_nonneg _)
