English
Let p be such that 0 < p.toReal and f, g ∈ WithLp p (α × β). Then the edistance is the Lp‑norm of the coordinatewise distances: edist(f,g) = (edist(f.fst,g.fst)^{p.toReal} + edist(f.snd,g.snd)^{p.toReal})^{1/p.toReal}.
Русский
Пусть p удовлетворяет 0 < p.toReal и f, g ∈ WithLp p (α × β). Тогда edist(f,g) равен p‑наимной норме по координатам: edist(f,g) = (edist(f.fst,g.fst)^{p.toReal} + edist(f.snd,g.snd)^{p.toReal})^{1/p.toReal}.
LaTeX
$$$$\operatorname{edist} f g = \Big( \operatorname{edist} f.fst g.fst^{\;p.toReal} + \operatorname{edist} f.snd g.snd^{\;p.toReal} \Big)^{1 / p.toReal}$$$$
Lean4
theorem prod_edist_eq_add (hp : 0 < p.toReal) (f g : WithLp p (α × β)) :
edist f g = (edist f.fst g.fst ^ p.toReal + edist f.snd g.snd ^ p.toReal) ^ (1 / p.toReal) :=
let hp' := ENNReal.toReal_pos_iff.mp hp
(if_neg hp'.1.ne').trans (if_neg hp'.2.ne)
