have l5 : BoundedAtFilter atTop (fun n : ℕ => C / (1 + (Real.log (↑n / x) / (2 * π)) ^ 2)) := by
  field_simp [BoundedAtFilter]
  apply isBigO_of_le' (c := C) ; intro n
  have : 0 ≤ (2 * π) ^ 2 + Real.log (n / x) ^ 2 := by positivity
  simp [abs_eq_self.mpr hC, abs_eq_self.mpr pi_nonneg, abs_eq_self.mpr this]
  apply div_le_of_nonneg_of_le_mul this hC
  gcongr
  apply le_add_of_le_of_nonneg le_rfl (sq_nonneg _)
n : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
C : ℝ
hC : 0 ≤ C
a : ℕ → ℝ := fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
hcheby : (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
l1 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑(n + 1)
l2 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑n
⊢ Summable fun n => ‖f n‖ / ↑n * (C / (1 + (1 / (2 * π) * (↑n / x).log) ^ 2))
n : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
C : ℝ
hC : 0 ≤ C
a : ℕ → ℝ := fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
hcheby : (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
l1 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑(n + 1)
l2 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑n
l5 : atTop.BoundedAtFilter fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2)
⊢ Summable fun n => ‖f n‖ / ↑n * (C / (1 + (1 / (2 * π) * (↑n / x).log) ^ 2))