Convergence of Fourier series

TheoremDirichlet–Jordan theorem on pointwise convergence of Fourier series#●ready to prove

Let \(f : \mathbb{R} \to \mathbb{C}\) be \(2\pi\)-periodic and of bounded variation on \([-\pi, \pi]\), and for \(n \in \mathbb{Z}\) let \(c_n = \frac{1}{2\pi} \int_0^{2\pi} f(t) e^{-int}\,dt\) be its Fourier coefficients. Then at every \(x \in \mathbb{R}\) the one-sided limits \(f(x^+) = \lim_{y \to x,\, y > x} f(y)\) and \(f(x^-) = \lim_{y \to x,\, y < x} f(y)\) exist, and the symmetric partial sums of the Fourier series converge to their average:

\[\lim_{N \to \infty} \sum_{n=-N}^{N} c_n e^{inx} = \frac{f(x^+) + f(x^-)}{2}.\]

By periodicity, the coefficients \(c_n\) equal the corresponding integrals over \([-\pi, \pi]\).

This is the bounded-variation (Dirichlet–Jordan) form. It is distinct from the version of Dirichlet's theorem that assumes \(f\) continuously differentiable and concludes convergence to \(f(x)\); here \(f\) may be discontinuous and the limit is the average of the one-sided limits.

public theorem_wanted dirichlet_pointwise_convergence
    (f : ℝ → ℂ)
    (hf_periodic : Function.Periodic f (2 * Real.pi))
    (hf_bv : BoundedVariationOn f (Icc (-Real.pi) Real.pi)) :
    ∀ x : ℝ, ∃ lPlus lMinus : ℂ,
      Tendsto f (nhdsWithin x (Ioi x)) (nhds lPlus) ∧
      Tendsto f (nhdsWithin x (Iio x)) (nhds lMinus) ∧
      Tendsto (fun N : ℕ ↦ ∑ n ∈ Finset.Icc (-(N : ℤ)) (N : ℤ),
          fourierCoeffOn Real.two_pi_pos f n * Complex.exp (Complex.I * (n : ℂ) * (x : ℂ)))
        atTop (nhds ((lPlus + lMinus) / 2))

Sources

• Y. Katznelson, An Introduction to Harmonic Analysis, 3rd ed., Ch. I, §5 (functions of bounded variation; Dirichlet–Jordan test).
• https://en.wikipedia.org/wiki/Dirichlet%27s_theorem_on_Fourier_series

DefinitionSymmetric Fourier partial sums#✓fully proved

For \(f \colon \mathbb{R} \to \mathbb{C}\), a natural number \(N\) and \(x \in \mathbb{R}\), the \(N\)-th symmetric Fourier partial sum of \(f\) at \(x\) is \(S_N(f)(x) = \sum_{n=-N}^{N} \hat f_n e^{inx}\), where \(\hat f_n = \frac{1}{2\pi} \int_0^{2\pi} e^{-int} f(t)\,dt\) is the \(n\)-th Fourier coefficient of \(f\) on the interval \([0, 2\pi]\).

noncomputable def fourierPartialSum (f : ℝ → ℂ) (N : ℕ) (x : ℝ) : ℂ :=
  ∑ n ∈ Finset.Icc (-(N : ℤ)) N,
    fourierCoeffOn Real.two_pi_pos f n * Complex.exp (Complex.I * (n : ℂ) * (x : ℂ))

Used by 2

Used byDirichlet's theorem on pointwise convergence of Fourier series · Cesàro means of Fourier series

DefinitionCesàro means of Fourier series#✓fully proved

For \(f \colon \mathbb{R} \to \mathbb{C}\), a natural number \(N\) and \(x \in \mathbb{R}\), the \(N\)-th Cesàro mean of the Fourier series of \(f\) at \(x\) is the average of the first \(N + 1\) symmetric Fourier partial sums, \(\sigma_N(f)(x) = \frac{1}{N+1} \sum_{k=0}^{N} S_k(f)(x)\), where \(S_k(f)(x) = \sum_{n=-k}^{k} \hat f_n e^{inx}\) and \(\hat f_n = \frac{1}{2\pi} \int_0^{2\pi} e^{-int} f(t)\,dt\) is the \(n\)-th Fourier coefficient of \(f\) on the interval \([0, 2\pi]\).

noncomputable def fourierCesaroMean (f : ℝ → ℂ) (N : ℕ) (x : ℝ) : ℂ :=
  (∑ k ∈ Finset.range (N + 1), fourierPartialSum f k x) / (N + 1 : ℂ)

Uses 1 · Used by 1

Statement usesSymmetric Fourier partial sums

Used byFejér's theorem

TheoremDirichlet's theorem on pointwise convergence of Fourier series#●ready to prove

Let \(f \colon \mathbb{R} \to \mathbb{C}\) be \(2\pi\)-periodic and continuously differentiable, and for \(n \in \mathbb{Z}\) let \(\hat f_n = \frac{1}{2\pi} \int_0^{2\pi} e^{-int} f(t)\,dt\) be the \(n\)-th Fourier coefficient of \(f\) on \([0, 2\pi]\). Then for every \(x \in \mathbb{R}\) the symmetric Fourier partial sums \(S_N(f)(x) = \sum_{n=-N}^{N} \hat f_n e^{inx}\) converge to \(f(x)\) as \(N \to \infty\).

public theorem_wanted dirichlet_pointwise
    {f : ℝ → ℂ} (_hperiod : Function.Periodic f (2 * Real.pi)) (_hC1 : ContDiff ℝ 1 f)
    (x : ℝ) :
    Tendsto (fun N : ℕ => fourierPartialSum f N x) atTop (𝓝 (f x))

Sources

• P. G. L. Dirichlet (1829) and L. Fejér (1900). Listed as §46 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem fourier_dirichlet_fejer of the lean-eval benchmark.

Uses 1

Statement usesSymmetric Fourier partial sums

TheoremFejér's theorem#●ready to prove

Let \(f \colon \mathbb{R} \to \mathbb{C}\) be continuous and \(2\pi\)-periodic, and write \(S_k(f)\) for the \(k\)-th symmetric Fourier partial sum of \(f\). Then the Cesàro means \(\sigma_N(f) = (S_0(f) + S_1(f) + \dots + S_N(f)) / (N + 1)\) converge to \(f\) uniformly on \(\mathbb{R}\) as \(N \to \infty\).

public theorem_wanted fejer
    {f : ℝ → ℂ} (_hperiod : Function.Periodic f (2 * Real.pi)) (_hcont : Continuous f) :
    TendstoUniformly (fun N : ℕ => fourierCesaroMean f N) f atTop

Sources

• P. G. L. Dirichlet (1829) and L. Fejér (1900). Listed as §46 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem fourier_dirichlet_fejer of the lean-eval benchmark.

Uses 1

Statement usesCesàro means of Fourier series

2 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.