norm_sq_eq_of_L2 — Mathlib

English

For x,y ∈ PiLp 2 β, the distance is the Euclidean-type distance: dist(x,y) = (∑_i dist(x_i,y_i)^2)^{1/2}.

Русский

Для x,y ∈ PiLp 2 β расстояние равно евклидовой форме: dist(x,y) = (∑_i dist(x_i,y_i)^2)^{1/2}.

LaTeX

$$$\operatorname{dist}(x,y) = \sqrt{\sum_{i\in ι} \operatorname{dist}(x_i,y_i)^{2}},\quad x,y\in PiLp\;2\;β$$$

Lean4

theorem norm_sq_eq_of_L2 (β : ι → Type*) [∀ i, SeminormedAddCommGroup (β i)] (x : PiLp 2 β) :
    ‖x‖ ^ 2 = ∑ i : ι, ‖x i‖ ^ 2 :=
  by
  suffices ‖x‖₊ ^ 2 = ∑ i : ι, ‖x i‖₊ ^ 2 by simpa only [NNReal.coe_sum] using congr_arg ((↑) : ℝ≥0 → ℝ) this
  rw [nnnorm_eq_of_L2, NNReal.sq_sqrt]

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