toLp_norm_le — Mathlib

English

The operator norm of ContinuousMap.toLp is bounded above by a universal function of μ, consistent with the Lp embedding.

Русский

Нормa оператора ContinuousMap.toLp ограничена сверху универсальной функцией от μ, что согласуется с внедрением в Lp.

LaTeX

$$$\| toLp(p μ 𝕜) \| \le measureUnivNNReal(μ)^{p.toReal^{-1}}$$$

Lean4

/-- Bound for the operator norm of `ContinuousMap.toLp`. -/
theorem toLp_norm_le : ‖(toLp p μ 𝕜 : C(α, E) →L[𝕜] Lp E p μ)‖ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ :=
  by
  rw [toLp_norm_eq_toLp_norm_coe]
  exact BoundedContinuousFunction.toLp_norm_le μ

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