English
For any AEStronglyMeasurable X and real c, Var[X + c; μ] = Var[X; μ].
Русский
При любом AEStronglyMeasurable X и константе c дисперсия не изменяется при сдвиге: Var[X + c; μ] = Var[X; μ].
LaTeX
$$$$ \mathrm{variance}(X + c, \mu) = \mathrm{variance}(X, \mu). $$$$
Lean4
theorem variance_add_const [IsProbabilityMeasure μ] (hX : AEStronglyMeasurable X μ) (c : ℝ) :
Var[fun ω ↦ X ω + c; μ] = Var[X; μ] := by
by_cases hX_Lp : MemLp X 2 μ
· have hX_int : Integrable X μ := hX_Lp.integrable one_le_two
rw [variance_eq_integral (hX.add_const _).aemeasurable, integral_add hX_int (by fun_prop), integral_const,
variance_eq_integral hX.aemeasurable]
simp
· rw [variance_of_not_memLp (hX.add_const _), variance_of_not_memLp hX hX_Lp]
refine fun h_memLp ↦ hX_Lp ?_
have : X = fun ω ↦ X ω + c - c := by ext; ring
rw [this]
exact h_memLp.sub (memLp_const c)
