fejer_sum_eq_integral_alt

theorem fejer_sum_eq_integral_alt {f : ℝ → ℝ} (hf_int : IntervalIntegrable f MeasureTheory.volume (-Real.pi) Real.pi)    (hf_per : Function.Periodic f (2 * Real.pi)) (n : ℕ) (x : ℝ) :    fejer_sum f n x = (1 / Real.pi) * ∫ t in (-Real.pi)..Real.pi, f (x - t) * fejer_kernel n t := by      convert fejer_sum_eq_integral hf_int hf_per n x using 1;      -- By substitution using $ u = x - t $, we can rewrite the integral.      have h_subst : ∀ a b : ℝ, ∫ t in a..b, f (x - t) * fejer_kernel n t = ∫ u in (x - b).. (x - a), f u * fejer_kernel n (x - u) := by        norm_num [ ← intervalIntegral.integral_comp_sub_left ];      norm_num [ h_subst ];      convert integral_periodic_shift _ _ _ _ using 2;      · intro u; simp +decide [ hf_per, fejer_kernel ];        simp +decide [ dirichlet_kernel, hf_per ];        norm_num [ hf_per, mul_add, mul_sub, Real.cos_add, Real.cos_sub ];        norm_num [ show ∀ k : ℕ, Real.sin ( k * ( 2 * Real.pi ) ) = 0 from fun k => Real.sin_eq_zero_iff.mpr ⟨ k * 2, by push_cast; ring ⟩, hf_per ];        exact Or.inl <| hf_per u;      · apply_rules [ IntervalIntegrable.mul_continuousOn, hf_int ];        refine' Continuous.continuousOn _;        refine' Continuous.mul _ _;        · continuity;        · refine' continuous_finset_sum _ fun i hi => _;          exact continuous_const.add ( continuous_finset_sum _ fun j hj => Real.continuous_cos.comp ( by continuity ) )