carleson

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

Second part of Lemma 11.1.8 (Dirichlet kernel) from the paper. -/ lemma dirichletKernel_eq {x : ℝ} (h : cexp (I * x) ≠ 1) : dirichletKernel N x = dirichletKernel' N x := by have : (cexp (1 / 2 * I * x) - cexp (-1 / 2 * I * x)) * dirichletKernel N x = cexp ((N + 1 / 2) * I * x) - cexp (-(N + 1 / 2) * I * x) := by calc (cexp (1 / 2 * I * x) - cexp (-1 / 2 * I * x)) * dirichletKernel N x _ = ∑ n ∈ Icc (-(N : ℤ)) N, (cexp ((n + 1 / 2) * I * ↑x) - cexp ((n - 1 / 2) * I * ↑x)) := by rw [dirichletKernel, mul_sum] congr 1 with n simp [sub_mul, ← exp_add, ← exp_add] congr 2 <;> · ring_nf congr 1 rw [mul_assoc, mul_assoc] congr rw_mod_cast [← mul_assoc, mul_comm, ← mul_assoc, inv_mul_cancel₀, one_mul] exact Real.pi_pos.ne.symm _ = ∑ n ∈ Icc (-(N : ℤ)) N, cexp ((n + 1 / 2) * I * ↑x) - ∑ n ∈ Icc (-(N : ℤ)) N, cexp ((n - 1 / 2) * I * ↑x) := by rw [sum_sub_distrib] _ = cexp ((N + 1 / 2) * I * x) - cexp (-(N + 1 / 2) * I * x) := by rw [← sum_Ico_add_eq_sum_Icc, ← sum_Ioc_add_eq_sum_Icc, add_sub_add_comm, ← zero_add (cexp ((N + 1 / 2) * I * ↑x) - cexp (-(N + 1 / 2) * I * ↑x))] · congr 2 · rw [sub_eq_zero] conv => lhs; rw [← Int.add_sub_cancel (-(N : ℤ)) 1, sub_eq_add_neg, ← Int.add_sub_cancel (Nat.cast N) 1, sub_eq_add_neg, ← sum_Ico_add'] congr 2 with n · rw [mem_Ico, mem_Ioc, Int.lt_iff_add_one_le, add_le_add_iff_right, ← mem_Icc, Int.lt_iff_add_one_le, ← mem_Icc] simp · simp only [Int.reduceNeg, Int.cast_add, Int.cast_neg, Int.cast_one, one_div, add_assoc, sub_eq_add_neg] norm_num · rw [neg_add_rev, add_comm, Int.cast_neg, sub_eq_add_neg] norm_cast all_goals simp have h' : (cexp (1 / 2 * I * x) - cexp (-1 / 2 * I * x)) ≠ 0 := by contrapose! h rw [sub_eq_zero] at h calc cexp (I * ↑x) _ = cexp (1 / 2 * I * ↑x) * cexp (1 / 2 * I * ↑x) := by rw [← exp_add, mul_assoc, ← mul_add] ring_nf _ = cexp (1 / 2 * I * ↑x) * cexp (-1 / 2 * I * ↑x) := by congr 2 _ = 1 := by rw [← exp_add] ring_nf exact exp_zero rw [dirichletKernel'] apply mul_left_cancel₀ h' rw [this, mul_add, sub_eq_add_neg] congr · rw [mul_div] apply eq_div_of_mul_eq · contrapose! h rwa [sub_eq_zero, neg_mul, exp_neg, eq_comm, inv_eq_one] at h ring_nf rw [← exp_add, ← exp_add, ← exp_add] congr 2 <;> ring · rw [mul_div] apply eq_div_of_mul_eq (sub_ne_zero_of_ne h.symm) ring_nf rw [← exp_add, ← exp_add, ← exp_add, neg_add_eq_sub] congr 2 <;> ring

lemma dirichletKernel'_eq_zero {x : ℝ} (h : cexp (I * x) = 1) : dirichletKernel' N x = 0 := by simp [dirichletKernel', exp_neg, h]

/- "a.e." version of previous lemma.

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

Lemma 11.3.1.

Lemma 11.3.3.

Lemma 11.3.4.

Lemma 11.3.5, part 3.

The convolution with dirichletApprox is controlled on (0, 2π] in L^2 norm. This follows from the fact that it coincides (up to a constant) with approxHilbertTransform, which is essentially an average of Fourier projections (which are all contractions in L^2).