Riemann–Lebesgue lemma

TheoremA Fourier coefficient is bounded by the L¹ norm#✓fully proved

Let \(T > 0\), let \(\mu\) be the Haar probability measure on the circle \(\mathbb{R}/T\mathbb{Z}\), and let \(E\) be a normed space over \(\mathbb{C}\). For every function \(f : \mathbb{R}/T\mathbb{Z} \to E\) and every \(n \in \mathbb{Z}\), the \(n\)-th Fourier coefficient \(\hat f(n) = \int e^{-2\pi i n t / T} f(t)\,d\mu(t)\) satisfies \(\|\hat f(n)\| \le \int \|f(t)\|\,d\mu(t)\).

The bound holds because \(|e^{-2\pi i n t / T}| = 1\). No integrability is assumed: as usual for the Bochner integral, an integral whose integrand is not integrable is \(0\), and so is any \(E\)-valued integral when \(E\) is not complete.

theorem norm_fourierCoeff_le_integral_norm {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℂ E] {f : AddCircle T → E} (n : ℤ) :
    ‖fourierCoeff f n‖ ≤
      ∫ t, ‖f t‖ ∂(AddCircle.haarAddCircle (T := T))

Used by 1

Used byRiemann–Lebesgue lemma on the circle

TheoremRiemann–Lebesgue for continuous functions#✓fully proved

Let \(T > 0\) and let \(\mu\) be the Haar probability measure on the circle \(\mathbb{R}/T\mathbb{Z}\). For every continuous function \(g : \mathbb{R}/T\mathbb{Z} \to \mathbb{C}\), the Fourier coefficients \(\hat g(n) = \int e^{-2\pi i n t / T} g(t)\,d\mu(t)\) tend to \(0\) as \(|n| \to \infty\), that is, along the cofinite filter on \(\mathbb{Z}\).

The proof uses Parseval's identity in \(L^2(\mu)\): the sequence \(|\hat g(n)|^2\) is summable, so it tends to \(0\).

theorem tendsto_fourierCoeff_cofinite_of_continuous {g : C(AddCircle T, ℂ)} :
    Tendsto (fun n : ℤ => fourierCoeff g n) cofinite (𝓝 0)

Used by 1

Used byRiemann–Lebesgue lemma on the circle

TheoremRiemann–Lebesgue lemma on the circle#✓fully proved

Let \(T > 0\) and let \(\mu\) be the Haar probability measure on the circle \(\mathbb{R}/T\mathbb{Z}\). For every \(\mu\)-integrable function \(f : \mathbb{R}/T\mathbb{Z} \to \mathbb{C}\), the Fourier coefficients \(\hat f(n) = \int e^{-2\pi i n t / T} f(t)\,d\mu(t)\) tend to \(0\) as \(|n| \to \infty\), that is, along the cofinite filter on \(\mathbb{Z}\).

theorem tendsto_fourierCoeff_cofinite {f : AddCircle T → ℂ}
    (hf : Integrable f (AddCircle.haarAddCircle (T := T))) :
    Tendsto (fun n : ℤ => fourierCoeff f n) cofinite (𝓝 0)

Uses 2 · Used by 1

Proof usesA Fourier coefficient is bounded by the L¹ norm · Riemann–Lebesgue for continuous functions

Used byRiemann–Lebesgue lemma on an interval

TheoremRiemann–Lebesgue lemma on an interval#✓fully proved

Let \(a < b\) be real numbers and let \(f : \mathbb{R} \to \mathbb{C}\) be integrable on \([a, b]\). Then the Fourier coefficients of \(f\) on \([a, b]\),

\[\hat f(n) = \frac{1}{b - a} \int_a^b e^{-2\pi i n x / (b - a)} f(x)\,dx,\]

tend to \(0\) as \(|n| \to \infty\), that is, along the cofinite filter on \(\mathbb{Z}\).

theorem tendsto_fourierCoeffOn_cofinite {a b : ℝ} (hab : a < b)
    {f : ℝ → ℂ} (hf : IntervalIntegrable f volume a b) :
    Tendsto (fun n : ℤ => fourierCoeffOn hab f n) cofinite (𝓝 0)

Uses 1 · Used by 1

Proof usesRiemann–Lebesgue lemma on the circle

Used byDecay rate:

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.