theorem close_smooth_approx_periodic {f : ℝ → ℂ} (unicontf : UniformContinuous f) (periodicf : Function.Periodic f (2 * Real.pi)) {ε : ℝ} (εpos : ε > 0) : ∃ (f₀ : ℝ → ℂ), ContDiff ℝ ⊤ f₀ ∧ Function.Periodic f₀ (2 * Real.pi) ∧ ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε

theorem summable_of_le_on_nonzero {f : ℤ → ℝ} {g : ℤ → ℝ} (hgpos : 0 ≤ g) (hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i) (summablef : Summable f) : Summable g

theorem continuous_bounded {f : ℝ → ℂ} (hf : ContinuousOn f (Set.Icc 0 (2 * Real.pi))) : ∃ (C : ℝ), ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C

theorem fourierCoeffOn_bound {f : ℝ → ℂ} (f_continuous : Continuous f) : ∃ (C : ℝ), ∀ (n : ℤ), Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C

theorem periodic_deriv {𝕜 : Type} [NontriviallyNormedField 𝕜] {F : Type} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {T : 𝕜} (diff_f : ContDiff 𝕜 1 f) (periodic_f : Function.Periodic f T) : Function.Periodic (deriv f) T

theorem fourierCoeffOn_ContDiff_two_bound {f : ℝ → ℂ} (periodicf : Function.Periodic f (2 * Real.pi)) (fdiff : ContDiff ℝ 2 f) : ∃ (C : ℝ), ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2

theorem int_sum_nat {β : Type u_1} [AddCommGroup β] [TopologicalSpace β] [ContinuousAdd β] {f : ℤ → β} {a : β} (hfa : HasSum f a) : Filter.Tendsto (fun (N : ℕ) => ∑ n ∈ Finset.Icc (-Int.ofNat N) ↑N, f n) Filter.atTop (nhds a)

theorem fourierConv_ofTwiceDifferentiable {f : ℝ → ℂ} (periodicf : Function.Periodic f (2 * Real.pi)) (fdiff : ContDiff ℝ 2 f) {ε : ℝ} (εpos : ε > 0) : ∃ (N₀ : ℕ), ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), ‖f x - partialFourierSum N f x‖ ≤ ε