noncomputable def dirichletKernel (N : ℕ) : ℝ → ℂ

Equations

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

noncomputable 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))

theorem continuous_dirichletKernel {N : ℕ} : Continuous (dirichletKernel N)

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

Second part of Lemma 11.1.8 (Dirichlet kernel) from the paper.

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 instFactLtRealOfNatHMulPi_carleson_1 : Fact (0 < 2 * Real.pi)

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 {N : ℕ} {f : ℝ → ℂ} {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)

First part of lemma 11.1.8 (Dirichlet kernel) from the blueprint.

theorem partialFourierSum_eq_conv_dirichletKernel' {N : ℕ} {f : ℝ → ℂ} {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)