covarianceBilinDual_comm — Mathlib

English

The bilinear dual is symmetric in its two arguments: covarianceBilinDual μ L1 L2 = covarianceBilinDual μ L2 L1.

Русский

Билинейная двойка ковариации симметрична по своим аргументам: covarianceBilinDual μ L1 L2 = covarianceBilinDual μ L2 L1.

LaTeX

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

Lean4

theorem covarianceBilinDual_comm (L₁ L₂ : StrongDual ℝ E) : covarianceBilinDual μ L₁ L₂ = covarianceBilinDual μ L₂ L₁ :=
  by
  by_cases h : MemLp id 2 μ
  · have h' : MemLp id 2 (Measure.map (fun x ↦ x - ∫ (x : E), x ∂μ) μ) :=
      (measurableEmbedding_subRight _).memLp_map_measure_iff.mpr <| h.sub (memLp_const _)
    simp_rw [covarianceBilinDual, uncenteredCovarianceBilinDual_apply h', mul_comm (L₁ _)]
  · simp [h]

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