norm_dirichletKernel_le

lemma norm_dirichletKernel_le {x : ℝ} : ‖dirichletKernel N x‖ ≤ 2 * N + 1 := by  rw [dirichletKernel]  calc ‖∑ n ∈ Icc (-(N : ℤ)) N, (fourier n) ↑x‖    _ ≤ ∑ n ∈ Icc (-(N : ℤ)) N, ‖(fourier n) ↑x‖ := norm_sum_le _ _    _ ≤ ∑ n ∈ Icc (-(N : ℤ)) N, 1 := by      apply sum_le_sum      exact fun n _ ↦ le_trans (ContinuousMap.norm_coe_le_norm (fourier n) x) (fourier_norm n).le    _ = 2 * N + 1 := by      rw_mod_cast [sum_const, Int.card_Icc, sub_neg_eq_add, nsmul_eq_mul, mul_one,        Int.toNat_natCast]      ring