condVar_smul — Mathlib

English

Scaling a random variable by a constant c scales its conditional variance by c^2 almost surely.

Русский

Условная дисперсия при множителе c масштаба X возрастает как c^2.

LaTeX

$$$\\mathrm{Var}[c \\cdot X; \\mu | m] =^a.e_\\mu c^2 \\cdot \\mathrm{Var}[X; \\mu | m]$$$

Lean4

theorem condVar_smul (c : ℝ) (X : Ω → ℝ) : Var[c • X; μ | m] =ᵐ[μ] c ^ 2 • Var[X; μ | m] := by
  calc
    Var[c • X; μ | m]
    _ =ᵐ[μ] μ[c ^ 2 • (X - μ[X|m]) ^ 2|m] := by
      rw [condVar]
      refine condExp_congr_ae ?_
      filter_upwards [condExp_smul (m := m) c X] with ω hω
      simp [hω, ← mul_sub, mul_pow]
    _ =ᵐ[μ] c ^ 2 • Var[X; μ | m] := condExp_smul ..

Похожие утверждения