English
For L a continuous linear functional on E×F, the variance under the product measure equals the sum of variances of the two projections L∘inl and L∘inr.
Русский
Для L — непрерывный линейный функционал на E×F, дисперсия по мере μ×ν равна сумме дисперсий L∘inl и L∘inr.
LaTeX
$$$\operatorname{Var}[L;\, \mu\times\nu] = \operatorname{Var}[L\circ(\mathrm{inl});\, \mu] + \operatorname{Var}[L\circ(\mathrm{inr});\, \nu]$$$
Lean4
/-- **The Bhatia-Davis inequality on variance**
The variance of a random variable `X` satisfying `a ≤ X ≤ b` almost everywhere is at most
`(b - 𝔼 X) * (𝔼 X - a)`. -/
theorem variance_le_sub_mul_sub [IsProbabilityMeasure μ] {a b : ℝ} {X : Ω → ℝ} (h : ∀ᵐ ω ∂μ, X ω ∈ Set.Icc a b)
(hX : AEMeasurable X μ) : variance X μ ≤ (b - μ[X]) * (μ[X] - a) :=
by
have ha : ∀ᵐ ω ∂μ, a ≤ X ω := h.mono fun ω h => h.1
have hb : ∀ᵐ ω ∂μ, X ω ≤ b := h.mono fun ω h => h.2
have hX_int₂ : Integrable (fun ω ↦ -X ω ^ 2) μ := (memLp_of_bounded h hX.aestronglyMeasurable 2).integrable_sq.neg
have hX_int₁ : Integrable (fun ω ↦ (a + b) * X ω) μ :=
((integrable_const (max |a| |b|)).mono' hX.aestronglyMeasurable
(by filter_upwards [ha, hb] with ω using abs_le_max_abs_abs)).const_mul
(a + b)
have h0 : 0 ≤ -μ[X ^ 2] + (a + b) * μ[X] - a * b :=
calc
_ ≤ ∫ ω, (b - X ω) * (X ω - a) ∂μ := by
apply integral_nonneg_of_ae
filter_upwards [ha, hb] with ω ha' hb'
exact mul_nonneg (by linarith : 0 ≤ b - X ω) (by linarith : 0 ≤ X ω - a)
_ = ∫ ω, -X ω ^ 2 + (a + b) * X ω - a * b ∂μ := (integral_congr_ae <| ae_of_all μ fun ω ↦ by ring)
_ = ∫ ω, -X ω ^ 2 + (a + b) * X ω ∂μ - ∫ _, a * b ∂μ := (integral_sub (by fun_prop) (integrable_const (a * b)))
_ = ∫ ω, -X ω ^ 2 + (a + b) * X ω ∂μ - a * b := by simp
_ = -μ[X ^ 2] + (a + b) * μ[X] - a * b := by
simp [← integral_neg, ← integral_const_mul, integral_add hX_int₂ hX_int₁]
calc
_ ≤ (a + b) * μ[X] - a * b - μ[X] ^ 2 :=
by
rw [variance_eq_sub (memLp_of_bounded h hX.aestronglyMeasurable 2)]
linarith
_ = (b - μ[X]) * (μ[X] - a) := by ring
