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  calc partialFourierSum N f x    _ = ∑ n ∈ Icc (-(N : ℤ)) N, fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x := by      rw [partialFourierSum]    _ = ∑ n ∈ Icc (-(N : ℤ)) N, (1 / (2 * π - 0)) • ((∫ (y : ℝ) in (0 : ℝ)..2 * π, (fourier (-n) ↑y • f y)) * (fourier n) ↑x) := by      congr 1 with n      rw [fourierCoeffOn_eq_integral, smul_mul_assoc]    _ = (1 / (2 * π)) * ∑ n ∈ Icc (-(N : ℤ)) N, ((∫ (y : ℝ) in (0 : ℝ)..2 * π, (fourier (-n) ↑y • f y)) * (fourier n) ↑x) := by      rw [show ∑ n ∈ Icc (-(N : ℤ)) ↑N, (1 / (2 * π - 0) : ℝ) • ((∫ (y : ℝ) in (0 : ℝ)..2 * π, (fourier (-n)) ↑y • f y) * (fourier n) ↑x) = (1 / (2 * π - 0) : ℝ) • ∑ n ∈ Icc (-(N : ℤ)) ↑N, ((∫ (y : ℝ) in (0 : ℝ)..2 * π, (fourier (-n)) ↑y • f y) * (fourier n) ↑x) from (Finset.smul_sum ..).symm]      rw_mod_cast [real_smul, sub_zero]    _ = (1 / (2 * π)) * ∑ n ∈ Icc (-(N : ℤ)) N, ((∫ (y : ℝ) in (0 : ℝ)..2 * π, (fourier (-n) ↑y • f y) * (fourier n) ↑x)) := by      congr with n      exact (intervalIntegral.integral_mul_const _ _).symm    _ = (1 / (2 * π)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * π), ∑ n ∈ Icc (-(N : ℤ)) N, (fourier (-n)) y • f y * (fourier n) x := by      rw [← intervalIntegral.integral_finsetSum]      exact fun _ _ ↦ IntervalIntegrable.mul_const        (h.continuousOn_mul fourier_uniformContinuous.continuous.continuousOn) _    _ = (1 / (2 * π)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * π), f y * ∑ n ∈ Icc (-(N : ℤ)) N, (fourier (-n)) y * (fourier n) x := by      congr with y      rw [mul_sum]      congr with n      rw [smul_eq_mul]      ring    _ = (1 / (2 * π)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * π), f y * dirichletKernel N (x - y) := by      congr with y      rw [dirichletKernel]      congr with n      rw [fourier_coe_apply, fourier_coe_apply, fourier_coe_apply, ←exp_add]      congr      simp      field