linarith
n✝ : ℕ
A a b c d✝ u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
d : ℝ → ℝ := fun n => n * ((2 * π) ^ 2 + (n / x).log ^ 2)
l2 : ∀ᶠ (n : ℝ) in atTop, 0 < d n
l3 : ∀ᶠ (n : ℝ) in atTop, 0 < d (n + 1)
l1 : ∀ᶠ (n : ℝ) in atTop, nnabla (fun n => 1 / d n) n = (d (n + 1) - d n) * (d n)⁻¹ * (d (n + 1))⁻¹
l4 : (fun n => (d n)⁻¹) =O[atTop] fun n => (n * n.log ^ 2)⁻¹
n : ℝ
hn : 1 ≤ n
r1 : 0 < n
r2 : 0 < (2 * π) ^ 2
r3 : 0 ≤ (n / x).log ^ 2
⊢ 0 < (2 * π) ^ 2 + (n / x).log ^ 2
no goals