English
There is a canonical normed additive group homomorphism from bounded continuous functions into Lp, sending f to its Lp-class, with a uniform bound by Lp_norm_le.
Русский
Существует каноническое гомоморфное отображение от ограниченных непрерывных функций в Lp, отправляющее f в её класс в Lp, с равномерной оценкой Lp-нормы через Lp_norm_le.
LaTeX
$$$\\text{toLp}: (\\alpha \\to\\!^b E) \\to Lp(E,p,μ) \\quad\\text{ is a bounded additive group homomorphism with bound } \\|toLp\\| \\le \\mathrm{measureUnivNNReal}(μ)^{p^{\\mathrm{real}-1}}.$$$
Lean4
/-- A bounded continuous function on a finite-measure space is in `Lp`. -/
theorem mem_Lp (f : α →ᵇ E) : f.toContinuousMap.toAEEqFun μ ∈ Lp E p μ :=
by
refine Lp.mem_Lp_of_ae_bound ‖f‖ ?_
filter_upwards [f.toContinuousMap.coeFn_toAEEqFun μ] with x _
convert f.norm_coe_le_norm x using 2
