TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-16

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.

Bessel's inequality for a finite orthonormal list and Parseval's identity for an orthonormal basis

Statement

If $(e_{0}, \dots, e_{r - 1})$ is a finite orthonormal list and $v$ is any vector, then

$\sum_{i < r} ∣ ⟨ v, e_{i} ⟩ ∣^{2} \leq ∥ v ∥^{2} .$

Equality holds exactly when $v \in span (e_{0}, \dots, e_{r - 1})$ . If the list is an orthonormal basis, then for all $v, w$ ,

$v = \sum_{i < r} ⟨ v, e_{i} ⟩ e_{i}, ⟨ v, w ⟩ = \sum_{i < r} ⟨ v, e_{i} ⟩ \overline{⟨ w, e_{i} ⟩},$

and

$∥ v ∥^{2} = \sum_{i < r} ∣ ⟨ v, e_{i} ⟩ ∣^{2} .$

The empty-list case is included.

Facts & Assumptions

Given: A finite orthonormal list $(e_{i})_{i < r}$ and vectors $v, w$ .

[L1]

Orthonormality gives $⟨ e_{i}, e_{j} ⟩ = 0$ for $i \neq j$ and $⟨ e_{i}, e_{i} ⟩ = 1$ (Orthogonal vectors and subspaces, orthogonal and orthonormal sets, and orthonormal bases).

[L2]

Orthogonal vectors satisfy the Pythagorean identity (Pythagoras, the parallelogram identity, and the real and complex polarisation identities).

[L3]

$span (S) = L (S)$ , the set of finite linear combinations $\sum_{i < n} λ_{i} v_{i}$ of elements of $S$ ( $span (S)$ is exactly the set of linear combinations of finite lists of elements of $S$ , and $span (\emptyset) = {0_{V}}$ ).

[L4]

Finite sums include the empty sum, whose additive value is zero (The product $g_{0} g_{1} \dots g_{n - 1}$ of a finite list in a monoid, by recursion, with the empty product ( $n = 0$ ) equal to the identity).

Proof

technique · direct

1.1

Put $p = \sum_{i < r} ⟨ v, e_{i} ⟩ e_{i}$ . For each $j < r$ , [L1] gives $⟨ v - p, e_{j} ⟩ = 0$ , so $v - p$ is orthogonal to $p$ .

L1algebra

2.1

By [L2], $∥ v ∥^{2} = ∥ p ∥^{2} + ∥ v - p ∥^{2}$ . A second use of orthonormality gives $∥ p ∥^{2} = \sum_{i < r} ∣ ⟨ v, e_{i} ⟩ ∣^{2}$ , proving Bessel's inequality.

step 1.1L1L2

3.1

Equality holds in step 2.1 exactly when $∥ v - p ∥ = 0$ , hence exactly when $v = p$ . By [L3], this is exactly $v$ belonging to the listed span.

step 2.1L3

4.1

If the list is a basis, its span is $V$ , so step 3.1 gives the coordinate expansion and the squared-length identity. Substitute the coordinate expansion of $v$ into $⟨ v, w ⟩$ and use conjugate symmetry to obtain the displayed inner-product formula.

step 3.1L1algebra

5.1

When $r = 0$ , [L4] makes every displayed sum zero; the list can be a basis only of the zero space, so all assertions remain valid.

L4∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 49 results over 20 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Sheldon Axler, Linear Algebra Done Right, 4th ed., results 6.24, 6.26, and 6.30 (standard reference, not scraped)