English
If L: Hermitian-degree functional on E×F has suitable integrability, the variance of the sum L⟨X, Y⟩ equals Var[X; μ] + Var[Y; ν].
Русский
Если функционал L имеет достаточную интегрируемость, то дисперсия суммы факторов L⟨X,Y⟩ равна сумме дисперсий X и Y.
LaTeX
$$$\operatorname{Var}[L;\, \mu×ν] = \operatorname{Var}[L;X;\mu] + \operatorname{Var}[L;Y;ν]$$$
Lean4
theorem variance_add_prod (hfμ : MemLp X 2 μ) (hgν : MemLp Y 2 ν) :
Var[fun p ↦ X p.1 + Y p.2; μ.prod ν] = Var[X; μ] + Var[Y; ν] :=
by
refine (IndepFun.variance_fun_add (hfμ.comp_fst ν) (hgν.comp_snd μ) ?_).trans ?_
· exact indepFun_prod₀ hfμ.aemeasurable hgν.aemeasurable
·
rw [measurePreserving_fst.variance_fun_comp hfμ.aemeasurable,
measurePreserving_snd.variance_fun_comp hgν.aemeasurable]
