English
For the distance with p=0, dist f g equals the count of coordinates where dist(f_i,g_i) ≠ 0.
Русский
Для p=0 расстояние dist(f,g) равно число координат, где dist(f_i,g_i) ≠ 0.
LaTeX
$$$$dist(f,g)=\\lvert\\{i\\;|\\;dist(f_i,g_i)\\neq 0\\}\\rvert$$$$
Lean4
/-- Endowing the space `PiLp p β` with the `L^p` distance. We register this instance
separate from `pi_Lp.pseudo_metric` 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 metric-like structure on `PiLp p β` for `p < 1`
satisfying a relaxed triangle inequality. The terminology for this varies throughout the
literature, but it is sometimes called a *quasi-metric* or *semi-metric*. -/
instance : Dist (PiLp p α) where
dist f
g :=
if p = 0 then {i | dist (f i) (g i) ≠ 0}.toFinite.toFinset.card
else if p = ∞ then ⨆ i, dist (f i) (g i) else (∑ i, dist (f i) (g i) ^ p.toReal) ^ (1 / p.toReal)
