toLp_norm_le — Mathlib

English

There is a normed additive group homomorphism from bounded continuous functions to Lp, whose image lies in Lp and is bounded by Lp_norm_le.

Русский

Существует нормированное аддитивное гомоморфное отображение из ограниченных непрерывных функций в Lp, образ которого ограничен оценки Lp_norm_le.

LaTeX

$$$\\mathrm{toLp}\\colon (\\alpha\\to^{\\text{ᵇ}} E) \\to Lp(E,p,μ) \\text{ is a bounded add. group hom. with bound } \\|\\mathrm{toLp}\\| \\le \\mathrm{measureUnivNNReal}(μ)^{p^{\\tfrac{1}{\\mathrm{real}}-1}}.$$$

Lean4

theorem toLp_norm_le {𝕜 : Type*} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] :
    ‖(toLp p μ 𝕜 : (α →ᵇ E) →L[𝕜] Lp E p μ)‖ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ :=
  LinearMap.mkContinuous_norm_le _ (measureUnivNNReal μ ^ p.toReal⁻¹).coe_nonneg _

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