English
The range of the canonical toLp homomorphism equals the subgroup of Lp consisting of bounded continuous representatives.
Русский
Образ отображения toLp совпадает с подгруппой Lp, состоящей из ограниченных непрерывных представителей.
LaTeX
$$$\\mathrm{range}(\\mathrm{toLp}) = \\mathrm{Lp}_{\\text{bounded}}(E,p,μ).$$$
Lean4
/-- The `Lp`-norm of a bounded continuous function is at most a constant (depending on the measure
of the whole space) times its sup-norm. -/
theorem Lp_nnnorm_le (f : α →ᵇ E) :
‖(⟨f.toContinuousMap.toAEEqFun μ, mem_Lp f⟩ : Lp E p μ)‖₊ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * ‖f‖₊ :=
by
apply Lp.nnnorm_le_of_ae_bound
refine (f.toContinuousMap.coeFn_toAEEqFun μ).mono ?_
intro x hx
rw [← NNReal.coe_le_coe, coe_nnnorm, coe_nnnorm]
convert f.norm_coe_le_norm x using 2