nnnorm_ofLp — Mathlib

English

The NN-norm of form toLp equals the NN-norm of the original function: ‖nnnorm (toLp f)‖₊ = ‖nnnorm f‖₊.

Русский

NN-норма преобразования toLp равна NN-норме исходной функции: ‖toLp f‖₊ = ‖f‖₊.

LaTeX

$$$$ \|\mathrm{toLp}\,\infty\, f\|_{+} = \|f\|_{+} $$$$

Lean4

@[simp]
theorem nnnorm_ofLp (f : PiLp ∞ β) : ‖ofLp f‖₊ = ‖f‖₊ :=
  by
  rw [nnnorm_eq_ciSup, Pi.nnnorm_def, Finset.sup_univ_eq_ciSup]
  dsimp only [ofLp_apply]

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