instEDist — Mathlib

English

Endowing PiLp p β with the Lp edistance, we have edist(f,g) = (∑_i edist(f_i,g_i)^p.toReal)^{1/p.toReal} for p in (0,∞), with the usual special cases p=0 and p=∞.

Русский

На пространстве PiLp p β задается расстояние Lp: edist(f,g) = (∑ edist(f_i,g_i)^p)^{1/p} для p∈(0,∞), с особыми случаями p=0 и p=∞.

LaTeX

$$$\\mathrm{edist}(f,g)=\\begin{cases} \\lvert\\{i\\mid \\mathrm{edist}(f_i,g_i)\\neq 0\\}\\rvert,& p=0,\\\\[2mm] \\bigl(\\sum_i \\mathrm{edist}(f_i,g_i)^p\\bigr)^{1/p},& 0

Lean4

/-- Endowing the space `PiLp p β` with the `L^p` edistance. We register this instance
separate from `pi_Lp.pseudo_emetric` 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 emetric-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 : EDist (PiLp p β) where
  edist f
    g :=
    if p = 0 then {i | edist (f i) (g i) ≠ 0}.toFinite.toFinset.card
    else if p = ∞ then ⨆ i, edist (f i) (g i) else (∑ i, edist (f i) (g i) ^ p.toReal) ^ (1 / p.toReal)

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