LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generated

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.

Sine orthogonality on a half period and the full-period integrals of odd $2 L$ -periodic functions

Statement

All integrals in this statement and proof are ordinary Riemann integrals of continuous functions on compact intervals, as in Sine coefficients, sine series and the odd periodic extension.

Let $L > 0$ . Then:

(a) For all integers $n, k \geq 1$ ,

$\int_{0}^{L} \sin (\frac{n π x}{L}) \sin (\frac{k π x}{L}) d x = \frac{L}{2} δ_{n k} .$

(b) Let $W : R \to R$ be continuous (Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point), odd and $2 L$ -periodic. Then

$\int_{0}^{2 L} W (x) d x = 0, \int_{0}^{2 L} W (x) \cos (\frac{k π x}{L}) d x = 0 for every integer k,$

and, for every integer $k \geq 1$ ,

$\frac{1}{2 L} \int_{0}^{2 L} W (x) \sin (\frac{k π x}{L}) d x = \frac{1}{L} \int_{0}^{L} W (x) \sin (\frac{k π x}{L}) d x .$

Facts & Assumptions

Given: The period $L > 0$ ; the integers $n, k$ in (a); the continuous odd $2 L$ -periodic $W$ in (b).

[F1]

Product-to-sum identities and values: $2 \sin a \sin b = \cos (a - b) - \cos (a + b)$ , $\sin (m π) = 0$ and $\cos (m π) = (- 1)^{m}$ for integers $m$ , and $\sin 0 = 0$ , $\cos 0 = 1$ (The addition formulas for sine and cosine, The zero sets of sine and cosine and the least positive common period 2 pi, Parity and the Pythagorean identity for sine and cosine, Sine and cosine defined by their real power series).

[F2]

The sine and cosine integrands in this proof are continuous on each compact interval, hence Riemann integrable (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion). For $m \neq 0$ , $\int_{0}^{L} \cos (m π x / L) d x = (L / (m π)) [\sin (m π) - 0] = 0$ , and for $m = 0$ the integral is $L$ ; the values follow from the fundamental theorem (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)$ , The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ , Integrable functions on $[a, b]$ form a set closed under sums and scalar multiples, and $\int_{a}^{b} (λ f + μ g) = λ \int_{a}^{b} f + μ \int_{a}^{b} g$ ).

[F3]

Additivity and change of variable on a period: for a continuous $2 L$ -periodic $g$ , $\int_{0}^{2 L} g = \int_{0}^{L} g + \int_{L}^{2 L} g$ , and substituting $x = 2 L - u$ in the second integral gives $\int_{L}^{2 L} g (x) d x = \int_{0}^{L} g (2 L - u) d u = \int_{0}^{L} g (- u) d u$ by periodicity (For $a < c < b$ : $f$ is integrable on $[a, b]$ if and only if it is integrable on $[a, c]$ and on $[c, b]$ , and then $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f$ ; with the oriented form for arbitrary $a, b, c$ , The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ , Substitution: if $φ$ is differentiable on $[c, d]$ with $φ^{'}$ integrable and $f$ is continuous on an interval containing $φ ([c, d])$ , then $\int_{φ (c)}^{φ (d)} f = \int_{c}^{d} (f \circ φ) φ^{'}$ , The first fundamental theorem: if $f$ is integrable on $[a, b]$ and continuous at $c$ , then $F^{'} (c) = f (c)$ ; in particular a continuous $f$ has $F$ as a primitive).

Proof

technique · direct; product-to-sum and elementary substitutions on a period

1.1givenF1F2algebra

For $n, k \geq 1$ , [F1] gives $2 \sin (n π x / L) \sin (k π x / L) = \cos ((n - k) π x / L) - \cos ((n + k) π x / L)$ . Integrating over $[0, L]$ and using [F2]: if $n \neq k$ both frequencies are nonzero, so the integral is $0$ ; if $n = k$ the first term contributes $L$ and the second (frequency $2 n \neq 0$ ) contributes $0$ , so the integral is $L / 2$ . This proves (a).

1.2givenF3algebra

Since $W$ is odd and $2 L$ -periodic, [F3] gives $\int_{0}^{2 L} W = \int_{0}^{L} W + \int_{0}^{L} W (- u) d u = \int_{0}^{L} W - \int_{0}^{L} W = 0$ .

1.3givenF1F3algebra

Likewise, $\int_{0}^{2 L} W (x) \cos (k π x / L) d x = \int_{0}^{L} W (x) \cos (k π x / L) d x + \int_{0}^{L} W (- u) \cos (k π (2 L - u) / L) d u$ . Now $W (- u) = - W (u)$ and $\cos (k π (2 L - u) / L) = \cos (2 k π - k π u / L) = \cos (k π u / L)$ ; the two integrals are equal and opposite, so the total is $0$ .

2.1givenF1F3algebra∎

For the sine integral, split at $L$ : $\int_{0}^{2 L} W (x) \sin (k π x / L) d x = \int_{0}^{L} (\dots) d x + \int_{0}^{L} W (- u) \sin (k π (2 L - u) / L) d u$ . Here $\sin (k π (2 L - u) / L) = \sin (2 k π - k π u / L) = - \sin (k π u / L)$ , and $W (- u) = - W (u)$ ; the second integral equals $\int_{0}^{L} W (u) \sin (k π u / L) d u$ . Hence the full-period integral is twice the half-period integral, which is the displayed identity.

Remarks

The sine functions $\sin (n π x / L)$ , $n \geq 1$ , are the eigenfunctions of the fixed-end problem in the elementary sense of satisfying the two endpoint conditions and the second-derivative eigenequation; part (a) records only their mutual orthogonality, not completeness, which is proved separately with Fejer means.
The identities of part (b) are the reason an odd $2 L$ -periodic function has no cosine component in its complex Fourier expansion; the statement is computational and uses no expansion theory.

Sine orthogonality on a half period and the full-period integrals of odd $2 L$ -periodic functions

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

Sine orthogonality on a half period and the full-period integrals of odd 2L2L-periodic functions

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

Sine orthogonality on a half period and the full-period integrals of odd $2 L$ -periodic functions