covarianceBilinDual_zero — Mathlib

English

For μ = 0, covarianceBilinDual(μ) = 0 as a bilinear form on StrongDual Real E.

Русский

Для μ = 0 ковариационная билинейная двойкаcovarianceBilinDual(μ) равна нулю как билинейная форма на StrongDual Real E.

LaTeX

$$$covarianceBilinDual(0) = 0$$$

Lean4

@[simp]
theorem covarianceBilinDual_zero : covarianceBilinDual (0 : Measure E) = 0 := by
  rw [covarianceBilinDual, Measure.map_zero, uncenteredCovarianceBilinDual_zero]

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