sum_sq_norm_inner_right — Mathlib

English

Let b be an orthonormal basis; then the sum of squared norms of the inner products ⟪b_i, x⟫ equals the squared norm of x: ∑_i ‖⟪b_i, x⟫‖^2 = ‖x‖^2.

Русский

Пусть b — ортонормированный базис; тогда сумма квадратов модулей скалярных произведений ‖⟪b_i, x⟫‖^2 равна ‖x‖^2.

LaTeX

$$$\sum_i \|\langle b_i, x \rangle\|^2 = \|x\|^2$$$

Lean4

theorem sum_sq_norm_inner_right (b : OrthonormalBasis ι 𝕜 E) (x : E) : ∑ i, ‖⟪b i, x⟫‖ ^ 2 = ‖x‖ ^ 2 :=
  by
  rw [@norm_eq_sqrt_re_inner 𝕜, ← OrthonormalBasis.sum_inner_mul_inner b x x, map_sum]
  simp_rw [inner_mul_symm_re_eq_norm, norm_mul, ← inner_conj_symm x, starRingEnd_apply, norm_star, ← pow_two]
  rw [Real.sq_sqrt]
  exact Fintype.sum_nonneg fun _ ↦ by positivity

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