internlm/Lean-Github huggingface dataset:
Theorem: isBigO_log_mul_add
Proof state before:
case h.e'_7
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
⊢ Real.log = (fun x => (a⁻¹ * x + -b / a).log) ∘ fun x => a * x + b
Tactic:
ext x
Proof state after:
case h.e'_7.h
n : ℕ
A a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b x : ℝ
⊢ x.log = ((fun x => (a⁻¹ * x + -b / a).log) ∘ fun x => a * x + b) x
Theorem: isBigO_log_mul_add
Proof state before:
case h.e'_7.h
n : ℕ
A a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b x : ℝ
⊢ x.log = ((fun x => (a⁻¹ * x + -b / a).log) ∘ fun x => a * x + b) x
Tactic:
field_simp [ha.ne.symm]
Proof state after:
no goals
Theorem: log_isbigo_log_div
Proof state before:
n : ℕ
A a b c d✝ u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
d : ℝ
hb : 0 < d
⊢ (fun n => n.log) =O[atTop] fun n => (n / d).log
Tactic:
convert isBigO_log_mul_add (inv_pos.mpr hb) 0 using 1
Proof state after:
case h.e'_8
n : ℕ
A a b c d✝ u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
d : ℝ
hb : 0 < d
⊢ (fun n => (n / d).log) = fun x => (d⁻¹ * x + 0).log
Theorem: log_isbigo_log_div
Proof state before:
case h.e'_8
n : ℕ
A a b c d✝ u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
d : ℝ
hb : 0 < d
⊢ (fun n => (n / d).log) = fun x => (d⁻¹ * x + 0).log
Tactic:
field_simp
Proof state after:
no goals
Theorem: Asymptotics.IsBigO.add_isLittleO_right
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h : g =o[atTop] f
⊢ f =O[atTop] (f + g)
Tactic:
rw [isLittleO_iff] at h
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ c * ‖f x‖
⊢ f =O[atTop] (f + g)
Theorem: Asymptotics.IsBigO.add_isLittleO_right
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ c * ‖f x‖
⊢ f =O[atTop] (f + g)
Tactic:
specialize h (c := 2⁻¹) (by norm_num)
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
⊢ f =O[atTop] (f + g)
Theorem: Asymptotics.IsBigO.add_isLittleO_right
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
⊢ f =O[atTop] (f + g)
Tactic:
rw [isBigO_iff'']
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
⊢ ∃ c > 0, ∀ᶠ (x : ℝ) in atTop, c * ‖f x‖ ≤ ‖(f + g) x‖
Theorem: Asymptotics.IsBigO.add_isLittleO_right
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
⊢ ∃ c > 0, ∀ᶠ (x : ℝ) in atTop, c * ‖f x‖ ≤ ‖(f + g) x‖
Tactic:
refine ⟨2⁻¹, by norm_num, ?_⟩
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
⊢ ∀ᶠ (x : ℝ) in atTop, 2⁻¹ * ‖f x‖ ≤ ‖(f + g) x‖
Theorem: Asymptotics.IsBigO.add_isLittleO_right
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
⊢ ∀ᶠ (x : ℝ) in atTop, 2⁻¹ * ‖f x‖ ≤ ‖(f + g) x‖
Tactic:
filter_upwards [h] with x h
Proof state after:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h✝ : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
x : ℝ
h : ‖g x‖ ≤ 2⁻¹ * ‖f x‖
⊢ 2⁻¹ * ‖f x‖ ≤ ‖(f + g) x‖
Theorem: Asymptotics.IsBigO.add_isLittleO_right
Proof state before:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h✝ : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
x : ℝ
h : ‖g x‖ ≤ 2⁻¹ * ‖f x‖
⊢ 2⁻¹ * ‖f x‖ ≤ ‖(f + g) x‖
Tactic:
simp at h ⊢
Proof state after:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h✝ : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
x : ℝ
h : |g x| ≤ 2⁻¹ * |f x|
⊢ 2⁻¹ * |f x| ≤ |f x + g x|
Theorem: Asymptotics.IsBigO.add_isLittleO_right
Proof state before:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h✝ : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
x : ℝ
h : |g x| ≤ 2⁻¹ * |f x|
⊢ 2⁻¹ * |f x| ≤ |f x + g x|
Tactic:
calc _ = |f x| - 2⁻¹ * |f x| := by ring
     _ ≤ |f x| - |g x| := by linarith
     _ ≤ |(|f x| - |g x|)| := le_abs_self _
     _ ≤ _ := by rw [← sub_neg_eq_add, ← abs_neg (g x)] ; exact abs_abs_sub_abs_le (f x) (-g x)
Proof state after:
no goals
Theorem: Asymptotics.IsBigO.add_isLittleO_right
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ c * ‖f x‖
⊢ 0 < 2⁻¹
Tactic:
norm_num
Proof state after:
no goals
Theorem: Asymptotics.IsBigO.add_isLittleO_right
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
⊢ 2⁻¹ > 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: Asymptotics.IsBigO.add_isLittleO_right
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h✝ : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
x : ℝ
h : |g x| ≤ 2⁻¹ * |f x|
⊢ 2⁻¹ * |f x| = |f x| - 2⁻¹ * |f x|
Tactic:
ring
Proof state after:
no goals
Theorem: Asymptotics.IsBigO.add_isLittleO_right
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h✝ : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
x : ℝ
h : |g x| ≤ 2⁻¹ * |f x|
⊢ |f x| - 2⁻¹ * |f x| ≤ |f x| - |g x|
Tactic:
linarith
Proof state after:
no goals
Theorem: Asymptotics.IsBigO.add_isLittleO_right
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h✝ : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
x : ℝ
h : |g x| ≤ 2⁻¹ * |f x|
⊢ ||f x| - |g x|| ≤ |f x + g x|
Tactic:
rw [← sub_neg_eq_add, ← abs_neg (g x)]
Proof state after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h✝ : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
x : ℝ
h : |g x| ≤ 2⁻¹ * |f x|
⊢ ||f x| - |(-g x)|| ≤ |f x - -g x|
Theorem: Asymptotics.IsBigO.add_isLittleO_right
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h✝ : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
x : ℝ
h : |g x| ≤ 2⁻¹ * |f x|
⊢ ||f x| - |(-g x)|| ≤ |f x - -g x|
Tactic:
exact abs_abs_sub_abs_le (f x) (-g x)
Proof state after:
no goals
Theorem: Asymptotics.IsBigO.sq
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
α : Type u_1
inst✝ : Preorder α
f g : α → ℝ
h : f =O[atTop] g
⊢ (fun n => f n ^ 2) =O[atTop] fun n => g n ^ 2
Tactic:
simpa [pow_two] using h.mul h
Proof state after:
no goals
Theorem: log_sq_isbigo_mul
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
⊢ (fun x => x.log ^ 2) =O[atTop] fun x => a + (x / b).log ^ 2
Tactic:
apply (log_isbigo_log_div hb).sq.trans
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
⊢ (fun n => (n / b).log ^ 2) =O[atTop] fun x => a + (x / b).log ^ 2
Theorem: log_sq_isbigo_mul
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
⊢ (fun n => (n / b).log ^ 2) =O[atTop] fun x => a + (x / b).log ^ 2
Tactic:
simp_rw [add_comm a]
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
⊢ (fun n => (n / b).log ^ 2) =O[atTop] fun x => (x / b).log ^ 2 + a
Theorem: log_sq_isbigo_mul
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
⊢ (fun n => (n / b).log ^ 2) =O[atTop] fun x => (x / b).log ^ 2 + a
Tactic:
refine IsBigO.add_isLittleO_right <| isLittleO_const_of_tendsto_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
⊢ Tendsto (fun n => (n / b).log ^ 2) atTop atTop
Theorem: log_sq_isbigo_mul
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
⊢ Tendsto (fun n => (n / b).log ^ 2) atTop atTop
Tactic:
exact (tendsto_pow_atTop (two_ne_zero)).comp <| tendsto_log_atTop.comp <| tendsto_id.atTop_div_const hb
Proof state after:
no goals
Theorem: log_add_div_isBigO_log
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
⊢ (fun x => ((x + a) / b).log) =O[atTop] fun x => x.log
Tactic:
convert log_mul_add_isBigO_log (inv_pos.mpr hb) (a / b) using 3
Proof state after:
case h.e'_7.h.h.e'_1
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
hb : 0 < b
x✝ : ℝ
⊢ (x✝ + a) / b = b⁻¹ * x✝ + a / b
Theorem: log_add_div_isBigO_log
Proof state before:
case h.e'_7.h.h.e'_1
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
hb : 0 < b
x✝ : ℝ
⊢ (x✝ + a) / b = b⁻¹ * x✝ + a / b
Tactic:
ring
Proof state after:
no goals
Theorem: log_add_one_sub_log_le
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
⊢ nabla Real.log x ≤ x⁻¹
Tactic:
have l1 : ContinuousOn Real.log (Icc x (x + 1)) := by
  apply continuousOn_log.mono ; intro t ⟨h1, _⟩ ; simp ; 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
l1 : ContinuousOn Real.log (Icc x (x + 1))
⊢ nabla Real.log x ≤ x⁻¹
Theorem: log_add_one_sub_log_le
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
l1 : ContinuousOn Real.log (Icc x (x + 1))
⊢ nabla Real.log x ≤ x⁻¹
Tactic:
have l2 t (ht : t ∈ Ioo x (x + 1)) : HasDerivAt Real.log t⁻¹ t := Real.hasDerivAt_log (by linarith [ht.1])
Proof state after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
l1 : ContinuousOn Real.log (Icc x (x + 1))
l2 : ∀ t ∈ Ioo x (x + 1), HasDerivAt Real.log t⁻¹ t
⊢ nabla Real.log x ≤ x⁻¹
Theorem: log_add_one_sub_log_le
Proof state before:
case intro.intro.intro
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
l1 : ContinuousOn Real.log (Icc x (x + 1))
l2 : ∀ t ∈ Ioo x (x + 1), HasDerivAt Real.log t⁻¹ t
t : ℝ
htx : t⁻¹ = ((x + 1).log - x.log) / (x + 1 - x)
ht1 : x < t
right✝ : t < x + 1
⊢ nabla Real.log x ≤ x⁻¹
Tactic:
simp at htx
Proof state after:
case intro.intro.intro
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
l1 : ContinuousOn Real.log (Icc x (x + 1))
l2 : ∀ t ∈ Ioo x (x + 1), HasDerivAt Real.log t⁻¹ t
t : ℝ
ht1 : x < t
right✝ : t < x + 1
htx : t⁻¹ = (x + 1).log - x.log
⊢ nabla Real.log x ≤ x⁻¹
Theorem: log_add_one_sub_log_le
Proof state before:
case intro.intro.intro
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
l1 : ContinuousOn Real.log (Icc x (x + 1))
l2 : ∀ t ∈ Ioo x (x + 1), HasDerivAt Real.log t⁻¹ t
t : ℝ
ht1 : x < t
right✝ : t < x + 1
htx : t⁻¹ = (x + 1).log - x.log
⊢ nabla Real.log x ≤ x⁻¹
Tactic:
rw [nabla, ← htx, inv_le_inv (by linarith) hx]
Proof state after:
case intro.intro.intro
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
l1 : ContinuousOn Real.log (Icc x (x + 1))
l2 : ∀ t ∈ Ioo x (x + 1), HasDerivAt Real.log t⁻¹ t
t : ℝ
ht1 : x < t
right✝ : t < x + 1
htx : t⁻¹ = (x + 1).log - x.log
⊢ x ≤ t
Theorem: log_add_one_sub_log_le
Proof state before:
case intro.intro.intro
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
l1 : ContinuousOn Real.log (Icc x (x + 1))
l2 : ∀ t ∈ Ioo x (x + 1), HasDerivAt Real.log t⁻¹ t
t : ℝ
ht1 : x < t
right✝ : t < x + 1
htx : t⁻¹ = (x + 1).log - x.log
⊢ x ≤ t
Tactic:
linarith
Proof state after:
no goals
Theorem: log_add_one_sub_log_le
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
⊢ ContinuousOn Real.log (Icc x (x + 1))
Tactic:
apply continuousOn_log.mono
Proof state after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
⊢ Icc x (x + 1) ⊆ {0}ᶜ
Theorem: log_add_one_sub_log_le
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
⊢ Icc x (x + 1) ⊆ {0}ᶜ
Tactic:
intro t ⟨h1, _⟩
Proof state after:
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
t : ℝ
h1 : x ≤ t
right✝ : t ≤ x + 1
⊢ t ∈ {0}ᶜ
Theorem: log_add_one_sub_log_le
Proof state before:
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
t : ℝ
h1 : x ≤ t
right✝ : t ≤ x + 1
⊢ t ∈ {0}ᶜ
Tactic:
simp
Proof state after:
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
t : ℝ
h1 : x ≤ t
right✝ : t ≤ x + 1
⊢ ¬t = 0
Theorem: log_add_one_sub_log_le
Proof state before:
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
t : ℝ
h1 : x ≤ t
right✝ : t ≤ x + 1
⊢ ¬t = 0
Tactic:
linarith
Proof state after:
no goals
Theorem: log_add_one_sub_log_le
Proof state before:
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
l1 : ContinuousOn Real.log (Icc x (x + 1))
t : ℝ
ht : t ∈ Ioo x (x + 1)
⊢ t ≠ 0
Tactic:
linarith [ht.1]
Proof state after:
no goals
Theorem: log_add_one_sub_log_le
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
l1 : ContinuousOn Real.log (Icc x (x + 1))
l2 : ∀ t ∈ Ioo x (x + 1), HasDerivAt Real.log t⁻¹ t
⊢ x < x + 1
Tactic:
linarith
Proof state after:
no goals
Theorem: log_add_one_sub_log_le
Proof state before:
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
l1 : ContinuousOn Real.log (Icc x (x + 1))
l2 : ∀ t ∈ Ioo x (x + 1), HasDerivAt Real.log t⁻¹ t
t : ℝ
ht1 : x < t
right✝ : t < x + 1
htx : t⁻¹ = (x + 1).log - x.log
⊢ 0 < t
Tactic:
linarith
Proof state after:
no goals
Theorem: nabla_log_main
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ nabla Real.log =O[atTop] fun x => 1 / x
Tactic:
apply IsBigO.of_bound 1
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ ∀ᶠ (x : ℝ) in atTop, ‖nabla Real.log x‖ ≤ 1 * ‖1 / x‖
Theorem: nabla_log_main
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ ∀ᶠ (x : ℝ) in atTop, ‖nabla Real.log x‖ ≤ 1 * ‖1 / x‖
Tactic:
filter_upwards [eventually_gt_atTop 0] with x l1
Proof state after:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
l1 : 0 < x
⊢ ‖nabla Real.log x‖ ≤ 1 * ‖1 / x‖
Theorem: nabla_log_main
Proof state before:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
l1 : 0 < x
⊢ ‖nabla Real.log x‖ ≤ 1 * ‖1 / x‖
Tactic:
have l2 : log x ≤ log (x + 1) := log_le_log l1 (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 : ℝ
l1 : 0 < x
l2 : x.log ≤ (x + 1).log
⊢ ‖nabla Real.log x‖ ≤ 1 * ‖1 / x‖
Theorem: nabla_log_main
Proof state before:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
l1 : 0 < x
l2 : x.log ≤ (x + 1).log
⊢ ‖nabla Real.log x‖ ≤ 1 * ‖1 / x‖
Tactic:
simpa [nabla, abs_eq_self.mpr l1.le, abs_eq_self.mpr (sub_nonneg.mpr l2)] using log_add_one_sub_log_le l1
Proof state after:
no goals
Theorem: nabla_log_main
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
l1 : 0 < x
⊢ x ≤ x + 1
Tactic:
linarith
Proof state after:
no goals
Theorem: nabla_log
Proof state before:
n : ℕ
A a b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
b : ℝ
hb : 0 < b
⊢ (nabla fun x => (x / b).log) =O[atTop] fun x => 1 / x
Tactic:
refine EventuallyEq.trans_isBigO ?_ nabla_log_main
Proof state after:
n : ℕ
A a b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
b : ℝ
hb : 0 < b
⊢ (nabla fun x => (x / b).log) =ᶠ[atTop] nabla Real.log
Theorem: nabla_log
Proof state before:
n : ℕ
A a b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
b : ℝ
hb : 0 < b
⊢ (nabla fun x => (x / b).log) =ᶠ[atTop] nabla Real.log
Tactic:
filter_upwards [eventually_gt_atTop 0] with x l2
Proof state after:
case h
n : ℕ
A a b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
b : ℝ
hb : 0 < b
x : ℝ
l2 : 0 < x
⊢ nabla (fun x => (x / b).log) x = nabla Real.log x
Theorem: nabla_log
Proof state before:
case h
n : ℕ
A a b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
b : ℝ
hb : 0 < b
x : ℝ
l2 : 0 < x
⊢ nabla (fun x => (x / b).log) x = nabla Real.log x
Tactic:
rw [nabla, log_div (by linarith) (by linarith), log_div l2.ne.symm (by linarith), nabla]
Proof state after:
case h
n : ℕ
A a b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
b : ℝ
hb : 0 < b
x : ℝ
l2 : 0 < x
⊢ (x + 1).log - b.log - (x.log - b.log) = (x + 1).log - x.log
Theorem: nabla_log
Proof state before:
case h
n : ℕ
A a b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
b : ℝ
hb : 0 < b
x : ℝ
l2 : 0 < x
⊢ (x + 1).log - b.log - (x.log - b.log) = (x + 1).log - x.log
Tactic:
ring
Proof state after:
no goals
Theorem: nabla_log
Proof state before:
n : ℕ
A a b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
b : ℝ
hb : 0 < b
x : ℝ
l2 : 0 < x
⊢ x + 1 ≠ 0
Tactic:
linarith
Proof state after:
no goals
Theorem: nabla_log
Proof state before:
n : ℕ
A a b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
b : ℝ
hb : 0 < b
x : ℝ
l2 : 0 < x
⊢ b ≠ 0
Tactic:
linarith
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
⊢ (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
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)
⊢ (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)
⊢ (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
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)
⊢ (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)
⊢ (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
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
⊢ (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
⊢ (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)
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
⊢ (nabla fun x => x * (a + (x / b).log ^ 2)) =O[atTop] fun x => x.log ^ 2