norm_sq_eq — Mathlib

English

In a finite-product Euclidean space, the square of the norm is the sum of the squares of the coordinate norms: ∥x∥^2 = ∑_i ∥x_i∥^2.

Русский

В конечном произведении Евклидова пространства квадрат нормы равен сумме квадратов норм координат: ∥x∥^2 = ∑_i ∥x_i∥^2.

LaTeX

$$$\|x\|^2 = \sum_i \|x_i\|^2$$$

Lean4

theorem norm_sq_eq {𝕜 : Type*} [RCLike 𝕜] {n : Type*} [Fintype n] (x : EuclideanSpace 𝕜 n) : ‖x‖ ^ 2 = ∑ i, ‖x i‖ ^ 2 :=
  PiLp.norm_sq_eq_of_L2 _ x

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