toLpₗ_apply — Mathlib

English

Definition of a continuous bilinear form on the dual spaces via inner products, related to covariances without centering the measure.

Русский

Определение непрерывной билинейной формы на двойственных пространствах через скалярное произведение, связанное с ковариациями без центрирования меры.

LaTeX

$$$\\text{uncenteredCovarianceBilinDual}(μ): \\text{StrongDual } 𝕜 E \\to_L[𝕜] (\\text{StrongDual } 𝕜 E \\to_L[𝕜] \\mathbb{R})$$$

Lean4

@[simp]
theorem toLpₗ_apply (h_Lp : MemLp id p μ) (L : StrongDual 𝕜 E) :
    L.toLpₗ μ p = MemLp.toLp L (h_Lp.continuousLinearMap_comp L) := by simp [toLpₗ, dif_pos h_Lp]

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