covarianceBilinDual_eq_covariance

English

For MemLp id 2 μ, the covariance bilinear dual equals the standard covariance functional: covarianceBilinDual μ L1 L2 = cov[L1, L2; μ].

Русский

Для MemLp id 2 μ ковариационная билинейная двойка равна стандартной ковариационной функциональности: covarianceBilinDual μ L1 L2 = cov[L1, L2; μ].

LaTeX

$$$covarianceBilinDual(\\mu) L_1 L_2 = cov[L_1,L_2;\\mu]$$$

Lean4

theorem covarianceBilinDual_eq_covariance (h : MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :
    covarianceBilinDual μ L₁ L₂ = cov[L₁, L₂; μ] := by rw [covarianceBilinDual_apply h, covariance]

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