English
In the Lp product space PiLp p β, the distance is the p-th root of the sum of the p-th powers of component distances: nndist(x,y) = (∑ i nndist(x_i, y_i)^p.toReal)^(1/p.toReal).
Русский
В пространстве Lp-произведения PiLp p β расстояние равно корню p-й степени из суммы p-й степени расстояний компонент: nndist(x,y) = (∑ i nndist(x_i, y_i)^p)^(1/p).
LaTeX
$$$\mathrm{nndist}(x,y) = \left( \sum_{i} \mathrm{nndist}(x_i,y_i)^{p} \right)^{\frac{1}{p}}.$$$
Lean4
theorem nndist_eq_sum {p : ℝ≥0∞} [Fact (1 ≤ p)] {β : ι → Type*} [∀ i, PseudoMetricSpace (β i)] (hp : p ≠ ∞)
(x y : PiLp p β) : nndist x y = (∑ i : ι, nndist (x i) (y i) ^ p.toReal) ^ (1 / p.toReal) :=
NNReal.eq <| by
push_cast
exact dist_eq_sum (p.toReal_pos_iff_ne_top.mpr hp) _ _
