variance_dual_prod — Mathlib

English

For a StrongDual L on E×F, the variance under μ×ν equals the sum of variances of the projected functionals on E and F.

Русский

Для сильного двойственного модуля L на E×F дисперсия по мере μ×ν равна сумме дисперсий проекций на E и F.

LaTeX

$$$\operatorname{Var}[L;\, \mu\times\nu] = \operatorname{Var}[L;\text{inl};\mu] + \operatorname{Var}[L;\text{inr};\nu]$$$

Lean4

theorem variance_dual_prod {L : StrongDual ℝ (E × F)} (hLμ : MemLp id 2 μ) (hLν : MemLp id 2 ν) :
    Var[L; μ.prod ν] = Var[L.comp (.inl ℝ E F); μ] + Var[L.comp (.inr ℝ E F); ν] :=
  variance_dual_prod' (ContinuousLinearMap.comp_memLp' _ hLμ) (ContinuousLinearMap.comp_memLp' _ hLν)

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