English
Let μ be a finite measure on α, E a normed additively commutative group, and p ≥ 1. The operator that sends an E-valued function to its Lp-variant with constant Lp embedding has its operator norm bounded above by μ(α)^(1/p).
Русский
Пусть μ—конечное мерное пространство на α, E нормированная аддитивная абелева группа и p ≥ 1. Оператор, переходящий из E-векторных функций в соответствующие Lp-функции, имеет норму ограниченного линейного оператора не более чем μ(α)^(1/p).
LaTeX
$$$\\| \\mathrm{Lp.constL}(p,\\mu,\\mathbb{K}) : E \\to_L[\\mathbb{K}] \\mathrm{Lp}\\,E\\,p\\,\\mu \\| \\le \\mu(\\mathrm{Set.univ})^{1/p}$$$
Lean4
theorem norm_constL_le (𝕜 : Type*) [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [Fact (1 ≤ p)] :
‖(Lp.constL p μ 𝕜 : E →L[𝕜] Lp E p μ)‖ ≤ μ.real Set.univ ^ (1 / p.toReal) :=
LinearMap.mkContinuous_norm_le _ (by positivity) _
