tsum_inner_products_le — Mathlib

English

For any i, hv.equiv hv' e applied to v_i equals v'_i' as prescribed by the index equivalence.

Русский

Для любого i hv.equiv hv' e применено к v_i равно соответствующему v'_{e(i)} согласно эквивалентности индексов.

LaTeX

$$$hv.equiv hv' e (v i) = v' (e i)$$$

Lean4

/-- Bessel's inequality. -/
theorem tsum_inner_products_le (hv : Orthonormal 𝕜 v) : ∑' i, ‖⟪v i, x⟫‖ ^ 2 ≤ ‖x‖ ^ 2 :=
  by
  refine tsum_le_of_sum_le' ?_ fun s => hv.sum_inner_products_le x
  simp only [norm_nonneg, pow_nonneg]

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