Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-21
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.

Riemann–Lebesgue lemma for continuous functions on a compact interval

Statement

Let a<b and let f:[a,b]→R be continuous. For positive integer n, put

In:=∫abf(t)sin⁡(nt) dt,Jn:=∫abf(t)cos⁡(nt) dt.

Then

lim⁡n→∞In=0,lim⁡n→∞Jn=0.

In particular, for every continuous g:[0,π]→R, lim⁡n→∞∫0πg(x)sin⁡(nx) dx=0.

Facts & Assumptions

Given: Reals a<b, a continuous f:[a,b]→R, and a real ε>0.

[L1]

For a≤b, every continuous real function on [a,b] is a uniform limit of polynomials (Polynomials are uniformly dense in C([a,b],R) for every closed interval).

[L2]

If integrable functions u,v satisfy ∣u(x)−v(x)∣≤η between endpoints, then ∣∫u−∫v∣≤η times the endpoint distance (Uniformly close integrable functions have integrals differing by at most the interval length times their uniform error).

[L3]

If u,v are differentiable on [a,b] with integrable derivatives, then ∫abuv′=u(b)v(b)−u(a)v(a)−∫abu′v (If u,v are differentiable on [a,b] with u′,v′ integrable, then ∫abuv′=u(b)v(b)−u(a)v(a)−∫abu′v).

[L4]

The derivative formulas for sine and cosine, together with the chain rule, give (sin⁡nt)′=ncos⁡nt and (cos⁡nt)′=−nsin⁡nt for positive integers n (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∘g is differentiable at c with (f∘g)′(c)=f′(g(c)) g′(c)).

[L8]

For every real η>0 there is a positive integer N with 1/N<η (For every ε>0 in a complete ordered field there is a natural n≥1 with 1/n<ε).

[L9]

For every real x, ∣sin⁡x∣≤1 and ∣cos⁡x∣≤1 (Parity and the Pythagorean identity for sine and cosine).

[L10]

The number π=2γ is positive because the smallest positive zero of cosine satisfies γ∈(0,2) (Pi as twice the smallest positive zero of cosine, Cosine has a smallest positive zero, lying strictly between zero and two).

[L12]

A real sequence converges to zero when, for every positive rational ε, its terms are eventually smaller than ε in absolute value (Limits and Cauchy sequences of reals).

Proof

technique · direct
1.1givenL1choose

By [L1], choose a polynomial p with ∣f(t)−p(t)∣<ε/(4(b−a)) for every t∈[a,b].

1.2L3L4L5L6L7L9L11algebra

Put Cp:=∣p(a)∣+∣p(b)∣+∫ab∣p′(t)∣ dt. Using v(t)=−cos⁡(nt)/n in [L3], and then [L6], [L7], [L9], and [L11], gives ∣∫abp(t)sin⁡(nt) dt∣≤Cp/n. Using v(t)=sin⁡(nt)/n gives the identical bound for the cosine integral.

1.3L8choosealgebra

Apply [L8] to ε/(2(Cp+1)) and choose a positive integer N with (Cp+1)/N<ε/2. Then Cp/n<ε/2 whenever n≥N.

2.1step 1.1L2L5L6L9algebra

The functions f(t)sin⁡(nt) and p(t)sin⁡(nt) are integrable, and [L2] with [L6] and [L9] gives ∣∫ab(f(t)−p(t))sin⁡(nt) dt∣≤ε/4<ε/2 for every positive integer n; the same estimate holds with cosine.

3.1step 2.1step 1.2step 1.3L7algebra

For every n≥N, linearity [L7] splits each integral into its (f−p) part and its p part. Steps 2.1, 1.2, and 1.3 make the absolute value of each integral less than ε, for sine and for cosine.

4.1step 3.1L10L12∎

Since ε>0 was arbitrary, step 3.1 is exactly convergence of both sequences of integrals to zero by [L12]; [L10] permits the substitution a=0, b=π, and g for f in the stated special case.

Depends on

Used by

Dependency tree · two levels

78 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