inner_products_summable — Mathlib

English

The identity index bijection yields the identity isometry on the basis.

Русский

Идентичная биекция индексов даёт тождественную изоморфную изометрическую трансформацию базиса.

LaTeX

$$$hv.equiv hv (Equiv.refl ι) = LinearIsometryEquiv.refl 𝕜 E$$$

Lean4

/-- The sum defined in Bessel's inequality is summable. -/
theorem inner_products_summable (hv : Orthonormal 𝕜 v) : Summable fun i => ‖⟪v i, x⟫‖ ^ 2 :=
  by
  use ⨆ s : Finset ι, ∑ i ∈ s, ‖⟪v i, x⟫‖ ^ 2
  apply hasSum_of_isLUB_of_nonneg
  · intro b
    simp only [norm_nonneg, pow_nonneg]
  · refine isLUB_ciSup ?_
    use ‖x‖ ^ 2
    rintro y ⟨s, rfl⟩
    exact hv.sum_inner_products_le x

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