norm_eq_sum — Mathlib

English

PiLp p β carries the Lp-norm: ‖f‖ is defined by the usual Lp formula, with special cases for p=0 and p=∞.

Русский

PiLp p β снабжено Lp-нормой: ‖f‖ задается по обычной формуле Lp, с особенными случаями p=0 и p=∞.

LaTeX

$$$$\\|f\\|=\\begin{cases} \\lvert\\{i\\;|\\;\\|f_i\\|\\neq 0\\}\\rvert,& p=0,\\\\[2mm] \\left(\\sum_i \\|f_i\\|^{p^{\\mathrm{toReal}}}\\right)^{1/p^{\\mathrm{toReal}}},& \\text{otherwise}\\end{cases}$$$$

Lean4

theorem norm_eq_sum (hp : 0 < p.toReal) (f : PiLp p β) : ‖f‖ = (∑ i, ‖f i‖ ^ p.toReal) ^ (1 / p.toReal) :=
  let hp' := ENNReal.toReal_pos_iff.mp hp
  (if_neg hp'.1.ne').trans (if_neg hp'.2.ne)

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