uncenteredCovarianceBilinDual_of_not_memLp

English

If MemLp id 2 μ does not hold, then the uncentered covariance bilinear dual vanishes for all L1, L2 in StrongDual ℝ E.

Русский

Если отношение MemLp id 2 μ не выполняется, то нецентрированная ковариантная билинейная форма равна нулю для любых L1, L2 в StrongDual ℝ E.

LaTeX

$$$\\operatorname{uncenteredCovarianceBilinDual}(\\mu)(L_1,L_2) = 0$$$

Lean4

theorem uncenteredCovarianceBilinDual_of_not_memLp (h : ¬MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :
    uncenteredCovarianceBilinDual μ L₁ L₂ = 0 := by simp [uncenteredCovarianceBilinDual, StrongDual.toLp_of_not_memLp h]

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