norm_toLp — Mathlib

English

The norm of the Lp-image of a simple function equals the real eLp-norm of the original function.

Русский

Норма изображения в Lp простой функции равна вещественному eLp-норму исходной функции.

LaTeX

$$$\|toLp(f)\| = \operatorname{toReal}(eLpNorm(f,p,\mu))$$$

Lean4

nonrec theorem norm_toLp [Fact (1 ≤ p)] (f : α →ₛ E) (hf : MemLp f p μ) :
    ‖toLp f hf‖ = ENNReal.toReal (eLpNorm f p μ) :=
  norm_toLp f hf

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