Theorems · Definition · functional analysis

HilbertBasis.toSchauderBasis

{𝕜 : Type u_2} →
  [inst : RCLike 𝕜] →
    {E : Type u_3} →
      [inst_1 : NormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → HilbertBasis ℕ 𝕜 E → SchauderBasis 𝕜 E

Every Hilbert basis indexed by ℕ is a Schauder basis (SchauderBasis) with coordinate functionals x ↦ ⟪b i, x⟫. The expansion x = ∑ i, ⟪b i, x⟫ • b i converges.

Defined in

Mathlib.Analysis.InnerProductSpace.l2Space

Cited by

2 results in Mathlib

Foundations

Depth 239 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeNormedAddCommGroupInnerProductSpace