covarianceBilinDual_apply' — Mathlib

English

With MemLp id 2 μ, covarianceBilinDual μ L1 L2 equals the integral of L1(x - μ[id]) L2(x - μ[id]) over μ.

Русский

При MemLp id 2 μ ковариационная билинейная двойка равна интегралу L1(x - μ[id]) L2(x - μ[id]) по μ.

LaTeX

$$$covarianceBilinDual(\\mu) L_1 L_2 = \\int_E L_1(x - \\mu[id]) L_2(x - \\mu[id]) \\, d\\mu(x)$$$

Lean4

theorem covarianceBilinDual_apply' (h : MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :
    covarianceBilinDual μ L₁ L₂ = ∫ x, L₁ (x - μ[id]) * L₂ (x - μ[id]) ∂μ :=
  by
  rw [covarianceBilinDual_apply h]
  have hL (L : StrongDual ℝ E) : μ[L] = L (∫ x, x ∂μ) := L.integral_comp_comm (h.integrable (by simp))
  simp [← hL]

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