fourierCoeffOn_ContDiff_two_bound

lemma fourierCoeffOn_ContDiff_two_bound {f : ℝ → ℂ} (periodicf : f.Periodic (2 * π)) (fdiff : ContDiff ℝ 2 f) :    ∃ C, ∀ n ≠ 0, ‖fourierCoeffOn Real.two_pi_pos f n‖ ≤ C / n ^ 2 := by  have h : ∀ x ∈ Set.uIcc 0 (2 * π), HasDerivAt f (deriv f x) x := by    intro x _    rw [hasDerivAt_deriv_iff]    exact fdiff.differentiable (by norm_num) _  have h' : ∀ x ∈ Set.uIcc 0 (2 * π), HasDerivAt (deriv f) (deriv (deriv f) x) x := by    intro x _    rw [hasDerivAt_deriv_iff]    exact ((contDiff_succ_iff_deriv (n := 1)).mp fdiff).2.2.differentiable (by norm_num) _  /-Get better representation for the fourier coefficients of f. -/  have fourierCoeffOn_eq {n : ℤ} (hn : n ≠ 0): (fourierCoeffOn Real.two_pi_pos f n) = - 1 / (n^2) * fourierCoeffOn Real.two_pi_pos (fun x ↦ deriv (deriv f) x) n := by    rw [fourierCoeffOn_of_hasDerivAt Real.two_pi_pos hn h, fourierCoeffOn_of_hasDerivAt Real.two_pi_pos hn h']    · have h1 := periodicf 0      have periodic_deriv_f : (deriv f).Periodic (2 * π) := periodic_deriv (fdiff.of_le one_le_two) periodicf      have h2 := periodic_deriv_f 0      simp at h1 h2      simp [h1, h2]      ring_nf      simp [pi_pos.ne.symm]    · exact (contDiff_one_iff_deriv.mp ((contDiff_succ_iff_deriv (n := 1)).mp        fdiff).2.2).2.intervalIntegrable ..    · exact ((contDiff_succ_iff_deriv (n := 1)).mp fdiff).2.2.continuous.intervalIntegrable ..  obtain ⟨C, hC⟩ := fourierCoeffOn_bound (contDiff_one_iff_deriv.mp    ((contDiff_succ_iff_deriv (n := 1)).mp fdiff).2.2).2  refine ⟨C, fun n hn ↦ ?_⟩  simp only [fourierCoeffOn_eq hn, Complex.norm_mul, Complex.norm_div, norm_neg, norm_one, norm_pow,    Complex.norm_intCast, sq_abs, one_div, div_eq_mul_inv C, mul_comm C]  gcongr  exact hC n