fourierCoeffOn_bound

lemma fourierCoeffOn_bound {f : ℝ → ℂ} (f_continuous : Continuous f) :    ∃ C, ∀ n, ‖fourierCoeffOn Real.two_pi_pos f n‖ ≤ C := by  obtain ⟨C, f_bounded⟩ := continuous_bounded f_continuous.continuousOn  refine ⟨C, fun n ↦ ?_⟩  rw [fourierCoeffOn_eq_integral, norm_smul, sub_zero, Real.norm_of_nonneg (by positivity),      one_div, inv_mul_le_iff₀ Real.two_pi_pos]  calc ‖∫ (x : ℝ) in (0 : ℝ)..2 * π, fourier (-n) (↑x : AddCircle (2 * π)) • f x‖      ≤ ∫ (x : ℝ) in (0 : ℝ)..2 * π, ‖fourier (-n) (↑x : AddCircle (2 * π)) • f x‖ :=        intervalIntegral.norm_integral_le_integral_norm Real.two_pi_pos.le    _ = ∫ (x : ℝ) in (0 : ℝ)..2 * π, ‖f x‖ := by        apply intervalIntegral.integral_congr (fun x _ ↦ ?_)        simp only [norm_smul, fourier_apply, Circle.norm_coe, one_mul]    _ ≤ ∫ (_ : ℝ) in (0 : ℝ)..2 * π, C :=        intervalIntegral.integral_mono_on Real.two_pi_pos.le          (f_continuous.norm.intervalIntegrable 0 (2 * π))          intervalIntegrable_const          (fun x hx ↦ f_bounded x hx)    _ = 2 * π * C := by        rw [intervalIntegral.integral_const, smul_eq_mul, sub_zero]