LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

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.

L2 normalisation of the sine modes on an interval

Statement

Assume Countable Choice. For all integers $k, l \geq 1$ , $\int_{0}^{π} \sin (k x) \sin (l x) d x = \frac{π}{2} δ_{k l} .$ In particular $∥ \sin (k \cdot) ∥_{L^{2} (0, π)} = \sqrt{π / 2}$ .

Facts & Assumptions

Given: Countable Choice and integers $k, l \geq 1$ , and the trigonometric functions of the power-series definition.

[A1]

Countable Choice is the ambient hypothesis inherited through the L² inner-product dictionary [F5] (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

Angle addition: $\sin (x + y) = \sin x \cos y + \cos x \sin y$ and $\cos (x + y) = \cos x \cos y - \sin x \sin y$ (The addition formulas for sine and cosine).

[F2]

$\sin^{'} = \cos$ and $\cos^{'} = - \sin$ , with $\sin 0 = 0$ (The derivatives of sine and cosine are cosine and minus sine).

[F3]

$\sin x = 0$ exactly for $x = m π$ , $m \in Z$ (The zero sets of sine and cosine and the least positive common period 2 pi).

[F4]

On an order-convex $I$ with at least two elements, a continuous function has primitives, and for $a < b$ in $I$ and any primitive $G$ one has $\int_{a}^{b} f = G (b) - G (a)$ (Every continuous function on an interval has a primitive; two primitives differ by a constant; and $\int_{a}^{b} f = G (b) - G (a)$ for any primitive $G$ ).

[F5]

$L^{2} (0, π)$ is the quotient space of The space $L^{p} (μ)$ as the quotient by null functions, and under its Countable Choice hypothesis the integral pairing of $L^{2}$ with the integral pairing is a Hilbert space satisfies $⟨ f, f ⟩ = ∥ f ∥_{L^{2} (0, π)}^{2} = \int_{0}^{π} ∣ f ∣^{2}$ ; Countable Choice is inherited from that supplier (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F6]

Chain rule: $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ at a differentiability point (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)$ ).

Proof

Given: Countable Choice and integers $k, l \geq 1$ .

1.1F1given

Combining the two addition formulas [F1] gives the product-to-sum identity $2 \sin (k x) \sin (l x) = \cos ((k - l) x) - \cos ((k + l) x)$ for all real $x$ ; when $k = l$ it reads $2 \sin^{2} (k x) = 1 - \cos (2 k x)$ , which is the same identity with $\cos (0) = 1$ .

2.1step 1.1F2F3F4F6given

For every nonzero integer $m$ the function $x \mapsto \sin (m x) / m$ is a primitive of $x \mapsto \cos (m x)$ on $[0, π]$ by [F2] and [F6], so the evaluation clause of [F4] ([F3] for the vanishing of sine at the endpoints) gives $\int_{0}^{π} \cos (m x) d x = \frac{\sin (m π) - \sin 0}{m} = 0$ ; also $\int_{0}^{π} 1 d x = π$ .

3.1step 1.1step 2.1given

If $k \neq l$ then both $k - l$ and $k + l$ are nonzero integers, so step 2.1 and step 1.1 give $\int_{0}^{π} \sin (k x) \sin (l x) d x = \frac{1}{2} (0 - 0) = 0$ ; if $k = l$ then $k - l = 0$ and $k + l = 2 k \neq 0$ , so $\int_{0}^{π} \sin (k x)^{2} d x = \frac{1}{2} (π - 0) = \frac{π}{2}$ . Hence the displayed identity holds for all integers $k, l \geq 1$ .

4.1step 3.1A1F5given∎

Taking $k = l$ and using the inner-product dictionary [F5] gives $∥ \sin (k \cdot) ∥_{L^{2} (0, π)}^{2} = \int_{0}^{π} \sin (k x)^{2} d x = \frac{π}{2}$ and hence $∥ \sin (k \cdot) ∥_{L^{2} (0, π)} = \sqrt{π / 2}$ . The integral computation of steps 1.1–3.1 is choice-free; the only use of Countable Choice is the inheritance through [F5] in this last step, needed to read the quotient norm as the integral pairing.

Depends on

Used by

Backward heat amplifies small high-frequency errors Counterexample
Sine modes decay under Dirichlet heat flow Example
Backward ill-posedness does not mean universal nonexistence Remark
The backward heat solution map is unbounded Theorem

Dependency tree · two levels

60 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, Partial Differential Equations: From Classical to Modern (2025 archived author manuscript, AMS Graduate Studies in Mathematics) (standard reference, not scraped)