boundedContinuousFunction — Mathlib

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 μ)

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