fourierConv_ofTwiceDifferentiable

lemma fourierConv_ofTwiceDifferentiable {f : ℝ → ℂ} (periodicf : f.Periodic (2 * π))    (fdiff : ContDiff ℝ 2 f) {ε : ℝ} (εpos : ε > 0) :    ∃ N₀, ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * π), ‖f x - S_ N f x‖ ≤ ε := by  set g : C(AddCircle (2 * π), ℂ) := ⟨AddCircle.liftIco (2 * π) 0 f,    AddCircle.liftIco_continuous ((periodicf 0).symm) fdiff.continuous.continuousOn⟩ with g_def  have two_pi_pos' : 0 < 0 + 2 * π := by linarith [Real.two_pi_pos]  have fourierCoeff_correspondence {i : ℤ} : fourierCoeff g i = fourierCoeffOn two_pi_pos' f i := fourierCoeff_liftIco_eq f i  simp only [zero_add] at fourierCoeff_correspondence  have function_sum : HasSum (fun (i : ℤ) => fourierCoeff g i • fourier i) g := by    apply hasSum_fourier_series_of_summable    obtain ⟨C, hC⟩ := fourierCoeffOn_ContDiff_two_bound periodicf fdiff    set maj : ℤ → ℝ := fun i ↦ 1 / (i ^ 2) * C with maj_def    have summable_maj : Summable maj := by      by_cases Ceq0 : C = 0      · simp [maj_def, Ceq0, one_div, mul_zero, summable_zero]      · rw [← summable_div_const_iff Ceq0]        convert! Real.summable_one_div_int_pow.mpr one_lt_two using 1        simp [maj_def, mul_div_cancel_right₀, Ceq0]    rw [summable_congr @fourierCoeff_correspondence, ←summable_norm_iff]    apply summable_of_le_on_nonzero _ _ summable_maj <;> intro i    · simp    · intro ine0; simpa only [maj_def, one_div_mul_eq_div] using hC i ine0  have := int_sum_nat function_sum  rw [ContinuousMap.tendsto_iff_tendstoUniformly, Metric.tendstoUniformly_iff] at this  have := this ε εpos  rw [Filter.eventually_atTop] at this  obtain ⟨N₀, hN₀⟩ := this  refine ⟨N₀, fun N hN x hx ↦ ?_⟩  have := hN₀ N hN.le x  simp only [Complex.dist_eq, ContinuousMap.coe_sum, Finset.sum_apply] at this  convert! this.le using 2  congr 1  · rw [g_def, ContinuousMap.coe_mk]    by_cases h : x = 2 * π    · conv => lhs; rw [h, ← zero_add  (2 * π), periodicf]      have := AddCircle.coe_add_period (2 * π) 0      rw [zero_add] at this      rw [h, this, AddCircle.liftIco_coe_apply]      simp [pi_pos]    · have : x ∈ Set.Ico 0 (2 * π) := ⟨hx.1, lt_of_le_of_ne hx.2 h⟩      simp [AddCircle.liftIco_coe_apply, this]  · simp [partialFourierSum, fourierCoeff_correspondence]