covarianceBilinDual_of_not_memLp — Mathlib

English

If MemLp id 2 μ does not hold, then for any L1, L2 in StrongDual ℝ E, the covariance bilinear dual equals 0.

Русский

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

LaTeX

$$$covarianceBilinDual(\\mu) L_1 L_2 = 0$$$

Lean4

@[simp]
theorem covarianceBilinDual_of_not_memLp (h : ¬MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :
    covarianceBilinDual μ L₁ L₂ = 0 :=
  by
  rw [covarianceBilinDual, uncenteredCovarianceBilinDual_of_not_memLp]
  rw [(measurableEmbedding_subRight _).memLp_map_measure_iff]
  refine fun h_Lp ↦ h ?_
  have : (id : E → E) = fun x ↦ x - ∫ x, x ∂μ + ∫ x, x ∂μ := by ext; simp
  rw [this]
  exact h_Lp.add (memLp_const _)

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