dirichletKernel_eq_ae

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.