fejer_sum_eq_integral

theorem fejer_sum_eq_integral {f : ℝ → ℝ} (hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) Real.pi)    (h_per : Function.Periodic f (2 * Real.pi)) (n : ℕ) (x : ℝ) :    fejer_sum f n x = (1 / Real.pi) * ∫ t in (-Real.pi)..Real.pi, f t * fejer_kernel n (x - t) := by      -- By Fubini's theorem, we can interchange the order of summation and integration.      have h_fubini : ∫ t in (-Real.pi)..Real.pi, f t * (∑ j ∈ Finset.range (n + 1), dirichlet_kernel j (x - t)) = ∑ j ∈ Finset.range (n + 1), ∫ t in (-Real.pi)..Real.pi, f t * dirichlet_kernel j (x - t) := by        simp +decide only [Finset.mul_sum _ _ _];        rw [ intervalIntegral.integral_finset_sum ];        intro i hi;        apply_rules [ IntervalIntegrable.mul_continuousOn ];        refine' Continuous.continuousOn _;        exact Continuous.add continuous_const <| continuous_finset_sum _ fun _ _ => Real.continuous_cos.comp <| by continuity;      -- Substitute the definitions of fejer_sum and fejer_kernel into the goal.      simp [fejer_sum, fejer_kernel];      field_simp;      rw [ intervalIntegral.integral_div, h_fubini, mul_comm ];      rw [ mul_div_cancel₀ _ ( by positivity ), Finset.sum_congr rfl fun i hi => fourier_partial_sum_eq_integral hf h_per i x ] ; norm_num [ mul_assoc, mul_comm, mul_left_comm, Finset.mul_sum _ _ _ ]