internlm/Lean-Github huggingface dataset:
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)⁻¹
⊢ ∀ x ∈ Ici 1, 0 < d x
Tactic:
intro n (hn : 1 ≤ 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)⁻¹
n : ℝ
hn : 1 ≤ n
⊢ 0 < d 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)⁻¹
n : ℝ
hn : 1 ≤ n
⊢ 0 < d n
Tactic:
have r1 : 0 < n := 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)⁻¹
n : ℝ
hn : 1 ≤ n
r1 : 0 < n
⊢ 0 < d 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)⁻¹
n : ℝ
hn : 1 ≤ n
r1 : 0 < n
⊢ 0 < d n
Tactic:
have r2 : 0 < (2 * π) ^ 2 := by apply sq_pos_of_ne_zero ; norm_num [pi_ne_zero]
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)⁻¹
n : ℝ
hn : 1 ≤ n
r1 : 0 < n
r2 : 0 < (2 * π) ^ 2
⊢ 0 < d 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)⁻¹
n : ℝ
hn : 1 ≤ n
r1 : 0 < n
r2 : 0 < (2 * π) ^ 2
⊢ 0 < d n
Tactic:
have r3 : 0 ≤ Real.log (↑n / x) ^ 2 := sq_nonneg _
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)⁻¹
n : ℝ
hn : 1 ≤ n
r1 : 0 < n
r2 : 0 < (2 * π) ^ 2
r3 : 0 ≤ (n / x).log ^ 2
⊢ 0 < d 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)⁻¹
n : ℝ
hn : 1 ≤ n
r1 : 0 < n
r2 : 0 < (2 * π) ^ 2
r3 : 0 ≤ (n / x).log ^ 2
⊢ 0 < d n
Tactic:
apply mul_pos r1 (by linarith)
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
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
⊢ 0 < n
Tactic:
linarith
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
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
⊢ 0 < (2 * π) ^ 2
Tactic:
apply sq_pos_of_ne_zero
Proof state after:
case a
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
⊢ 2 * π ≠ 0
Theorem: nnabla_bound_aux
Proof state before:
case a
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
⊢ 2 * π ≠ 0
Tactic:
norm_num [pi_ne_zero]
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
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
Tactic:
linarith
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
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)⁻¹
e1 : ∀ᶠ (n : ℝ) in atTop, 0 < d n
e2 : ∀ᶠ (n : ℝ) in atTop, 0 < d (n + 1)
⊢ ∀ᶠ (n : ℝ) in atTop, d n ≤ d (n + 1)
Tactic:
have : ∀ᶠ n in atTop, x ≤ n := by simpa using eventually_ge_atTop x
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)⁻¹
e1 : ∀ᶠ (n : ℝ) in atTop, 0 < d n
e2 : ∀ᶠ (n : ℝ) in atTop, 0 < d (n + 1)
this : ∀ᶠ (n : ℝ) in atTop, x ≤ n
⊢ ∀ᶠ (n : ℝ) in atTop, d n ≤ d (n + 1)
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)⁻¹
e1 : ∀ᶠ (n : ℝ) in atTop, 0 < d n
e2 : ∀ᶠ (n : ℝ) in atTop, 0 < d (n + 1)
this : ∀ᶠ (n : ℝ) in atTop, x ≤ n
⊢ ∀ᶠ (n : ℝ) in atTop, d n ≤ d (n + 1)
Tactic:
filter_upwards [this] with n hn
Proof state after:
case h
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)⁻¹
e1 : ∀ᶠ (n : ℝ) in atTop, 0 < d n
e2 : ∀ᶠ (n : ℝ) in atTop, 0 < d (n + 1)
this : ∀ᶠ (n : ℝ) in atTop, x ≤ n
n : ℝ
hn : x ≤ n
⊢ d n ≤ d (n + 1)
Theorem: nnabla_bound_aux
Proof state before:
case h
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)⁻¹
e1 : ∀ᶠ (n : ℝ) in atTop, 0 < d n
e2 : ∀ᶠ (n : ℝ) in atTop, 0 < d (n + 1)
this : ∀ᶠ (n : ℝ) in atTop, x ≤ n
n : ℝ
hn : x ≤ n
⊢ d n ≤ d (n + 1)
Tactic:
have e2 : 1 ≤ n / x := (one_le_div (by linarith)).mpr hn
Proof state after:
case h
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)⁻¹
e1 : ∀ᶠ (n : ℝ) in atTop, 0 < d n
e2✝ : ∀ᶠ (n : ℝ) in atTop, 0 < d (n + 1)
this : ∀ᶠ (n : ℝ) in atTop, x ≤ n
n : ℝ
hn : x ≤ n
e2 : 1 ≤ n / x
⊢ d n ≤ d (n + 1)
Theorem: nnabla_bound_aux
Proof state before:
case h
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)⁻¹
e1 : ∀ᶠ (n : ℝ) in atTop, 0 < d n
e2✝ : ∀ᶠ (n : ℝ) in atTop, 0 < d (n + 1)
this : ∀ᶠ (n : ℝ) in atTop, x ≤ n
n : ℝ
hn : x ≤ n
e2 : 1 ≤ n / x
⊢ d n ≤ d (n + 1)
Tactic:
have e3 : n ≤ n + 1 := by linarith
Proof state after:
case h
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)⁻¹
e1 : ∀ᶠ (n : ℝ) in atTop, 0 < d n
e2✝ : ∀ᶠ (n : ℝ) in atTop, 0 < d (n + 1)
this : ∀ᶠ (n : ℝ) in atTop, x ≤ n
n : ℝ
hn : x ≤ n
e2 : 1 ≤ n / x
e3 : n ≤ n + 1
⊢ d n ≤ d (n + 1)
Theorem: nnabla_bound_aux
Proof state before:
case h
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)⁻¹
e1 : ∀ᶠ (n : ℝ) in atTop, 0 < d n
e2✝ : ∀ᶠ (n : ℝ) in atTop, 0 < d (n + 1)
this : ∀ᶠ (n : ℝ) in atTop, x ≤ n
n : ℝ
hn : x ≤ n
e2 : 1 ≤ n / x
e3 : n ≤ n + 1
⊢ d n ≤ d (n + 1)
Tactic:
have e4 : 0 ≤ n + 1 := by linarith
Proof state after:
case h
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)⁻¹
e1 : ∀ᶠ (n : ℝ) in atTop, 0 < d n
e2✝ : ∀ᶠ (n : ℝ) in atTop, 0 < d (n + 1)
this : ∀ᶠ (n : ℝ) in atTop, x ≤ n
n : ℝ
hn : x ≤ n
e2 : 1 ≤ n / x
e3 : n ≤ n + 1
e4 : 0 ≤ n + 1
⊢ d n ≤ d (n + 1)
Theorem: nnabla_bound_aux
Proof state before:
case h
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)⁻¹
e1 : ∀ᶠ (n : ℝ) in atTop, 0 < d n
e2✝ : ∀ᶠ (n : ℝ) in atTop, 0 < d (n + 1)
this : ∀ᶠ (n : ℝ) in atTop, x ≤ n
n : ℝ
hn : x ≤ n
e2 : 1 ≤ n / x
e3 : n ≤ n + 1
e4 : 0 ≤ n + 1
⊢ d n ≤ d (n + 1)
Tactic:
dsimp [d]
Proof state after:
case h
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)⁻¹
e1 : ∀ᶠ (n : ℝ) in atTop, 0 < d n
e2✝ : ∀ᶠ (n : ℝ) in atTop, 0 < d (n + 1)
this : ∀ᶠ (n : ℝ) in atTop, x ≤ n
n : ℝ
hn : x ≤ n
e2 : 1 ≤ n / x
e3 : n ≤ n + 1
e4 : 0 ≤ n + 1
⊢ n * ((2 * π) ^ 2 + (n / x).log ^ 2) ≤ (n + 1) * ((2 * π) ^ 2 + ((n + 1) / x).log ^ 2)
Theorem: nnabla_bound_aux
Proof state before:
case h
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)⁻¹
e1 : ∀ᶠ (n : ℝ) in atTop, 0 < d n
e2✝ : ∀ᶠ (n : ℝ) in atTop, 0 < d (n + 1)
this : ∀ᶠ (n : ℝ) in atTop, x ≤ n
n : ℝ
hn : x ≤ n
e2 : 1 ≤ n / x
e3 : n ≤ n + 1
e4 : 0 ≤ n + 1
⊢ n * ((2 * π) ^ 2 + (n / x).log ^ 2) ≤ (n + 1) * ((2 * π) ^ 2 + ((n + 1) / x).log ^ 2)
Tactic:
gcongr
Proof state after:
case h.h₂.bc.ha
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)⁻¹
e1 : ∀ᶠ (n : ℝ) in atTop, 0 < d n
e2✝ : ∀ᶠ (n : ℝ) in atTop, 0 < d (n + 1)
this : ∀ᶠ (n : ℝ) in atTop, x ≤ n
n : ℝ
hn : x ≤ n
e2 : 1 ≤ n / x
e3 : n ≤ n + 1
e4 : 0 ≤ n + 1
⊢ 0 ≤ (n / x).log
Theorem: nnabla_bound_aux
Proof state before:
case h.h₂.bc.ha
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)⁻¹
e1 : ∀ᶠ (n : ℝ) in atTop, 0 < d n
e2✝ : ∀ᶠ (n : ℝ) in atTop, 0 < d (n + 1)
this : ∀ᶠ (n : ℝ) in atTop, x ≤ n
n : ℝ
hn : x ≤ n
e2 : 1 ≤ n / x
e3 : n ≤ n + 1
e4 : 0 ≤ n + 1
⊢ 0 ≤ (n / x).log
Tactic:
exact Real.log_nonneg e2
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
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)⁻¹
e1 : ∀ᶠ (n : ℝ) in atTop, 0 < d n
e2 : ∀ᶠ (n : ℝ) in atTop, 0 < d (n + 1)
⊢ ∀ᶠ (n : ℝ) in atTop, x ≤ n
Tactic:
simpa using eventually_ge_atTop x
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
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)⁻¹
e1 : ∀ᶠ (n : ℝ) in atTop, 0 < d n
e2 : ∀ᶠ (n : ℝ) in atTop, 0 < d (n + 1)
this : ∀ᶠ (n : ℝ) in atTop, x ≤ n
n : ℝ
hn : x ≤ n
⊢ 0 < x
Tactic:
linarith
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
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)⁻¹
e1 : ∀ᶠ (n : ℝ) in atTop, 0 < d n
e2✝ : ∀ᶠ (n : ℝ) in atTop, 0 < d (n + 1)
this : ∀ᶠ (n : ℝ) in atTop, x ≤ n
n : ℝ
hn : x ≤ n
e2 : 1 ≤ n / x
⊢ n ≤ n + 1
Tactic:
linarith
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
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)⁻¹
e1 : ∀ᶠ (n : ℝ) in atTop, 0 < d n
e2✝ : ∀ᶠ (n : ℝ) in atTop, 0 < d (n + 1)
this : ∀ᶠ (n : ℝ) in atTop, x ≤ n
n : ℝ
hn : x ≤ n
e2 : 1 ≤ n / x
e3 : n ≤ n + 1
⊢ 0 ≤ n + 1
Tactic:
linarith
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
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 n => d (n + 1) - d n) =O[atTop] fun n => n.log ^ 2
Tactic:
simpa [d, nabla] using (nnabla_mul_log_sq ((2 * π) ^ 2) (by linarith))
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
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)⁻¹
⊢ 0 < x
Tactic:
linarith
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
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
⊢ n.log ≠ 0
Tactic:
have e1 : n ≠ 0 := 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
n : ℝ
hn : 2 ≤ n
e1 : n ≠ 0
⊢ n.log ≠ 0
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
e1 : n ≠ 0
⊢ n.log ≠ 0
Tactic:
have e2 : n ≠ 1 := 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
n : ℝ
hn : 2 ≤ n
e1 : n ≠ 0
e2 : n ≠ 1
⊢ n.log ≠ 0