internlm/Lean-Github huggingface dataset:
Theorem: nnabla_mul_log_sq
Proof 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
Proof 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
Theorem: nnabla_mul_log_sq
Proof 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)
Proof 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
Theorem: nnabla_mul_log_sq
Proof 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]
Proof 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
Theorem: nnabla_mul_log_sq
Proof 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
Proof 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)
Theorem: nnabla_mul_log_sq
Proof 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]
Proof 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)
Theorem: nnabla_mul_log_sq
Proof 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
Proof state after:
no goals
Theorem: nnabla_mul_log_sq
Proof 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)
Proof state after:
no goals
Theorem: nnabla_mul_log_sq
Proof 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
Proof state after:
no goals
Theorem: nnabla_mul_log_sq
Proof 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
Proof state after:
no goals
Theorem: nnabla_mul_log_sq
Proof 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
Proof state after:
no goals
Theorem: nnabla_bound_aux
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
⊢ (nnabla fun n => 1 / (n * ((2 * π) ^ 2 + (n / x).log ^ 2))) =O[atTop] fun n => 1 / (n.log ^ 2 * n ^ 2)
Tactic:
let d n : ℝ := n * ((2 * π) ^ 2 + Real.log (n / x) ^ 2)
Proof state after:
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)
⊢ (nnabla fun n => 1 / (n * ((2 * π) ^ 2 + (n / x).log ^ 2))) =O[atTop] fun n => 1 / (n.log ^ 2 * n ^ 2)
Theorem: nnabla_bound_aux
Proof state before:
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)
⊢ (nnabla fun n => 1 / (n * ((2 * π) ^ 2 + (n / x).log ^ 2))) =O[atTop] fun n => 1 / (n.log ^ 2 * n ^ 2)
Tactic:
change (fun x_1 ↦ nnabla (fun n ↦ 1 / d n) x_1) =O[atTop] _
Proof state after:
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)
⊢ (fun x_1 => nnabla (fun n => 1 / d n) x_1) =O[atTop] fun n => 1 / (n.log ^ 2 * n ^ 2)
Theorem: nnabla_bound_aux
Proof state before:
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)
⊢ (fun x_1 => nnabla (fun n => 1 / d n) x_1) =O[atTop] fun n => 1 / (n.log ^ 2 * n ^ 2)
Tactic:
have l2 : ∀ᶠ n in atTop, 0 < d n := (nnabla_bound_aux2 ((2 * π) ^ 2) hx)
Proof state after:
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
⊢ (fun x_1 => nnabla (fun n => 1 / d n) x_1) =O[atTop] fun n => 1 / (n.log ^ 2 * n ^ 2)
Theorem: nnabla_bound_aux
Proof state before:
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
⊢ (fun x_1 => nnabla (fun n => 1 / d n) x_1) =O[atTop] fun n => 1 / (n.log ^ 2 * n ^ 2)
Tactic:
have l3 : ∀ᶠ n in atTop, 0 < d (n + 1) :=
  (tendsto_atTop_add_const_right atTop (1 : ℝ) tendsto_id).eventually l2
Proof state after:
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)
⊢ (fun x_1 => nnabla (fun n => 1 / d n) x_1) =O[atTop] fun n => 1 / (n.log ^ 2 * n ^ 2)
Theorem: nnabla_bound_aux
Proof state before:
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)
⊢ (fun x_1 => nnabla (fun n => 1 / d n) x_1) =O[atTop] fun n => 1 / (n.log ^ 2 * n ^ 2)
Tactic:
have l1 : ∀ᶠ n : ℝ in atTop, nnabla (fun n ↦ 1 / d n) n = (d (n + 1) - d n) * (d n)⁻¹ * (d (n + 1))⁻¹ := by
  filter_upwards [l2, l3] with n l2 l3
  rw [nnabla, one_div, one_div, inv_sub_inv l2.ne.symm l3.ne.symm, div_eq_mul_inv, mul_inv, mul_assoc]
Proof state after:
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))⁻¹
⊢ (fun x_1 => nnabla (fun n => 1 / d n) x_1) =O[atTop] fun n => 1 / (n.log ^ 2 * n ^ 2)
Theorem: nnabla_bound_aux
Proof state before:
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)⁻¹
⊢ (fun x_1 => nnabla (fun n => 1 / d n) x_1) =O[atTop] fun n => 1 / (n.log ^ 2 * n ^ 2)
Tactic:
have l5 : (fun n => (d (n + 1))⁻¹) =O[atTop] (fun n => (n * (Real.log n) ^ 2)⁻¹) := by
  refine IsBigO.trans ?_ l4
  rw [isBigO_iff] ; use 1
  have e1 : ∀ᶠ n in atTop, 0 < d n := by
    apply eventually_of_mem (Ici_mem_atTop 1) ; intro n (hn : 1 ≤ n)
    have r1 : 0 < n := by linarith
    have r2 : 0 < (2 * π) ^ 2 := by apply sq_pos_of_ne_zero ; norm_num [pi_ne_zero]
    have r3 : 0 ≤ Real.log (↑n / x) ^ 2 := sq_nonneg _
    apply mul_pos r1 (by linarith)
  have e2 : ∀ᶠ n in atTop, 0 < d (n + 1) := (tendsto_atTop_add_const_right atTop (1 : ℝ) tendsto_id).eventually e1
  have e3 : ∀ᶠ n in atTop, d n ≤ d (n + 1) := by
    have : ∀ᶠ n in atTop, x ≤ n := by simpa using eventually_ge_atTop x
    filter_upwards [this] with n hn
    have e2 : 1 ≤ n / x := (one_le_div (by linarith)).mpr hn
    have e3 : n ≤ n + 1 := by linarith
    have e4 : 0 ≤ n + 1 := by linarith
    dsimp [d]
    gcongr
    exact Real.log_nonneg e2
  filter_upwards [e1, e2, e3] with n e1 e2 e3
  simp_rw [one_mul, Real.norm_eq_abs, abs_inv, abs_eq_self.mpr e1.le, abs_eq_self.mpr e2.le, inv_le_inv e2 e1]
  exact e3
Proof state after:
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)⁻¹
l5 : (fun n => (d (n + 1))⁻¹) =O[atTop] fun n => (n * n.log ^ 2)⁻¹
⊢ (fun x_1 => nnabla (fun n => 1 / d n) x_1) =O[atTop] fun n => 1 / (n.log ^ 2 * n ^ 2)
Theorem: nnabla_bound_aux
Proof state before:
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)⁻¹
l5 : (fun n => (d (n + 1))⁻¹) =O[atTop] fun n => (n * n.log ^ 2)⁻¹
⊢ (fun x_1 => nnabla (fun n => 1 / d n) x_1) =O[atTop] fun n => 1 / (n.log ^ 2 * n ^ 2)
Tactic:
have l6 : (fun n => d (n + 1) - d n) =O[atTop] (fun n => (Real.log n) ^ 2) := by
  simpa [d, nabla] using (nnabla_mul_log_sq ((2 * π) ^ 2) (by linarith))
Proof state after:
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)⁻¹
l5 : (fun n => (d (n + 1))⁻¹) =O[atTop] fun n => (n * n.log ^ 2)⁻¹
l6 : (fun n => d (n + 1) - d n) =O[atTop] fun n => n.log ^ 2
⊢ (fun x_1 => nnabla (fun n => 1 / d n) x_1) =O[atTop] fun n => 1 / (n.log ^ 2 * n ^ 2)
Theorem: nnabla_bound_aux
Proof state before:
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)⁻¹
l5 : (fun n => (d (n + 1))⁻¹) =O[atTop] fun n => (n * n.log ^ 2)⁻¹
l6 : (fun n => d (n + 1) - d n) =O[atTop] fun n => n.log ^ 2
⊢ (fun x_1 => nnabla (fun n => 1 / d n) x_1) =O[atTop] fun n => 1 / (n.log ^ 2 * n ^ 2)
Tactic:
apply EventuallyEq.trans_isBigO l1
Proof state after:
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)⁻¹
l5 : (fun n => (d (n + 1))⁻¹) =O[atTop] fun n => (n * n.log ^ 2)⁻¹
l6 : (fun n => d (n + 1) - d n) =O[atTop] fun n => n.log ^ 2
⊢ (fun x => (d (x + 1) - d x) * (d x)⁻¹ * (d (x + 1))⁻¹) =O[atTop] fun n => 1 / (n.log ^ 2 * n ^ 2)
Theorem: nnabla_bound_aux
Proof state before:
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)⁻¹
l5 : (fun n => (d (n + 1))⁻¹) =O[atTop] fun n => (n * n.log ^ 2)⁻¹
l6 : (fun n => d (n + 1) - d n) =O[atTop] fun n => n.log ^ 2
⊢ (fun x => (d (x + 1) - d x) * (d x)⁻¹ * (d (x + 1))⁻¹) =O[atTop] fun n => 1 / (n.log ^ 2 * n ^ 2)
Tactic:
apply ((l6.mul l4).mul l5).trans_eventuallyEq
Proof state after:
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)⁻¹
l5 : (fun n => (d (n + 1))⁻¹) =O[atTop] fun n => (n * n.log ^ 2)⁻¹
l6 : (fun n => d (n + 1) - d n) =O[atTop] fun n => n.log ^ 2
⊢ (fun x => x.log ^ 2 * (x * x.log ^ 2)⁻¹ * (x * x.log ^ 2)⁻¹) =ᶠ[atTop] fun n => 1 / (n.log ^ 2 * n ^ 2)
Theorem: nnabla_bound_aux
Proof state before:
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)⁻¹
l5 : (fun n => (d (n + 1))⁻¹) =O[atTop] fun n => (n * n.log ^ 2)⁻¹
l6 : (fun n => d (n + 1) - d n) =O[atTop] fun n => n.log ^ 2
⊢ (fun x => x.log ^ 2 * (x * x.log ^ 2)⁻¹ * (x * x.log ^ 2)⁻¹) =ᶠ[atTop] fun n => 1 / (n.log ^ 2 * n ^ 2)
Tactic:
apply eventually_of_mem (Ici_mem_atTop 2)
Proof state after:
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)⁻¹
l5 : (fun n => (d (n + 1))⁻¹) =O[atTop] fun n => (n * n.log ^ 2)⁻¹
l6 : (fun n => d (n + 1) - d n) =O[atTop] fun n => n.log ^ 2
⊢ ∀ x ∈ Ici 2, (fun x => x.log ^ 2 * (x * x.log ^ 2)⁻¹ * (x * x.log ^ 2)⁻¹) x = (fun n => 1 / (n.log ^ 2 * n ^ 2)) x
Theorem: nnabla_bound_aux
Proof state before:
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)⁻¹
l5 : (fun n => (d (n + 1))⁻¹) =O[atTop] fun n => (n * n.log ^ 2)⁻¹
l6 : (fun n => d (n + 1) - d n) =O[atTop] fun n => n.log ^ 2
⊢ ∀ x ∈ Ici 2, (fun x => x.log ^ 2 * (x * x.log ^ 2)⁻¹ * (x * x.log ^ 2)⁻¹) x = (fun n => 1 / (n.log ^ 2 * n ^ 2)) x
Tactic:
intro n (hn : 2 ≤ n)
Proof state after:
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)⁻¹
l5 : (fun n => (d (n + 1))⁻¹) =O[atTop] fun n => (n * n.log ^ 2)⁻¹
l6 : (fun n => d (n + 1) - d n) =O[atTop] fun n => n.log ^ 2
n : ℝ
hn : 2 ≤ n
⊢ (fun x => x.log ^ 2 * (x * x.log ^ 2)⁻¹ * (x * x.log ^ 2)⁻¹) n = (fun n => 1 / (n.log ^ 2 * n ^ 2)) n
Theorem: nnabla_bound_aux
Proof state before:
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)⁻¹
l5 : (fun n => (d (n + 1))⁻¹) =O[atTop] fun n => (n * n.log ^ 2)⁻¹
l6 : (fun n => d (n + 1) - d n) =O[atTop] fun n => n.log ^ 2
n : ℝ
hn : 2 ≤ n
⊢ (fun x => x.log ^ 2 * (x * x.log ^ 2)⁻¹ * (x * x.log ^ 2)⁻¹) n = (fun n => 1 / (n.log ^ 2 * n ^ 2)) n
Tactic:
have : Real.log n ≠ 0 := by
  have e1 : n ≠ 0 := by linarith
  have e2 : n ≠ 1 := by linarith
  have e3 : n ≠ -1 := by linarith
  simp [e1, e2, e3]
Proof state after:
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)⁻¹
l5 : (fun n => (d (n + 1))⁻¹) =O[atTop] fun n => (n * n.log ^ 2)⁻¹
l6 : (fun n => d (n + 1) - d n) =O[atTop] fun n => n.log ^ 2
n : ℝ
hn : 2 ≤ n
this : n.log ≠ 0
⊢ (fun x => x.log ^ 2 * (x * x.log ^ 2)⁻¹ * (x * x.log ^ 2)⁻¹) n = (fun n => 1 / (n.log ^ 2 * n ^ 2)) n