partialFourierSum_eq_conv_dirichletKernel'

lemma partialFourierSum_eq_conv_dirichletKernel' {f : ℝ → ℂ} {x : ℝ}    (h : IntervalIntegrable f volume 0 (2 * π)) :    partialFourierSum N f x =      (1 / (2 * π)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * π), f y * dirichletKernel' N (x - y) := by  rw [partialFourierSum_eq_conv_dirichletKernel h]  calc _    _ = (1 / (2 * π)) * ∫ (y : ℝ) in (x - 2 * π)..(x - 0), f (x - y) * dirichletKernel N y := by      congr 1      rw [← intervalIntegral.integral_comp_sub_left]      simp    _ = (1 / (2 * π)) * ∫ (y : ℝ) in (x - 2 * π)..(x - 0), f (x - y) * dirichletKernel' N y := by      congr 1      apply intervalIntegral.integral_congr_ae (ae_imp_of_ae_restrict        (ae_restrict_of_ae _))      have : {a | ¬f (x - a) * dirichletKernel N a = f (x - a) * dirichletKernel' N a} ⊆ {a | ¬dirichletKernel N a = dirichletKernel' N a} := by        simp_all      apply measure_mono_null this dirichletKernel_eq_ae    _ = (1 / (2 * π)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * π), f y * dirichletKernel' N (x - y) := by      congr 1      rw [← intervalIntegral.integral_comp_sub_left]      simp