Theorem: nnabla_bound (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 0 < x
⊢ (nnabla fun n => C / (1 + ((n / x).log / (2 * π)) ^ 2) / n) =O[atTop] fun n => (n ^ 2 * n.log ^ 2)⁻¹
Tactic:
field_simp
State after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 0 < x
⊢ (nnabla fun n => C * (2 * π) ^ 2 / (((2 * π) ^ 2 + (n / x).log ^ 2) * n)) =O[atTop] fun n => 1 / (n ^ 2 * n.log ^ 2)

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 0 < x
⊢ (nnabla fun n => C * (2 * π) ^ 2 / (((2 * π) ^ 2 + (n / x).log ^ 2) * n)) =O[atTop] fun n => 1 / (n ^ 2 * n.log ^ 2)
Tactic:
simp [div_eq_mul_inv]
State after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 0 < x
⊢ ((C * (2 * π) ^ 2) • nnabla fun n => n⁻¹ * ((2 * π) ^ 2 + (n * x⁻¹).log ^ 2)⁻¹) =O[atTop] fun n =>
    (n.log ^ 2)⁻¹ * (n ^ 2)⁻¹

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 0 < x
⊢ ((C * (2 * π) ^ 2) • nnabla fun n => n⁻¹ * ((2 * π) ^ 2 + (n * x⁻¹).log ^ 2)⁻¹) =O[atTop] fun n =>
    (n.log ^ 2)⁻¹ * (n ^ 2)⁻¹
Tactic:
apply IsBigO.const_mul_left
State after:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 0 < x
⊢ (fun x_1 => nnabla (fun n => n⁻¹ * ((2 * π) ^ 2 + (n * x⁻¹).log ^ 2)⁻¹) x_1) =O[atTop] fun n =>
    (n.log ^ 2)⁻¹ * (n ^ 2)⁻¹

State before:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 0 < x
⊢ (fun x_1 => nnabla (fun n => n⁻¹ * ((2 * π) ^ 2 + (n * x⁻¹).log ^ 2)⁻¹) x_1) =O[atTop] fun n =>
    (n.log ^ 2)⁻¹ * (n ^ 2)⁻¹
Tactic:
field_simp
State after:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 0 < x
⊢ (fun x_1 => nnabla (fun n => 1 / (n * ((2 * π) ^ 2 + (n / x).log ^ 2))) x_1) =O[atTop] fun n =>
    1 / (n.log ^ 2 * n ^ 2)

State before:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 0 < x
⊢ (fun x_1 => nnabla (fun n => 1 / (n * ((2 * π) ^ 2 + (n / x).log ^ 2))) x_1) =O[atTop] fun n =>
    1 / (n.log ^ 2 * n ^ 2)
Tactic:
exact nnabla_bound_aux hx
State after:
no goals