English
If μ is a probability measure and X: Ω → ℝ is strongly measurable and square-integrable, then Var[X; μ] ≤ μ[X^2].
Русский
Если μ — распределение вероятностей, и X: Ω → ℝ является сильно измеримой и квадрат-зку
LaTeX
$$$\operatorname{Var}[X;\, \mu] \leq \mu[X^{2}]$$$
Lean4
theorem variance_le_expectation_sq [IsProbabilityMeasure μ] {X : Ω → ℝ} (hm : AEStronglyMeasurable X μ) :
variance X μ ≤ μ[X ^ 2] := by
by_cases hX : MemLp X 2 μ
· rw [variance_eq_sub hX]
simp only [sq_nonneg, sub_le_self_iff]
rw [variance, evariance_eq_lintegral_ofReal, ← integral_eq_lintegral_of_nonneg_ae]
· by_cases hint : Integrable X μ; swap
· simp only [integral_undef hint, Pi.pow_apply, sub_zero]
exact le_rfl
· rw [integral_undef]
· exact integral_nonneg fun a => sq_nonneg _
intro h
have A : MemLp (X - fun ω : Ω => μ[X]) 2 μ := (memLp_two_iff_integrable_sq (by fun_prop)).2 h
have B : MemLp (fun _ : Ω => μ[X]) 2 μ := memLp_const _
apply hX
convert A.add B
simp
· exact Eventually.of_forall fun x => sq_nonneg _
· exact (AEMeasurable.pow_const (hm.aemeasurable.sub_const _) _).aestronglyMeasurable
