English
The space lp E p carries a norm defined by the standard L^p formula: for p = 0 it counts nonzero coordinates, for p = ∞ it takes the supremum of norms, and otherwise it uses the p-norm sum.
Русский
Пространство lp E p обладает нормой, заданной обычной формулой L^p: при p = 0 учитывается число ненулевых координат; при p = ∞ берётся супремум норм; иначе применяется p-норма.
LaTeX
$$$\\|f\\| = \\begin{cases} \\#\\{ i : f(i) \\neq 0 \\}, & p = 0 \\\\ \\sup_i \\|f(i)\\|, & p = \\infty \\\\ \\left( \\sum_i \\|f(i)\\|^{{\\rm p.real}} \\right)^{1/ {\\rm p.real}}, & \\text{otherwise} \\end{cases}$$$
Lean4
instance : Norm (lp E p) where
norm
f :=
if hp : p = 0 then by
subst hp
exact ((lp.memℓp f).finite_dsupport.toFinset.card : ℝ)
else if p = ∞ then ⨆ i, ‖f i‖ else (∑' i, ‖f i‖ ^ p.toReal) ^ (1 / p.toReal)
