noncomputable def Integration.fourierCoefficientCos (f : ℝ → ℝ) (n : ℕ) : ℝ

The n-th cosine Fourier coefficient of a function f : ℝ → ℝ, defined as (1/π) ∫_{-π}^{π} f(x) · cos(n·x) dx. This corresponds to the coefficient bₙ in the Fourier series expansion of f.

theorem Integration.riemann_lebesgue (f : ℝ → ℝ) (hf : ContDiffOn ℝ 1 f (Set.Icc (-Real.pi) Real.pi)) : Filter.Tendsto (fun (n : ℕ) => 1 / Real.pi * ∫ (x : ℝ) in -Real.pi..Real.pi, f x * Real.sin (↑n * x)) Filter.atTop (nhds 0) ∧ Filter.Tendsto (fun (n : ℕ) => 1 / Real.pi * ∫ (x : ℝ) in -Real.pi..Real.pi, f x * Real.cos (↑n * x)) Filter.atTop (nhds 0)

Riemann–Lebesgue lemma (for continuously differentiable functions on [-π, π]).

If f : ℝ → ℝ is continuously differentiable on [-π, π], then both Fourier-coefficient integrals tend to zero as n → ∞:

• (1/π) ∫_{-π}^{π} f(x) · sin(n·x) dx → 0, and
• (1/π) ∫_{-π}^{π} f(x) · cos(n·x) dx → 0.

The proof uses integration by parts to express each integral in terms of a bounded antiderivative of sin(n·x) (resp. cos(n·x)) of size O(1/n), then squeezes to zero.