uncenteredCovarianceBilinDual_zero

English

For the zero measure, the uncentered covariance bilinear dual is identically zero for all L1, L2.

Русский

Для нулевой меры нецентрированная ковариантная билинейная форма тождественно равна нулю для любых L1, L2.

LaTeX

$$$\\operatorname{uncenteredCovarianceBilinDual}(0) = 0$$$

Lean4

theorem uncenteredCovarianceBilinDual_zero : uncenteredCovarianceBilinDual (0 : Measure E) = 0 :=
  by
  ext
  have : Subsingleton (Lp ℝ 2 (0 : Measure E)) := ⟨fun x y ↦ Lp.ext_iff.2 rfl⟩
  simp [uncenteredCovarianceBilinDual, Subsingleton.eq_zero (StrongDual.toLp 0 2)]

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