toLpCLM_apply — Mathlib

English

There is a CLM (continuous linear map) from Schwartz maps to Lp-norm structures, preserving the linear functional.

Русский

Существует непрерывно линейное отображение из отображений Шварца в структуру Lp-норм, сохраняющее линейную функциональность.

LaTeX

$$$$ toLpCLM 𝕜 F p μ : SchwartzMap E F \\to Lp\\text{-space} F $$$$

Lean4

@[simp]
theorem toLpCLM_apply {p : ℝ≥0∞} [Fact (1 ≤ p)] {μ : Measure E} [hμ : μ.HasTemperateGrowth] {f : 𝓢(E, F)} :
    toLpCLM 𝕜 F p μ f = f.toLp p μ :=
  rfl

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