linarith
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)
l3 : a =O[atTop] fun n => 1 / ↑n
l4 : nnabla a =O[atTop] fun n => (↑n ^ 2 * (↑n).log ^ 2)⁻¹
x : ℕ
hx : 2 ≤ x
⊢ ¬x = 0
no goals