Fourier series

Fourier series on the circle and torus: Fejér and Dirichlet kernels, pointwise and Cesàro convergence, Riemann–Lebesgue, uniqueness, absolutely convergent series and Wiener's theorems, periodic convolution, Fourier optimization on the torus.

• Brezis–Gallouët inequality on the two-dimensional torus
• Convergence of Fourier series
• Convolutions and translates on the circle
• Fejér kernel and Fejér's theorem
• Fourier coefficients of measures on the circle
• Riemann–Lebesgue lemma
• Absolutely convergent Fourier series
• Uniqueness of Fourier coefficients

DefinitionFourier coefficients of the Mathieu–Fibonacci periodic function#✓fully proved

Let \(\varphi = (1 + \sqrt{5}) / 2\) be the golden ratio. For each natural number \(n \ge 1\), the \(n\)-th coefficient is the real number \(c_n = (2 / \log \varphi) \, |\Gamma(1 + 2 n \pi i / \log \varphi)|^2\), where \(\Gamma\) is the complex Gamma function.

In the source, these are the coefficients of the cosine series \(H(x) = 1 + \sum_{n \ge 1} c_n \cos(4 n \pi x / \log \varphi)\) of a periodic function \(H\).

public noncomputable def mathieuFibonacciFourierCoefficient (n : {n : ℕ // 1 ≤ n}) : ℝ :=
  (2 / Real.log ((1 + Real.sqrt 5) / 2)) *
    ‖Complex.Gamma (1 + 2 * (n.val : ℂ) * (Real.pi : ℂ) * Complex.I /
      (Real.log ((1 + Real.sqrt 5) / 2) : ℂ))‖ ^ 2

TheoremPeriodic convolution#✓fully proved

Let \(A\) be a normed ring that is a normed algebra over \(\mathbb{R}\) (for example \(\mathbb{R}\) or \(\mathbb{C}\)), let \(T\) be a real number, and let \(f, g : \mathbb{R} \to A\) with \(g\) periodic of period \(T\), that is, \(g(x + T) = g(x)\) for all real \(x\). Then the function \(x \mapsto \int_0^T f(t)\, g(x - t)\, dt\) is periodic of period \(T\). The function \(f\) need not be periodic or integrable.

theorem periodic_convolution {A : Type*} [NormedRing A] [NormedAlgebra ℝ A]
    {T : ℝ} {f g : ℝ → A} (hg : Function.Periodic g T) :
    Function.Periodic (fun x ↦ ∫ t in (0 : ℝ)..T, f t * g (x - t)) T

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.