English
For a bounded continuous function f on a finite-measure space, its Lp norm is bounded above by a universal constant times its sup-norm.
Русский
Для ограниченной непрерывной функции f на пространстве с конечной мерой её Lp-норма не превышает константы, умноженной на её суп-норма.
LaTeX
$$$\\| \mathrm{toLp}(f) \\|_{Lp} \\le \\mathrm{measureUnivNNReal}(\\mu)^{p^{\\mathrm{real}-1}} \\|f\\|_{\\infty}. $$$
Lean4
/-- An additive subgroup of `Lp E p μ`, consisting of the equivalence classes which contain a
bounded continuous representative. -/
def boundedContinuousFunction : AddSubgroup (Lp E p μ) :=
AddSubgroup.addSubgroupOf ((ContinuousMap.toAEEqFunAddHom μ).comp (toContinuousMapAddHom α E)).range (Lp E p μ)