English
For general p, dist f g is the Lp-sum distance: dist f g = (∑ dist(f_i,g_i)^{p.toReal})^{1/p.toReal} when Real p>0.
Русский
Для общего p расстояние имеет Lp-форму: dist f g = (∑ dist(f_i,g_i)^{p.toReal})^{1/p.toReal} при p>0 в реальном смысле.
LaTeX
$$$$dist(f,g)=\\left(\\sum_i dist(f_i,g_i)^{p^{\\mathrm{toReal}}}\\right)^{1/p^{\\mathrm{toReal}}}$$$$
Lean4
/-- Endowing the space `PiLp p β` with the `L^p` norm. We register this instance
separate from `PiLp.seminormedAddCommGroup` since the latter requires the type class hypothesis
`[Fact (1 ≤ p)]` in order to prove the triangle inequality.
Registering this separately allows for a future norm-like structure on `PiLp p β` for `p < 1`
satisfying a relaxed triangle inequality. These are called *quasi-norms*. -/
instance instNorm : Norm (PiLp p β) where
norm
f :=
if p = 0 then {i | ‖f i‖ ≠ 0}.toFinite.toFinset.card
else if p = ∞ then ⨆ i, ‖f i‖ else (∑ i, ‖f i‖ ^ p.toReal) ^ (1 / p.toReal)
