covarianceBilinDual_self_eq_variance

English

For MemLp id 2 μ, the covariance of L with itself equals the variance: covarianceBilinDual μ L L = Var[L; μ].

Русский

Для MemLp id 2 μ ковариация L с самим собой равна дисперсии: covarianceBilinDual μ L L = Var[L; μ].

LaTeX

$$$covarianceBilinDual(\\mu) L L = Var[L;\\mu]$$$

Lean4

theorem covarianceBilinDual_self_eq_variance (h : MemLp id 2 μ) (L : StrongDual ℝ E) :
    covarianceBilinDual μ L L = Var[L; μ] := by rw [covarianceBilinDual_eq_covariance h, covariance_self (by fun_prop)]

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