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 sawtooth and the Basel sum

Example

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $f$ be the class in $L^{2} (T; C)$ represented on the fundamental domain $[0, 1)$ by $f (t) = t$ for $0 \leq t < \frac{1}{2}$ and $f (t) = t - 1$ for $\frac{1}{2} \leq t < 1$ ; this is the $1$ -periodic extension of $x \mapsto x$ on $(- \frac{1}{2}, \frac{1}{2})$ , and the values at the endpoints may be chosen arbitrarily, as they do not change the class. Then

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

the Fourier series of $f$ converges to $f$ in mean square (Fourier series converge in mean square), and Parseval's identity gives the Basel sum $\sum_{k = 1}^{\infty} k^{- 2} = π^{2} / 6$ . Only $L^{2}$ convergence is asserted; no pointwise claim is made at the discontinuity.

Facts & Assumptions

[A1]

$\hat{f} (k) = \int_{T} f e_{- k} d m_{T}$ and the torus integral is represented on $[0, 1)$ , so $\hat{f} (k) = \int_{0}^{1} f (t) e^{- 2 π i k t} d t$ for the representative above; Parseval's identity holds in the form $∥ f ∥_{2}^{2} = \sum_{k \in Z} ∣ \hat{f} (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]

For real $u, v$ differentiable with integrable derivatives, $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$ ; and $\int_{a}^{b} G^{'} = G (b) - G (a)$ for differentiable $G$ with integrable derivative (If $u, v$ are differentiable on $[a, b]$ with $u^{'}, v^{'}$ integrable, then $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$ , 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)$ ).

[A3]

The derivatives of sine and cosine are cosine and minus sine, the chain rule gives the derivatives of $t \mapsto \sin (c t)$ and $t \mapsto \cos (c t)$ , and power functions have the expected derivatives; continuous functions on a closed interval are Riemann integrable, and a bounded Riemann integrable function on $[a, b]$ 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)$ , 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, 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).

[A4]

$\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).

[A5]

The characters satisfy $\int_{T} e_{m} d m_{T} = 1$ for $m = 0$ and $0$ otherwise; the coefficient family is square-summable and its total square sum is the supremum of the symmetric partial sums (Fourier coefficients and trigonometric polynomials on the torus, Square-summable families on an arbitrary index set and the space $ℓ^{2} (I)$ ).

Verification

technique · direct

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

1.1A1A3algebra

The zeroth coefficient vanishes: $\hat{f} (0) = \int_{0}^{1} f (t) d t = \int_{0}^{1 / 2} t d t + \int_{1 / 2}^{1} (t - 1) d t = \frac{1}{8} + [\frac{t^{2}}{2} - t]_{1 / 2}^{1} = \frac{1}{8} - \frac{1}{2} + \frac{3}{8} = 0$ .

1.2A2A3A4algebra

For $k \neq 0$ , write $e^{- 2 π i k t} = \cos (2 π k t) - i \sin (2 π k t)$ and integrate by parts on the two halves. Integrating $t \cos (2 π k t)$ and $(t - 1) \cos (2 π k t)$ with antiderivatives $\frac{\sin (2 π k t)}{2 π k}$ and $\frac{\cos (2 π k t)}{4 π^{2} k^{2}}$ gives $\int_{0}^{1 / 2} t \cos (2 π k t) d t = \frac{\sin (π k)}{4 π k} + \frac{\cos (π k) - 1}{4 π^{2} k^{2}}, \int_{1 / 2}^{1} (t - 1) \cos (2 π k t) d t = \frac{\sin (π k)}{4 π k} + \frac{1 - \cos (π k)}{4 π^{2} k^{2}},$ so $\int_{0}^{1} f (t) \cos (2 π k t) d t = \frac{\sin (π k)}{2 π k} = 0$ ; and integrating $t \sin (2 π k t)$ and $(t - 1) \sin (2 π k t)$ with antiderivatives $- \frac{t \cos (2 π k t)}{2 π k} + \frac{\sin (2 π k t)}{4 π^{2} k^{2}}$ and $- \frac{(t - 1) \cos (2 π k t)}{2 π k} + \frac{\sin (2 π k t)}{4 π^{2} k^{2}}$ gives $\int_{0}^{1 / 2} t \sin (2 π k t) d t = - \frac{\cos (π k)}{4 π k} + \frac{\sin (π k)}{4 π^{2} k^{2}}, \int_{1 / 2}^{1} (t - 1) \sin (2 π k t) d t = - \frac{\cos (π k)}{4 π k},$ so $\int_{0}^{1} f (t) \sin (2 π k t) d t = - \frac{\cos (π k)}{2 π k} = - \frac{(- 1)^{k}}{2 π k}$ .

2.1step 1.2A4algebra

Adding the real and imaginary contributions, $\hat{f} (k) = - i \int_{0}^{1} f (t) \sin (2 π k t) d t = \frac{i (- 1)^{k}}{2 π k} = \frac{(- 1)^{k + 1}}{2 π i k}$ for every $k \neq 0$ .

3.1step 1.1step 2.1A1A5algebra

Parseval's identity gives $\frac{1}{12} = ∥ f ∥_{2}^{2} = \sum_{k \neq 0} \frac{1}{4 π^{2} k^{2}} = \frac{1}{2 π^{2}} \sum_{k \geq 1} \frac{1}{k^{2}}$ , where $∥ f ∥_{2}^{2} = \int_{0}^{1} f (t)^{2} d t = 2 \int_{0}^{1 / 2} t^{2} d t = \frac{1}{12}$ ; multiplying by $2 π^{2}$ gives $\sum_{k \geq 1} k^{- 2} = π^{2} / 6$ .

4.1step 1.1step 2.1step 3.1A5∎

The coefficients of steps 1.1 and 2.1 are the displayed ones, the Fourier series converges to $f$ in mean square, and the Parseval computation of step 3.1 yields the Basel sum; the endpoint values of the representative are irrelevant, and the claim is an $L^{2}$ statement only.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

138 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.2, p.7 (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)