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 Fourier series of a square wave and the odd reciprocal-square sum

Example

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $s$ be the class in $L^{2} (T; C)$ represented on $[0, 1)$ by $s (t) = 1$ for $0 \leq t < \frac{1}{2}$ and $s (t) = - 1$ for $\frac{1}{2} \leq t < 1$ , the $1$ -periodic extension of the sign function on $(- \frac{1}{2}, \frac{1}{2})$ ; the endpoint values are immaterial for the class. Then

$\hat{s} (0) = 0, \hat{s} (k) = \frac{1 - (- 1)^{k}}{π i k} (k \neq 0),$

the Fourier series of $s$ converges to $s$ in mean square (Fourier series converge in mean square), and Parseval's identity gives $\sum_{k odd, k \geq 1} k^{- 2} = π^{2} / 8$ . The example deliberately claims norm convergence and nothing else: it asserts no pointwise convergence of the series to the values of this representative at the jump, and no endpoint statement is made.

Facts & Assumptions

[A1]

$\hat{s} (k) = \int_{T} s e_{- k} d m_{T}$ is represented on $[0, 1)$ by the Riemann integral of the representative against $e^{- 2 π i k t}$ , and Parseval's identity reads $∥ s ∥_{2}^{2} = \sum_{k \in Z} ∣ \hat{s} (k) ∣^{2}$ (Fourier coefficients and trigonometric polynomials on the torus, The one-dimensional torus and its normalized Haar integral, The Parseval identity for Fourier series).

[A2]

With sine and cosine having the stated derivatives and the chain rule applying, $\int_{a}^{b} G^{'} = G (b) - G (a)$ for differentiable $G$ with integrable derivative; continuous functions on a closed interval are Riemann integrable, and a bounded Riemann integrable function is Lebesgue measurable with the same integral (The derivatives of sine and cosine are cosine and minus sine, The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , 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)$ , A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral).

[A3]

$\sin (m π) = 0$ and $\cos (m π) = (- 1)^{m}$ for integers $m$ : the zero-set theorem gives the sine values, while $\cos (x + π) = - \cos x$ and $\cos 0 = 1$ give the cosine values by integer induction (The zero sets of sine and cosine and the least positive common period 2 pi, Quarter-turn values and shifts by pi/2 and pi).

[A4]

The averaged character integrals are $\int_{0}^{1 / 2} e^{- 2 π i k t} d t = \frac{1 - (- 1)^{k}}{2 π i k}$ and $\int_{1 / 2}^{1} e^{- 2 π i k t} d t = \frac{(- 1)^{k} - 1}{2 π i k}$ for $k \neq 0$ (Fourier coefficients and trigonometric polynomials on the torus).

[A5]

The coefficient family is square-summable in the finite-subset sense, and its total square sum is the supremum of the symmetric partial sums (Square-summable families on an arbitrary index set and the space $ℓ^{2} (I)$ , The Parseval identity for Fourier series).

[A6]

For every $f \in L^{2} (T; C)$ , the symmetric Fourier partial sums $\sum_{∣ k ∣ \leq N} \hat{f} (k) e_{k}$ converge to $f$ in the $L^{2}$ norm (Fourier series converge in mean square).

Verification

technique · direct

Given: The class $s$ represented by $1$ on $[0, \frac{1}{2})$ and by $- 1$ on $[\frac{1}{2}, 1)$ .

1.1A1A2algebra

The mean vanishes: $\hat{s} (0) = \int_{0}^{1} s (t) d t = \frac{1}{2} - \frac{1}{2} = 0$ .

1.2A2A3algebra

For $k \neq 0$ write $e^{- 2 π i k t} = \cos (2 π k t) - i \sin (2 π k t)$ . The cosine part vanishes: $\int_{0}^{1 / 2} \cos (2 π k t) d t = \frac{\sin (π k)}{2 π k} = 0$ and $\int_{1 / 2}^{1} \cos (2 π k t) d t = \frac{\sin (2 π k) - \sin (π k)}{2 π k} = 0$ , and the signs $\pm 1$ of $s$ multiply these to give $\int_{0}^{1} s (t) \cos (2 π k t) d t = 0$ as well. For the sine part, the antiderivative $- \frac{\cos (2 π k t)}{2 π k}$ gives $\int_{0}^{1} s (t) \sin (2 π k t) d t = \frac{1 - (- 1)^{k}}{2 π k} - \frac{(- 1)^{k} - 1}{2 π k} = \frac{1 - (- 1)^{k}}{π k} .$

2.1step 1.2A4algebra

Therefore $\hat{s} (k) = - i \int_{0}^{1} s (t) \sin (2 π k t) d t = - \frac{i (1 - (- 1)^{k})}{π k} = \frac{1 - (- 1)^{k}}{π i k}$ for every $k \neq 0$ ; the coefficient vanishes exactly for even $k$ and is nonzero for odd $k$ .

3.1step 1.1step 2.1A1A5algebra

Parseval's identity gives $1 = ∥ s ∥_{2}^{2} = \sum_{k \in Z} ∣ \hat{s} (k) ∣^{2}$ , because $∣ s ∣ = 1$ and the domain has measure one; and $∣ \hat{s} (k) ∣^{2} = \frac{(1 - (- 1)^{k})^{2}}{π^{2} k^{2}}$ equals $\frac{4}{π^{2} k^{2}}$ for odd $k$ and $0$ for even $k$ . Hence $1 = \frac{4}{π^{2}} \sum_{k odd} \frac{1}{k^{2}} = \frac{8}{π^{2}} \sum_{k odd, k \geq 1} \frac{1}{k^{2}}$ , and multiplying by $π^{2} / 8$ gives $\sum_{k odd, k \geq 1} k^{- 2} = π^{2} / 8$ .

4.1step 1.1step 2.1step 3.1A6∎

The coefficients of steps 1.1 and 2.1 are the displayed ones, [A6] gives convergence of the symmetric Fourier partial sums to $s$ in mean square, and step 3.1 evaluates the associated square sum as $π^{2} / 8$ ; all statements are about the $L^{2}$ class, and no pointwise or endpoint convergence is asserted.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

131 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

Henri P. Gavin, Dynamic Periodic Response to Periodic Forcing, System Identification course notes, Fall 2013 — §4.1, p.6 (standard reference, not scraped)
Gerald Teschl, Topics in Real and Functional Analysis, version November 17, 2017 — §2.5, pp.64–66 (standard reference, not scraped)