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.

The Haar orthonormal basis of $L^{2} ((0, 1))$

Example

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). For integers $j \geq 0$ and $0 \leq k < 2^{j}$ let $I_{j, k} : = [k 2^{- j}, (k + 1) 2^{- j})$ be the dyadic interval of level $j$ , split at its midpoint $m_{j, k} : = (2 k + 1) 2^{- j - 1}$ , and let $h_{j, k} : = 2^{j / 2} (1_{[k 2^{- j}, m_{j, k})} - 1_{[m_{j, k}, (k + 1) 2^{- j})})$ . Then the family consisting of the constant function $1$ and of all $h_{j, k}$ with $j \geq 0$ , $0 \leq k < 2^{j}$ , is an orthonormal basis of $L^{2} ((0, 1))$ for Lebesgue measure, in the real and in the complex case (Orthonormal families, complete orthonormal systems and Hilbert bases, $L^{2}$ with the integral pairing is a Hilbert space).

Facts & Assumptions

[A1]

The dyadic intervals of level $j$ partition $[0, 1)$ into $2^{j}$ half-open intervals of length $2^{- j}$ .

[A2]

Indicators of measurable sets of finite measure have integral equal to their measure; finite linear combinations have the corresponding linear combination of integrals (The integral of a nonnegative simple function, The nonnegative integral agrees with the simple integral on simple functions, The Lebesgue integral is linear on $L^{1} (μ)$ ). The interval $[a, b)$ has Lebesgue measure $b - a$ , and singleton endpoints have measure zero, so restricting these indicators to $(0, 1)$ does not alter the calculations below (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).

[A3]

The Hilbert space $L^{2} ((0, 1))$ has pairing $\int f g$ in the real case and $\int f \overline{g}$ in the complex case, and orthogonality of a family means the vanishing of these pairings on distinct indices ( $L^{2}$ with the integral pairing is a Hilbert space, Real and complex inner-product spaces and their induced length).

[A4]

A continuous function on the compact metric space $[0, 1]$ is uniformly continuous (Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous, Heine-Borel by bisection: every closed bounded interval $[a, b]$ is compact), and the restrictions to $(0, 1)$ of continuous functions on $[0, 1]$ are dense in $L^{2} ((0, 1))$ (Continuous functions are dense in $L^{p}$ of finite tori and of bounded intervals).

Verification

technique · direct

Given: The family ${1} \cup {h_{j, k} : j \geq 0, 0 \leq k < 2^{j}}$ in $L^{2} ((0, 1))$ .

1.1

Orthonormality and $\int_{0}^{1} h_{j, k} = 0$ : each $h_{j, k}$ takes the two values $\pm 2^{j / 2}$ on two intervals of equal length $2^{- j - 1}$ , so its integral over $R$ is $2^{j / 2} (2^{- j - 1} - 2^{- j - 1}) = 0$ and $∥ h_{j, k} ∥_{2}^{2} = 2^{j} \cdot 2 \cdot 2^{- j - 1} = 1$ . Two distinct such functions either have disjoint supports, giving pairing $0$ , or have nested supports $I_{j^{'}, k^{'}} \subseteq I_{j, k}$ with $j^{'} > j$ , and the finer interval lies wholly in one half of the coarser interval, so the coarser function is constant there. Then the pairing is $\pm 2^{j / 2} \int h_{j^{'}, k^{'}} = 0$ because the integral of the finer function vanishes; and $⟨ 1, h_{j, k} ⟩ = \int h_{j, k} = 0$ , while $∥ 1 ∥_{2}^{2} = 1$ .

A1A2A3

1.2

Every continuous $f : [0, 1] \to C$ is uniformly approximated on $[0, 1)$ by functions constant on the level- $J$ dyadic intervals: by uniform continuity choose $δ > 0$ with $∣ f (x) - f (y) ∣ < ε$ whenever $∣ x - y ∣ < δ$ , choose $J$ with $2^{- J} < δ$ , and let $s_{J}$ be the function that on each level- $J$ interval takes the value of $f$ at its left endpoint; then $\sup_{x \in [0, 1)} ∣ f (x) - s_{J} (x) ∣ \leq ε$ and hence $∥ f - s_{J} ∥_{L^{2} ((0, 1))} \leq ε$ .

A2A3A4

2.1

For every $J \geq 0$ the linear span of ${1} \cup {h_{j, k} : j < J}$ is exactly the space $V_{J}$ of functions constant on each level- $J$ dyadic interval: the two functions $1_{[a, m)}$ and $1_{[m, b)}$ of a level- $(j + 1)$ interval inside a level- $j$ interval are $(1_{[a, b)} \pm 2^{- j / 2} h_{j, k}) / 2$ , so by induction every level- $J$ dyadic indicator lies in the span, and conversely every $h_{j, k}$ with $j < J$ is a linear combination of level- $J$ indicators; hence the span is contained in $V_{J}$ and contains all its indicators.

step 1.1A1A2algebra

3.1

Therefore the closed linear span of the family is $L^{2} ((0, 1))$ : it contains $V_{J}$ for every $J$ by step 2.1, hence by step 1.2 it contains the restrictions of $C ([0, 1])$ , and their $L^{2} ((0, 1))$ -closure is $L^{2} ((0, 1))$ .

step 1.2step 2.1A4

4.1

Since the family is orthonormal by step 1.1 and its closed linear span is all of $L^{2} ((0, 1))$ by step 3.1, it is an orthonormal basis of $L^{2} ((0, 1))$ in both the real and the complex case.

step 1.1step 3.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

96 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

Vladimir Dobrushkin, Eigenfunction Expansion, APMA0360 course tutorial — Example 5, dyadic functions and span discussion (standard reference, not scraped)
Gerald Teschl, Topics in Real and Functional Analysis, version November 17, 2017 — §2.1, p.50 (standard reference, not scraped)

The Haar orthonormal basis of L2((0,1))L2((0,1))