covarianceBilinDual_apply — Mathlib

English

Under MemLp id 2 μ, the covariance bilinear dual satisfies covarianceBilinDual μ L1 L2 = ∫ (L1(x) - μ[L1])(L2(x) - μ[L2]) dμ.

Русский

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

LaTeX

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

Lean4

theorem covarianceBilinDual_apply (h : MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :
    covarianceBilinDual μ L₁ L₂ = ∫ x, (L₁ x - μ[L₁]) * (L₂ x - μ[L₂]) ∂μ :=
  by
  rw [covarianceBilinDual, uncenteredCovarianceBilinDual_apply, integral_map (by fun_prop) (by fun_prop)]
  · have hL (L : StrongDual ℝ E) : μ[L] = L (∫ x, x ∂μ) := L.integral_comp_comm (h.integrable (by simp))
    simp [← hL]
  · exact (measurableEmbedding_subRight _).memLp_map_measure_iff.mpr <| h.sub (memLp_const _)

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