English
Endowing WithLp p (α × β) with the L^p distance, the distance between f and g is defined by the standard L^p combination of their coordinates, with special cases for p = 0 and p = ∞.
Русский
С помощью L^p-расстояния на WithLp p (α × β) расстояние между f и g задаётся обычной комбинацией по координатам: для p = 0 и p = ∞ имеются особые случаи.
LaTeX
$$$\\operatorname{dist}_{WithLp,p}(f,g) = \\begin{cases} (\\operatorname{dist}(f.fst,g.fst) = 0 ? 0 : 1) + (\\operatorname{dist}(f.snd,g.snd) = 0 ? 0 : 1), & p = 0 \\\\ dist(f.fst,g.fst) \\sqcup dist(f.snd,g.snd), & p = \\infty \\\\ \\big( dist(f.fst,g.fst)^{p.toReal} + dist(f.snd,g.snd)^{p.toReal} \\big)^{1/p.toReal}, & \\text{otherwise} \\end{cases} $$$
Lean4
/-- Endowing the space `WithLp p (α × β)` with the `L^p` distance. We register this instance
separate from `WithLp.instProdPseudoMetricSpace` 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 `WithLp 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 instProdDist : Dist (WithLp p (α × β)) where
dist f
g :=
if _hp : p = 0 then (if dist f.fst g.fst = 0 then 0 else 1) + (if dist f.snd g.snd = 0 then 0 else 1)
else
if p = ∞ then dist f.fst g.fst ⊔ dist f.snd g.snd
else (dist f.fst g.fst ^ p.toReal + dist f.snd g.snd ^ p.toReal) ^ (1 / p.toReal)
