ExampleConstruction: AI-adaptedVerification: 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.

Legendre polynomials from Gram–Schmidt

Example

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). On the real Hilbert space $L^{2} ([- 1, 1])$ with the integral pairing ( $L^{2}$ with the integral pairing is a Hilbert space) apply Gram–Schmidt elimination to the sequence of monomial classes $1, x, x^{2}, \dots$ (Gram–Schmidt turns every finite independent list into an orthonormal list with the same successive spans). The result is a complete orthonormal family — an orthonormal basis of $L^{2} ([- 1, 1])$ — whose first three members are

$e_{0} = \frac{1}{\sqrt{2}}, e_{1} = \sqrt{\frac{3}{2}} x, e_{2} = \sqrt{\frac{5}{8}} (3 x^{2} - 1) .$

The corresponding unnormalised polynomials with value $1$ at $x = 1$ are $P_{0} = 1$ , $P_{1} = x$ , and $P_{2} = (3 x^{2} - 1) / 2$ , the first three classical Legendre polynomials. No general formula for $P_{n}$ or its norm is asserted here.

Facts & Assumptions

[A1]

Every finite initial monomial list $(1, x, \dots, x^{r})$ is linearly independent as a list of $L^{2} ([- 1, 1])$ classes: a nontrivial linear combination is a nonzero polynomial, which has only finitely many roots, so some nondegenerate subinterval of $[- 1, 1]$ contains no root and has positive Lebesgue measure; the combination therefore cannot vanish almost everywhere (A nonzero real polynomial of degree $n$ has no more than $n$ distinct real roots, A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included). Finite Gram–Schmidt sends each such list to an orthonormal list with the same successive spans, using the displayed residual formula (Gram–Schmidt turns every finite independent list into an orthonormal list with the same successive spans).

[A2]

The polynomials are uniformly dense in $C ([- 1, 1], R)$ , and continuous functions are dense in $L^{2}$ of a bounded interval, so the $L^{2}$ -closure of the polynomials is all of $L^{2} ([- 1, 1])$ (Polynomials are uniformly dense in $C ([a, b], R)$ for every closed interval, Continuous functions are dense in $L^{p}$ of finite tori and of bounded intervals).

[A3]

The pairing on real $L^{2}$ is $⟨ f, g ⟩ = \int f g$ ; for continuous real functions on $[- 1, 1]$ the $L^{2}$ integral is the Riemann integral over $[- 1, 1]$ , and the Riemann integral is computed by the second fundamental theorem with the power rule ( $L^{2}$ with the integral pairing is a Hilbert space, A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral, The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ , For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term).

[A4]

A complete orthonormal family, equivalently an orthonormal family with closed linear span the whole space, is an orthonormal basis (Orthonormal families, complete orthonormal systems and Hilbert bases).

Verification

technique · direct

Given: The sequence of monomial classes $1, x, x^{2}, \dots$ in $L^{2} ([- 1, 1], R)$ .

1.1

For each $r$ , apply finite Gram–Schmidt to $(1, x, \dots, x^{r})$ . By [A1] every residual is nonzero, and the recursive formula is independent of how far the finite list is extended, so these finite outputs are compatible and define one orthonormal sequence $(e_{n})_{n \in N}$ . The successive-span identity gives $span {e_{0}, \dots, e_{r}} = span {1, x, \dots, x^{r}}$ for every $r$ . Hence the sequence and the monomials have the same closed linear span; this is all of $L^{2} ([- 1, 1])$ , because the polynomials are uniformly dense in $C ([- 1, 1])$ and the continuous functions are dense in $L^{2}$ . Thus $(e_{n})$ is a complete orthonormal family, that is, an orthonormal basis.

A1A2A4

1.2

First element: $x_{0} = 1$ has $∥ 1 ∥_{2}^{2} = \int_{- 1}^{1} 1 d x = 2$ , so $e_{0} = 1 / \sqrt{2}$ .

A1A3

2.1

Second element: $v_{1} = x - ⟨ x, e_{0} ⟩ e_{0}$ with $⟨ x, e_{0} ⟩ = \frac{1}{\sqrt{2}} \int_{- 1}^{1} x d x = 0$ , so $v_{1} = x$ and $∥ x ∥_{2}^{2} = \int_{- 1}^{1} x^{2} d x = [x^{3} / 3]_{- 1}^{1} = \frac{2}{3}$ , giving $e_{1} = \sqrt{3 / 2} x$ .

step 1.2A1A3

3.1

Third element: $v_{2} = x^{2} - ⟨ x^{2}, e_{0} ⟩ e_{0} - ⟨ x^{2}, e_{1} ⟩ e_{1}$ with $⟨ x^{2}, e_{1} ⟩ = \sqrt{\frac{3}{2}} \int_{- 1}^{1} x^{3} d x = 0$ and $⟨ x^{2}, e_{0} ⟩ = \frac{1}{\sqrt{2}} \int_{- 1}^{1} x^{2} d x = \frac{1}{\sqrt{2}} \cdot \frac{2}{3}$ , so $v_{2} = x^{2} - \frac{1}{3}$ ; its squared norm is $\int_{- 1}^{1} (x^{2} - \frac{1}{3})^{2} d x = [x^{5} / 5 - \frac{2}{9} x^{3} + \frac{1}{9} x]_{- 1}^{1} = \frac{2}{5} - \frac{4}{9} + \frac{2}{9} = \frac{8}{45}$ , giving $e_{2} = \sqrt{45 / 8} (x^{2} - \frac{1}{3}) = \sqrt{5 / 8} (3 x^{2} - 1)$ .

step 1.2step 2.1A1A3algebra

4.1

Therefore the Gram–Schmidt family of the monomials is a complete orthonormal family of $L^{2} ([- 1, 1])$ beginning with $1 / \sqrt{2}$ , $\sqrt{3 / 2} x$ and $\sqrt{5 / 8} (3 x^{2} - 1)$ . Rescaling these three displayed unit vectors to have value $1$ at $x = 1$ gives $P_{0} = 1$ , $P_{1} = x$ , and $P_{2} = (3 x^{2} - 1) / 2$ .

step 1.1step 1.2step 2.1step 3.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

95 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.50, example after Theorem 2.3 (standard reference, not scraped)
Theo Bühler and Dietmar Salamon, Functional Analysis — Exercise 2.63, p.87 (standard reference, not scraped)