English
For E and F normed spaces and L a continuous dual on E×F, the variance of L under the product measure equals the sum of variances of its components on E and F respectively.
Русский
Пусть E и F — нормированные пространства, L — непрерывно-двоичное линейное отображение на E×F. Тогда дисперсия L по мере μ×ν равна сумме дисперсий 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 variance of the sum of two independent random variables is the sum of the variances. -/
nonrec theorem variance_add {X Y : Ω → ℝ} (hX : MemLp X 2 μ) (hY : MemLp Y 2 μ) (h : IndepFun X Y μ) :
Var[X + Y; μ] = Var[X; μ] + Var[Y; μ] := by
by_cases h' : X =ᵐ[μ] 0
· rw [variance_congr h', variance_congr h'.add_right]
simp
have := hX.isProbabilityMeasure_of_indepFun X Y (by simp) (by simp) h' h
rw [variance_add hX hY, h.covariance_eq_zero hX hY]
simp
