TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedaudited 2026-09-22

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The Bessel inequality for an arbitrary orthonormal family

Statement

Let $(e_{i})_{i \in I}$ be an orthonormal family in a real or complex inner-product space $H$ (Orthonormal families, complete orthonormal systems and Hilbert bases). Then for every $x \in H$ the nonnegative family $(∣ ⟨ x, e_{i} ⟩ ∣^{2})_{i \in I}$ has finite sum in the finite-subset-supremum convention (Square-summable families on an arbitrary index set and the space $ℓ^{2} (I)$ ) and

$\sum_{i \in I} ∣ ⟨ x, e_{i} ⟩ ∣^{2} \leq ∥ x ∥^{2} .$

In particular the coefficient family $(⟨ x, e_{i} ⟩)_{i \in I}$ belongs to $ℓ^{2} (I, F)$ , and the inequality holds with no hypothesis on the cardinality of $I$ and with no completeness of $H$ .

Facts & Assumptions

[A1]

For every finite $F \subseteq I$ , $\sum_{i \in F} ∣ ⟨ x, e_{i} ⟩ ∣^{2} \leq ∥ x ∥^{2}$ ; the sum over the empty set is $0$ (The finite Bessel inequality and best approximation by a finite orthonormal family).

[A2]

The arbitrary sum $\sum_{i \in I} ∣ ⟨ x, e_{i} ⟩ ∣^{2}$ is the supremum in $[0, + \infty]$ of the finite subsums, and it is a real number exactly when that set of finite subsums is bounded above (Square-summable families on an arbitrary index set and the space $ℓ^{2} (I)$ ).

[A3]

$∥ x ∥^{2}$ is a nonnegative real number, and a family belongs to $ℓ^{2} (I, F)$ exactly when its square sum is finite (Square-summable families on an arbitrary index set and the space $ℓ^{2} (I)$ ).

Proof

technique · direct

Given: An orthonormal family $(e_{i})_{i \in I}$ in $H$ and a vector $x \in H$ .

1.1

Every finite $F \subseteq I$ satisfies $\sum_{i \in F} ∣ ⟨ x, e_{i} ⟩ ∣^{2} \leq ∥ x ∥^{2}$ , so the set of finite subsums of the family $(∣ ⟨ x, e_{i} ⟩ ∣^{2})_{i \in I}$ is nonempty and bounded above by the real number $∥ x ∥^{2}$ .

A1A3

2.1

Consequently the arbitrary sum $\sum_{i \in I} ∣ ⟨ x, e_{i} ⟩ ∣^{2}$ is a real number and is at most $∥ x ∥^{2}$ , being the supremum of a nonempty set of reals bounded above by $∥ x ∥^{2}$ .

step 1.1A2A3

3.1

The value $\sum_{i \in I} ∣ ⟨ x, e_{i} ⟩ ∣^{2}$ is finite, so the coefficient family $(⟨ x, e_{i} ⟩)_{i \in I}$ lies in $ℓ^{2} (I, F)$ , and the Bessel inequality $\sum_{i \in I} ∣ ⟨ x, e_{i} ⟩ ∣^{2} \leq ∥ x ∥^{2}$ holds.

step 2.1A3∎

Depends on

Used by

Dependency tree · two levels

24 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Gerald Teschl, Topics in Real and Functional Analysis, version November 17, 2017 — §2.1, p.48, equation (2.4) (standard reference, not scraped)
Theo Bühler and Dietmar Salamon, Functional Analysis — Theorem 2.65 area, p.87 (standard reference, not scraped)