theorem close_smooth_approx_periodic {T : ℝ} {f : ℝ → ℂ} (unicontf : UniformContinuous f) (periodicf : Function.Periodic f T) {ε : ℝ} (εpos : ε > 0) : ∃ (f₀ : ℝ → ℂ), ContDiff ℝ (↑⊤) f₀ ∧ Function.Periodic f₀ T ∧ ∀ (x : ℝ), ‖f x - f₀ x‖ ≤ ε

theorem close_smooth_approx_periodic_Lp {T : ℝ} [hT : Fact (0 < T)] {f : ℝ → ℂ} {p : ENNReal} (hp : 1 ≤ p) (hp' : p ≠ ⊤) (hf : MeasureTheory.MemLp f p (MeasureTheory.volume.restrict (Set.Ioc 0 T))) {ε : NNReal} (εpos : 0 < ε) : ∃ (f₀ : ℝ → ℂ), ContDiff ℝ (↑⊤) f₀ ∧ Function.Periodic f₀ T ∧ MeasureTheory.eLpNorm (f - f₀) p (MeasureTheory.volume.restrict (Set.Ioc 0 T)) ≤ ↑ε

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), ‖f x‖ ≤ C

theorem fourierCoeffOn_bound {f : ℝ → ℂ} (f_continuous : Continuous f) : ∃ (C : ℝ), ∀ (n : ℤ), ‖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 → ‖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 instFactLtRealOfNatHMulPi_carleson_1 : Fact (0 < 2 * Real.pi)

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‖ ≤ ε