English
Let (G_i) be normed spaces, V_i: G_i → E be linear isometries forming an orthogonal family. Then for any l_i ∈ G_i and any finite subset s, the squared norm of the sum ∑_{i∈s} V_i(l_i) equals the sum of squared norms ∑_{i∈s} ∥l_i∥^2.
Русский
Пусть (G_i) — семейство нормированных пространств, V_i: G_i → E — линейные изометрии, образующие ортогональную семью. Тогда для любых l_i ∈ G_i и конечного подмножества s, выполняется равенство \n∥ ∑_{i∈s} V_i(l_i) ∥^2 = ∑_{i∈s} ∥l_i∥^2.
LaTeX
$$$\\Big\\|\\sum_{i \\in s} V_i(l_i)\\Big\\|^2 = \\sum_{i \\in s} \\|l_i\\|^2.$$$
Lean4
theorem norm_sum (l : ∀ i, G i) (s : Finset ι) : ‖∑ i ∈ s, V i (l i)‖ ^ 2 = ∑ i ∈ s, ‖l i‖ ^ 2 :=
by
have : ((‖∑ i ∈ s, V i (l i)‖ : ℝ) : 𝕜) ^ 2 = ∑ i ∈ s, ((‖l i‖ : ℝ) : 𝕜) ^ 2 := by
simp only [← inner_self_eq_norm_sq_to_K, hV.inner_sum]
exact mod_cast this
