Documentation

Carleson.Classical.DirichletKernel

def dirichletKernel (N : ℕ) :

Equations

dirichletKernel N x = ∑ n ∈ Finset.Icc (-Int.ofNat N) ↑N, (fourier n) ↑x

Instances For

def dirichletKernel' (N : ℕ) :

Equations

dirichletKernel' N x = Complex.exp (Complex.I * ↑N * ↑x) / (1 - Complex.exp (-Complex.I * ↑x)) + Complex.exp (-Complex.I * ↑N * ↑x) / (1 - Complex.exp (Complex.I * ↑x))

Instances For

theorem dirichletKernel_periodic {N : ℕ} :

Function.Periodic (dirichletKernel N) (2 * Real.pi)

theorem dirichletKernel'_periodic {N : ℕ} :

Function.Periodic (dirichletKernel' N) (2 * Real.pi)

theorem dirichletKernel'_measurable {N : ℕ} :

Measurable (dirichletKernel' N)

theorem dirichletKernel_eq {N : ℕ} {x : ℝ} (h : Complex.exp (Complex.I * ↑x) ≠ 1) :

dirichletKernel N x = dirichletKernel' N x

theorem dirichletKernel'_eq_zero {N : ℕ} {x : ℝ} (h : Complex.exp (Complex.I * ↑x) = 1) :

dirichletKernel' N x = 0

theorem dirichletKernel_eq_ae {N : ℕ} :

∀ᵐ (x : ℝ), dirichletKernel N x = dirichletKernel' N x

theorem norm_dirichletKernel_le {N : ℕ} {x : ℝ} :

‖dirichletKernel N x‖ ≤ 2 * ↑N + 1

theorem norm_dirichletKernel'_le {N : ℕ} {x : ℝ} :

‖dirichletKernel' N x‖ ≤ 2 * ↑N + 1

theorem partialFourierSum_eq_conv_dirichletKernel {f : ℝ → ℂ} {N : ℕ} {x : ℝ} (h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)) :

partialFourierSum N f x = 1 / (2 * ↑Real.pi) * ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * dirichletKernel N (x - y)

theorem partialFourierSum_eq_conv_dirichletKernel' {f : ℝ → ℂ} {N : ℕ} {x : ℝ} (h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)) :

partialFourierSum N f x = 1 / (2 * ↑Real.pi) * ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * dirichletKernel' N (x - y)