Theorem: nnabla_mul_log_sq (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
hb : 0 < b
⊢ (nabla fun x => x * (a + (x / b).log ^ 2)) =O[atTop] fun x => x.log ^ 2
Tactic:
have l1 : nabla (fun n => n * (a + Real.log (n / b) ^ 2)) = fun n =>
    a + Real.log ((n + 1) / b) ^ 2 + (n * (Real.log ((n + 1) / b) ^ 2 - Real.log (n / b) ^ 2)) := by
  ext n ; simp [nabla] ; ring
State after:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
hb : 0 < b
l1 :
  (nabla fun n => n * (a + (n / b).log ^ 2)) = fun n =>
    a + ((n + 1) / b).log ^ 2 + n * (((n + 1) / b).log ^ 2 - (n / b).log ^ 2)
⊢ (nabla fun x => x * (a + (x / b).log ^ 2)) =O[atTop] fun x => x.log ^ 2

State before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
hb : 0 < b
l1 :
  (nabla fun n => n * (a + (n / b).log ^ 2)) = fun n =>
    a + ((n + 1) / b).log ^ 2 + n * (((n + 1) / b).log ^ 2 - (n / b).log ^ 2)
⊢ (nabla fun x => x * (a + (x / b).log ^ 2)) =O[atTop] fun x => x.log ^ 2
Tactic:
have l2 := (isLittleO_const_of_tendsto_atTop a ((tendsto_pow_atTop two_ne_zero).comp tendsto_log_atTop)).isBigO
State after:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
hb : 0 < b
l1 :
  (nabla fun n => n * (a + (n / b).log ^ 2)) = fun n =>
    a + ((n + 1) / b).log ^ 2 + n * (((n + 1) / b).log ^ 2 - (n / b).log ^ 2)
l2 : (fun x => a) =O[atTop] ((fun x => x ^ 2) ∘ Real.log)
⊢ (nabla fun x => x * (a + (x / b).log ^ 2)) =O[atTop] fun x => x.log ^ 2

State before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
hb : 0 < b
l1 :
  (nabla fun n => n * (a + (n / b).log ^ 2)) = fun n =>
    a + ((n + 1) / b).log ^ 2 + n * (((n + 1) / b).log ^ 2 - (n / b).log ^ 2)
l2 : (fun x => a) =O[atTop] ((fun x => x ^ 2) ∘ Real.log)
⊢ (nabla fun x => x * (a + (x / b).log ^ 2)) =O[atTop] fun x => x.log ^ 2
Tactic:
have l3 := (log_add_div_isBigO_log 1 hb).sq
State after:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
hb : 0 < b
l1 :
  (nabla fun n => n * (a + (n / b).log ^ 2)) = fun n =>
    a + ((n + 1) / b).log ^ 2 + n * (((n + 1) / b).log ^ 2 - (n / b).log ^ 2)
l2 : (fun x => a) =O[atTop] ((fun x => x ^ 2) ∘ Real.log)
l3 : (fun n => ((n + 1) / b).log ^ 2) =O[atTop] fun n => n.log ^ 2
⊢ (nabla fun x => x * (a + (x / b).log ^ 2)) =O[atTop] fun x => x.log ^ 2

State before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
hb : 0 < b
l1 :
  (nabla fun n => n * (a + (n / b).log ^ 2)) = fun n =>
    a + ((n + 1) / b).log ^ 2 + n * (((n + 1) / b).log ^ 2 - (n / b).log ^ 2)
l2 : (fun x => a) =O[atTop] ((fun x => x ^ 2) ∘ Real.log)
l3 : (fun n => ((n + 1) / b).log ^ 2) =O[atTop] fun n => n.log ^ 2
⊢ (nabla fun x => x * (a + (x / b).log ^ 2)) =O[atTop] fun x => x.log ^ 2
Tactic:
have l4 : (fun x => Real.log ((x + 1) / b) + Real.log (x / b)) =O[atTop] Real.log := by
  simpa using (log_add_div_isBigO_log _ hb).add (log_add_div_isBigO_log 0 hb)
State after:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
hb : 0 < b
l1 :
  (nabla fun n => n * (a + (n / b).log ^ 2)) = fun n =>
    a + ((n + 1) / b).log ^ 2 + n * (((n + 1) / b).log ^ 2 - (n / b).log ^ 2)
l2 : (fun x => a) =O[atTop] ((fun x => x ^ 2) ∘ Real.log)
l3 : (fun n => ((n + 1) / b).log ^ 2) =O[atTop] fun n => n.log ^ 2
l4 : (fun x => ((x + 1) / b).log + (x / b).log) =O[atTop] Real.log
⊢ (nabla fun x => x * (a + (x / b).log ^ 2)) =O[atTop] fun x => x.log ^ 2

State before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
hb : 0 < b
l1 :
  (nabla fun n => n * (a + (n / b).log ^ 2)) = fun n =>
    a + ((n + 1) / b).log ^ 2 + n * (((n + 1) / b).log ^ 2 - (n / b).log ^ 2)
l2 : (fun x => a) =O[atTop] ((fun x => x ^ 2) ∘ Real.log)
l3 : (fun n => ((n + 1) / b).log ^ 2) =O[atTop] fun n => n.log ^ 2
l4 : (fun x => ((x + 1) / b).log + (x / b).log) =O[atTop] Real.log
⊢ (nabla fun x => x * (a + (x / b).log ^ 2)) =O[atTop] fun x => x.log ^ 2
Tactic:
have e2 : (fun x : ℝ => x * (Real.log x * (1 / x))) =ᶠ[atTop] Real.log := by
  filter_upwards [eventually_ge_atTop 1] with x hx using by field_simp
State after:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
hb : 0 < b
l1 :
  (nabla fun n => n * (a + (n / b).log ^ 2)) = fun n =>
    a + ((n + 1) / b).log ^ 2 + n * (((n + 1) / b).log ^ 2 - (n / b).log ^ 2)
l2 : (fun x => a) =O[atTop] ((fun x => x ^ 2) ∘ Real.log)
l3 : (fun n => ((n + 1) / b).log ^ 2) =O[atTop] fun n => n.log ^ 2
l4 : (fun x => ((x + 1) / b).log + (x / b).log) =O[atTop] Real.log
e2 : (fun x => x * (x.log * (1 / x))) =ᶠ[atTop] Real.log
⊢ (nabla fun x => x * (a + (x / b).log ^ 2)) =O[atTop] fun x => x.log ^ 2

State before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
hb : 0 < b
l1 :
  (nabla fun n => n * (a + (n / b).log ^ 2)) = fun n =>
    a + ((n + 1) / b).log ^ 2 + n * (((n + 1) / b).log ^ 2 - (n / b).log ^ 2)
l2 : (fun x => a) =O[atTop] ((fun x => x ^ 2) ∘ Real.log)
l3 : (fun n => ((n + 1) / b).log ^ 2) =O[atTop] fun n => n.log ^ 2
l4 : (fun x => ((x + 1) / b).log + (x / b).log) =O[atTop] Real.log
e2 : (fun x => x * (x.log * (1 / x))) =ᶠ[atTop] Real.log
⊢ (nabla fun x => x * (a + (x / b).log ^ 2)) =O[atTop] fun x => x.log ^ 2
Tactic:
have l5 : (fun n ↦ n * (Real.log n * (1 / n))) =O[atTop] (fun n ↦ (Real.log n) ^ 2) :=
  e2.trans_isBigO (by simpa using (isLittleO_mul_add_sq 1 0).isBigO.comp_tendsto Real.tendsto_log_atTop)
State after:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
hb : 0 < b
l1 :
  (nabla fun n => n * (a + (n / b).log ^ 2)) = fun n =>
    a + ((n + 1) / b).log ^ 2 + n * (((n + 1) / b).log ^ 2 - (n / b).log ^ 2)
l2 : (fun x => a) =O[atTop] ((fun x => x ^ 2) ∘ Real.log)
l3 : (fun n => ((n + 1) / b).log ^ 2) =O[atTop] fun n => n.log ^ 2
l4 : (fun x => ((x + 1) / b).log + (x / b).log) =O[atTop] Real.log
e2 : (fun x => x * (x.log * (1 / x))) =ᶠ[atTop] Real.log
l5 : (fun n => n * (n.log * (1 / n))) =O[atTop] fun n => n.log ^ 2
⊢ (nabla fun x => x * (a + (x / b).log ^ 2)) =O[atTop] fun x => x.log ^ 2

State before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
hb : 0 < b
l1 :
  (nabla fun n => n * (a + (n / b).log ^ 2)) = fun n =>
    a + ((n + 1) / b).log ^ 2 + n * (((n + 1) / b).log ^ 2 - (n / b).log ^ 2)
l2 : (fun x => a) =O[atTop] ((fun x => x ^ 2) ∘ Real.log)
l3 : (fun n => ((n + 1) / b).log ^ 2) =O[atTop] fun n => n.log ^ 2
l4 : (fun x => ((x + 1) / b).log + (x / b).log) =O[atTop] Real.log
e2 : (fun x => x * (x.log * (1 / x))) =ᶠ[atTop] Real.log
l5 : (fun n => n * (n.log * (1 / n))) =O[atTop] fun n => n.log ^ 2
⊢ (nabla fun x => x * (a + (x / b).log ^ 2)) =O[atTop] fun x => x.log ^ 2
Tactic:
simp_rw [l1, _root_.sq_sub_sq]
State after:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
hb : 0 < b
l1 :
  (nabla fun n => n * (a + (n / b).log ^ 2)) = fun n =>
    a + ((n + 1) / b).log ^ 2 + n * (((n + 1) / b).log ^ 2 - (n / b).log ^ 2)
l2 : (fun x => a) =O[atTop] ((fun x => x ^ 2) ∘ Real.log)
l3 : (fun n => ((n + 1) / b).log ^ 2) =O[atTop] fun n => n.log ^ 2
l4 : (fun x => ((x + 1) / b).log + (x / b).log) =O[atTop] Real.log
e2 : (fun x => x * (x.log * (1 / x))) =ᶠ[atTop] Real.log
l5 : (fun n => n * (n.log * (1 / n))) =O[atTop] fun n => n.log ^ 2
⊢ (fun n =>
      a + ((n + 1) / b).log ^ 2 + n * ((((n + 1) / b).log + (n / b).log) * (((n + 1) / b).log - (n / b).log))) =O[atTop]
    fun x => x.log ^ 2

State before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
hb : 0 < b
⊢ (nabla fun n => n * (a + (n / b).log ^ 2)) = fun n =>
    a + ((n + 1) / b).log ^ 2 + n * (((n + 1) / b).log ^ 2 - (n / b).log ^ 2)
Tactic:
ext n
State after:
case h
n✝ : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
hb : 0 < b
n : ℝ
⊢ nabla (fun n => n * (a + (n / b).log ^ 2)) n =
    a + ((n + 1) / b).log ^ 2 + n * (((n + 1) / b).log ^ 2 - (n / b).log ^ 2)

State before:
case h
n✝ : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
hb : 0 < b
n : ℝ
⊢ nabla (fun n => n * (a + (n / b).log ^ 2)) n =
    a + ((n + 1) / b).log ^ 2 + n * (((n + 1) / b).log ^ 2 - (n / b).log ^ 2)
Tactic:
simp [nabla]
State after:
case h
n✝ : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
hb : 0 < b
n : ℝ
⊢ (n + 1) * (a + ((n + 1) / b).log ^ 2) - n * (a + (n / b).log ^ 2) =
    a + ((n + 1) / b).log ^ 2 + n * (((n + 1) / b).log ^ 2 - (n / b).log ^ 2)

State before:
case h
n✝ : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
hb : 0 < b
n : ℝ
⊢ (n + 1) * (a + ((n + 1) / b).log ^ 2) - n * (a + (n / b).log ^ 2) =
    a + ((n + 1) / b).log ^ 2 + n * (((n + 1) / b).log ^ 2 - (n / b).log ^ 2)
Tactic:
ring
State after:
no goals

State before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
hb : 0 < b
l1 :
  (nabla fun n => n * (a + (n / b).log ^ 2)) = fun n =>
    a + ((n + 1) / b).log ^ 2 + n * (((n + 1) / b).log ^ 2 - (n / b).log ^ 2)
l2 : (fun x => a) =O[atTop] ((fun x => x ^ 2) ∘ Real.log)
l3 : (fun n => ((n + 1) / b).log ^ 2) =O[atTop] fun n => n.log ^ 2
⊢ (fun x => ((x + 1) / b).log + (x / b).log) =O[atTop] Real.log
Tactic:
simpa using (log_add_div_isBigO_log _ hb).add (log_add_div_isBigO_log 0 hb)
State after:
no goals

State before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
hb : 0 < b
l1 :
  (nabla fun n => n * (a + (n / b).log ^ 2)) = fun n =>
    a + ((n + 1) / b).log ^ 2 + n * (((n + 1) / b).log ^ 2 - (n / b).log ^ 2)
l2 : (fun x => a) =O[atTop] ((fun x => x ^ 2) ∘ Real.log)
l3 : (fun n => ((n + 1) / b).log ^ 2) =O[atTop] fun n => n.log ^ 2
l4 : (fun x => ((x + 1) / b).log + (x / b).log) =O[atTop] Real.log
⊢ (fun x => x * (x.log * (1 / x))) =ᶠ[atTop] Real.log
Tactic:
filter_upwards [eventually_ge_atTop 1] with x hx using by field_simp
State after:
no goals

State before:
n : ℕ
A a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
hb : 0 < b
l1 :
  (nabla fun n => n * (a + (n / b).log ^ 2)) = fun n =>
    a + ((n + 1) / b).log ^ 2 + n * (((n + 1) / b).log ^ 2 - (n / b).log ^ 2)
l2 : (fun x => a) =O[atTop] ((fun x => x ^ 2) ∘ Real.log)
l3 : (fun n => ((n + 1) / b).log ^ 2) =O[atTop] fun n => n.log ^ 2
l4 : (fun x => ((x + 1) / b).log + (x / b).log) =O[atTop] Real.log
x : ℝ
hx : 1 ≤ x
⊢ x * (x.log * (1 / x)) = x.log
Tactic:
field_simp
State after:
no goals

State before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
hb : 0 < b
l1 :
  (nabla fun n => n * (a + (n / b).log ^ 2)) = fun n =>
    a + ((n + 1) / b).log ^ 2 + n * (((n + 1) / b).log ^ 2 - (n / b).log ^ 2)
l2 : (fun x => a) =O[atTop] ((fun x => x ^ 2) ∘ Real.log)
l3 : (fun n => ((n + 1) / b).log ^ 2) =O[atTop] fun n => n.log ^ 2
l4 : (fun x => ((x + 1) / b).log + (x / b).log) =O[atTop] Real.log
e2 : (fun x => x * (x.log * (1 / x))) =ᶠ[atTop] Real.log
⊢ Real.log =O[atTop] fun n => n.log ^ 2
Tactic:
simpa using (isLittleO_mul_add_sq 1 0).isBigO.comp_tendsto Real.tendsto_log_atTop
State after:
no goals