sum_sq_norm_inner_left — Mathlib

English

Equivalently, the same identity holds with the inner product on the other side: ∑_i ‖⟪x, b_i⟫‖^2 = ‖x‖^2.

Русский

Аналогично, та же тождество и слева: ∑_i ‖⟪x, b_i⟫‖^2 = ‖x‖^2.

LaTeX

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

Lean4

theorem sum_sq_norm_inner_left (b : OrthonormalBasis ι 𝕜 E) (x : E) : ∑ i, ‖⟪x, b i⟫‖ ^ 2 = ‖x‖ ^ 2 :=
  by
  convert sum_sq_norm_inner_right b x using 2 with i -
  rw [← inner_conj_symm, RCLike.norm_conj]

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