internlm/Lean-Github huggingface dataset:
Theorem: quadratic_pos
Proof state before:
n : ℕ
A a✝ b✝ c✝ d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b c x : ℝ
ha : 0 < a
hΔ : discrim a b c < 0
l1 : a * x ^ 2 + b * x + c = a * (x + b / (2 * a)) ^ 2 - discrim a b c / (4 * a)
⊢ 0 < a * x ^ 2 + b * x + c
Tactic:
have l2 : 0 < - discrim a b c := by linarith
Proof state after:
n : ℕ
A a✝ b✝ c✝ d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b c x : ℝ
ha : 0 < a
hΔ : discrim a b c < 0
l1 : a * x ^ 2 + b * x + c = a * (x + b / (2 * a)) ^ 2 - discrim a b c / (4 * a)
l2 : 0 < -discrim a b c
⊢ 0 < a * x ^ 2 + b * x + c
Theorem: quadratic_pos
Proof state before:
n : ℕ
A a✝ b✝ c✝ d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b c x : ℝ
ha : 0 < a
hΔ : discrim a b c < 0
l1 : a * x ^ 2 + b * x + c = a * (x + b / (2 * a)) ^ 2 - discrim a b c / (4 * a)
l2 : 0 < -discrim a b c
⊢ 0 < a * x ^ 2 + b * x + c
Tactic:
rw [l1, sub_eq_add_neg, ← neg_div]
Proof state after:
n : ℕ
A a✝ b✝ c✝ d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b c x : ℝ
ha : 0 < a
hΔ : discrim a b c < 0
l1 : a * x ^ 2 + b * x + c = a * (x + b / (2 * a)) ^ 2 - discrim a b c / (4 * a)
l2 : 0 < -discrim a b c
⊢ 0 < a * (x + b / (2 * a)) ^ 2 + -discrim a b c / (4 * a)
Theorem: quadratic_pos
Proof state before:
n : ℕ
A a✝ b✝ c✝ d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b c x : ℝ
ha : 0 < a
hΔ : discrim a b c < 0
l1 : a * x ^ 2 + b * x + c = a * (x + b / (2 * a)) ^ 2 - discrim a b c / (4 * a)
l2 : 0 < -discrim a b c
⊢ 0 < a * (x + b / (2 * a)) ^ 2 + -discrim a b c / (4 * a)
Tactic:
positivity
Proof state after:
no goals
Theorem: quadratic_pos
Proof state before:
n : ℕ
A a✝ b✝ c✝ d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b c x : ℝ
ha : 0 < a
hΔ : discrim a b c < 0
⊢ a * x ^ 2 + b * x + c = a * (x + b / (2 * a)) ^ 2 - discrim a b c / (4 * a)
Tactic:
field_simp [discrim]
Proof state after:
n : ℕ
A a✝ b✝ c✝ d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b c x : ℝ
ha : 0 < a
hΔ : discrim a b c < 0
⊢ (a * x ^ 2 + b * x + c) * ((2 * a) ^ 2 * (4 * a)) =
    a * (x * (2 * a) + b) ^ 2 * (4 * a) - (2 * a) ^ 2 * (b ^ 2 - 4 * a * c)
Theorem: quadratic_pos
Proof state before:
n : ℕ
A a✝ b✝ c✝ d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b c x : ℝ
ha : 0 < a
hΔ : discrim a b c < 0
⊢ (a * x ^ 2 + b * x + c) * ((2 * a) ^ 2 * (4 * a)) =
    a * (x * (2 * a) + b) ^ 2 * (4 * a) - (2 * a) ^ 2 * (b ^ 2 - 4 * a * c)
Tactic:
ring
Proof state after:
no goals
Theorem: quadratic_pos
Proof state before:
n : ℕ
A a✝ b✝ c✝ d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b c x : ℝ
ha : 0 < a
hΔ : discrim a b c < 0
l1 : a * x ^ 2 + b * x + c = a * (x + b / (2 * a)) ^ 2 - discrim a b c / (4 * a)
⊢ 0 < -discrim a b c
Tactic:
linarith
Proof state after:
no goals
Theorem: pp_pos
Proof state before:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : a ∈ Ioo (-1) 1
x : ℝ
⊢ 0 < pp a x
Tactic:
simp [pp]
Proof state after:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : a ∈ Ioo (-1) 1
x : ℝ
⊢ 0 < a ^ 2 * (x + 1) ^ 2 + (1 - a) * (1 + a)
Theorem: pp_pos
Proof state before:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : a ∈ Ioo (-1) 1
x : ℝ
⊢ 0 < a ^ 2 * (x + 1) ^ 2 + (1 - a) * (1 + a)
Tactic:
have : 0 < 1 - a := by linarith [ha.2]
Proof state after:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : a ∈ Ioo (-1) 1
x : ℝ
this : 0 < 1 - a
⊢ 0 < a ^ 2 * (x + 1) ^ 2 + (1 - a) * (1 + a)
Theorem: pp_pos
Proof state before:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : a ∈ Ioo (-1) 1
x : ℝ
this : 0 < 1 - a
⊢ 0 < a ^ 2 * (x + 1) ^ 2 + (1 - a) * (1 + a)
Tactic:
have : 0 < 1 + a := by linarith [ha.1]
Proof state after:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : a ∈ Ioo (-1) 1
x : ℝ
this✝ : 0 < 1 - a
this : 0 < 1 + a
⊢ 0 < a ^ 2 * (x + 1) ^ 2 + (1 - a) * (1 + a)
Theorem: pp_pos
Proof state before:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : a ∈ Ioo (-1) 1
x : ℝ
this✝ : 0 < 1 - a
this : 0 < 1 + a
⊢ 0 < a ^ 2 * (x + 1) ^ 2 + (1 - a) * (1 + a)
Tactic:
positivity
Proof state after:
no goals
Theorem: pp_pos
Proof state before:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : a ∈ Ioo (-1) 1
x : ℝ
⊢ 0 < 1 - a
Tactic:
linarith [ha.2]
Proof state after:
no goals
Theorem: pp_pos
Proof state before:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : a ∈ Ioo (-1) 1
x : ℝ
this : 0 < 1 - a
⊢ 0 < 1 + a
Tactic:
linarith [ha.1]
Proof state after:
no goals
Theorem: pp_deriv
Proof state before:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a x : ℝ
⊢ HasDerivAt (pp a) (pp' a x) x
Tactic:
simpa using hasDerivAt_id x |>.add_const 1 |>.pow 2 |>.const_mul _ |>.add_const _
Proof state after:
no goals
Theorem: pp_deriv_eq
Proof state before:
n : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
⊢ deriv (pp a) = pp' a
Tactic:
ext x
Proof state after:
case h
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a x : ℝ
⊢ deriv (pp a) x = pp' a x
Theorem: pp_deriv_eq
Proof state before:
case h
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a x : ℝ
⊢ deriv (pp a) x = pp' a x
Tactic:
exact pp_deriv a x |>.deriv
Proof state after:
no goals
Theorem: pp'_deriv
Proof state before:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a x : ℝ
⊢ HasDerivAt (pp' a) (a ^ 2 * 2) x
Tactic:
simpa using hasDerivAt_id x |>.add_const 1 |>.const_mul 2 |>.const_mul (a ^ 2)
Proof state after:
no goals
Theorem: pp'_deriv_eq
Proof state before:
n : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
⊢ deriv (pp' a) = fun x => a ^ 2 * 2
Tactic:
ext x
Proof state after:
case h
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a x : ℝ
⊢ deriv (pp' a) x = a ^ 2 * 2
Theorem: pp'_deriv_eq
Proof state before:
case h
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a x : ℝ
⊢ deriv (pp' a) x = a ^ 2 * 2
Tactic:
exact pp'_deriv a x |>.deriv
Proof state after:
no goals
Theorem: hh_nonneg
Proof state before:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : 0 ≤ t
⊢ 0 ≤ hh a t
Tactic:
dsimp only [hh]
Proof state after:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : 0 ≤ t
⊢ 0 ≤ (t * (1 + (a * t.log) ^ 2))⁻¹
Theorem: hh_nonneg
Proof state before:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : 0 ≤ t
⊢ 0 ≤ (t * (1 + (a * t.log) ^ 2))⁻¹
Tactic:
positivity
Proof state after:
no goals
Theorem: hh_le
Proof state before:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : 0 ≤ t
⊢ |hh a t| ≤ t⁻¹
Tactic:
by_cases h0 : t = 0
Proof state after:
case pos
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : 0 ≤ t
h0 : t = 0
⊢ |hh a t| ≤ t⁻¹

case neg
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : 0 ≤ t
h0 : ¬t = 0
⊢ |hh a t| ≤ t⁻¹
Theorem: hh_le
Proof state before:
case pos
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : 0 ≤ t
h0 : t = 0
⊢ |hh a t| ≤ t⁻¹

case neg
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : 0 ≤ t
h0 : ¬t = 0
⊢ |hh a t| ≤ t⁻¹
Tactic:
simp [hh, h0]
Proof state after:
case neg
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : 0 ≤ t
h0 : ¬t = 0
⊢ |hh a t| ≤ t⁻¹
Theorem: hh_le
Proof state before:
case neg
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : 0 ≤ t
h0 : ¬t = 0
⊢ |hh a t| ≤ t⁻¹
Tactic:
replace ht : 0 < t := lt_of_le_of_ne ht (by tauto)
Proof state after:
case neg
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ |hh a t| ≤ t⁻¹
Theorem: hh_le
Proof state before:
case neg
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ |hh a t| ≤ t⁻¹
Tactic:
unfold hh
Proof state after:
case neg
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ |(t * (1 + (a * t.log) ^ 2))⁻¹| ≤ t⁻¹
Theorem: hh_le
Proof state before:
case neg
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ |(t * (1 + (a * t.log) ^ 2))⁻¹| ≤ t⁻¹
Tactic:
rw [abs_inv, inv_le_inv (by positivity) ht, abs_mul, abs_eq_self.mpr ht.le]
Proof state after:
case neg
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ t ≤ t * |1 + (a * t.log) ^ 2|
Theorem: hh_le
Proof state before:
case neg
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ t ≤ t * |1 + (a * t.log) ^ 2|
Tactic:
convert_to t * 1 ≤ _
Proof state after:
case h.e'_3
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ t = t * 1

case neg.convert_2
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ t * 1 ≤ t * |1 + (a * t.log) ^ 2|
Theorem: hh_le
Proof state before:
case h.e'_3
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ t = t * 1

case neg.convert_2
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ t * 1 ≤ t * |1 + (a * t.log) ^ 2|
Tactic:
simp
Proof state after:
case neg.convert_2
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ t * 1 ≤ t * |1 + (a * t.log) ^ 2|
Theorem: hh_le
Proof state before:
case neg.convert_2
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ t * 1 ≤ t * |1 + (a * t.log) ^ 2|
Tactic:
apply mul_le_mul le_rfl ?_ zero_le_one ht.le
Proof state after:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ 1 ≤ |1 + (a * t.log) ^ 2|
Theorem: hh_le
Proof state before:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ 1 ≤ |1 + (a * t.log) ^ 2|
Tactic:
rw [abs_eq_self.mpr (by positivity)]
Proof state after:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ 1 ≤ 1 + (a * t.log) ^ 2
Theorem: hh_le
Proof state before:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ 1 ≤ 1 + (a * t.log) ^ 2
Tactic:
simp
Proof state after:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ 0 ≤ (a * t.log) ^ 2
Theorem: hh_le
Proof state before:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ 0 ≤ (a * t.log) ^ 2
Tactic:
positivity
Proof state after:
no goals
Theorem: hh_le
Proof state before:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : 0 ≤ t
h0 : ¬t = 0
⊢ 0 ≠ t
Tactic:
tauto
Proof state after:
no goals
Theorem: hh_le
Proof state before:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ 0 < |t * (1 + (a * t.log) ^ 2)|
Tactic:
positivity
Proof state after:
no goals
Theorem: hh_le
Proof state before:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ 0 ≤ 1 + (a * t.log) ^ 2
Tactic:
positivity
Proof state after:
no goals
Theorem: hh_deriv
Proof state before:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : t ≠ 0
⊢ HasDerivAt (hh a) (hh' a t) t
Tactic:
have e1 : t * (1 + (a * log t) ^ 2) ≠ 0 := mul_ne_zero ht (_root_.ne_of_lt (by positivity)).symm
Proof state after:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : t ≠ 0
e1 : t * (1 + (a * t.log) ^ 2) ≠ 0
⊢ HasDerivAt (hh a) (hh' a t) t
Theorem: hh_deriv
Proof state before:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : t ≠ 0
e1 : t * (1 + (a * t.log) ^ 2) ≠ 0
⊢ HasDerivAt (hh a) (hh' a t) t
Tactic:
have l5 : HasDerivAt (fun t : ℝ => log t) t⁻¹ t := Real.hasDerivAt_log ht
Proof state after:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : t ≠ 0
e1 : t * (1 + (a * t.log) ^ 2) ≠ 0
l5 : HasDerivAt (fun t => t.log) t⁻¹ t
⊢ HasDerivAt (hh a) (hh' a t) t
Theorem: hh_deriv
Proof state before:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : t ≠ 0
e1 : t * (1 + (a * t.log) ^ 2) ≠ 0
l5 : HasDerivAt (fun t => t.log) t⁻¹ t
⊢ HasDerivAt (hh a) (hh' a t) t
Tactic:
have l4 : HasDerivAt (fun t : ℝ => a * log t) (a * t⁻¹) t := l5.const_mul _
Proof state after:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : t ≠ 0
e1 : t * (1 + (a * t.log) ^ 2) ≠ 0
l5 : HasDerivAt (fun t => t.log) t⁻¹ t
l4 : HasDerivAt (fun t => a * t.log) (a * t⁻¹) t
⊢ HasDerivAt (hh a) (hh' a t) t
Theorem: hh_deriv
Proof state before:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : t ≠ 0
e1 : t * (1 + (a * t.log) ^ 2) ≠ 0
l5 : HasDerivAt (fun t => t.log) t⁻¹ t
l4 : HasDerivAt (fun t => a * t.log) (a * t⁻¹) t
⊢ HasDerivAt (hh a) (hh' a t) t
Tactic:
have l3 : HasDerivAt (fun t : ℝ => (a * log t) ^ 2) (2 * a ^ 2 * t⁻¹ * log t) t := by
  convert l4.pow 2 using 1 ; ring
Proof state after:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : t ≠ 0
e1 : t * (1 + (a * t.log) ^ 2) ≠ 0
l5 : HasDerivAt (fun t => t.log) t⁻¹ t
l4 : HasDerivAt (fun t => a * t.log) (a * t⁻¹) t
l3 : HasDerivAt (fun t => (a * t.log) ^ 2) (2 * a ^ 2 * t⁻¹ * t.log) t
⊢ HasDerivAt (hh a) (hh' a t) t
Theorem: hh_deriv
Proof state before:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : t ≠ 0
e1 : t * (1 + (a * t.log) ^ 2) ≠ 0
l5 : HasDerivAt (fun t => t.log) t⁻¹ t
l4 : HasDerivAt (fun t => a * t.log) (a * t⁻¹) t
l3 : HasDerivAt (fun t => (a * t.log) ^ 2) (2 * a ^ 2 * t⁻¹ * t.log) t
⊢ HasDerivAt (hh a) (hh' a t) t
Tactic:
have l2 : HasDerivAt (fun t : ℝ => 1 + (a * log t) ^ 2) (2 * a ^ 2 * t⁻¹ * log t) t := l3.const_add _
Proof state after:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : t ≠ 0
e1 : t * (1 + (a * t.log) ^ 2) ≠ 0
l5 : HasDerivAt (fun t => t.log) t⁻¹ t
l4 : HasDerivAt (fun t => a * t.log) (a * t⁻¹) t
l3 : HasDerivAt (fun t => (a * t.log) ^ 2) (2 * a ^ 2 * t⁻¹ * t.log) t
l2 : HasDerivAt (fun t => 1 + (a * t.log) ^ 2) (2 * a ^ 2 * t⁻¹ * t.log) t
⊢ HasDerivAt (hh a) (hh' a t) t
Theorem: hh_deriv
Proof state before:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : t ≠ 0
e1 : t * (1 + (a * t.log) ^ 2) ≠ 0
l5 : HasDerivAt (fun t => t.log) t⁻¹ t
l4 : HasDerivAt (fun t => a * t.log) (a * t⁻¹) t
l3 : HasDerivAt (fun t => (a * t.log) ^ 2) (2 * a ^ 2 * t⁻¹ * t.log) t
l2 : HasDerivAt (fun t => 1 + (a * t.log) ^ 2) (2 * a ^ 2 * t⁻¹ * t.log) t
⊢ HasDerivAt (hh a) (hh' a t) t
Tactic:
have l1 : HasDerivAt (fun t : ℝ => t * (1 + (a * log t) ^ 2))
    (1 + 2 * a ^ 2 * log t + a ^ 2 * log t ^ 2) t := by
  convert (hasDerivAt_id t).mul l2 using 1 ; field_simp ; ring
Proof state after:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : t ≠ 0
e1 : t * (1 + (a * t.log) ^ 2) ≠ 0
l5 : HasDerivAt (fun t => t.log) t⁻¹ t
l4 : HasDerivAt (fun t => a * t.log) (a * t⁻¹) t
l3 : HasDerivAt (fun t => (a * t.log) ^ 2) (2 * a ^ 2 * t⁻¹ * t.log) t
l2 : HasDerivAt (fun t => 1 + (a * t.log) ^ 2) (2 * a ^ 2 * t⁻¹ * t.log) t
l1 : HasDerivAt (fun t => t * (1 + (a * t.log) ^ 2)) (1 + 2 * a ^ 2 * t.log + a ^ 2 * t.log ^ 2) t
⊢ HasDerivAt (hh a) (hh' a t) t
Theorem: hh_deriv
Proof state before:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : t ≠ 0
e1 : t * (1 + (a * t.log) ^ 2) ≠ 0
l5 : HasDerivAt (fun t => t.log) t⁻¹ t
l4 : HasDerivAt (fun t => a * t.log) (a * t⁻¹) t
l3 : HasDerivAt (fun t => (a * t.log) ^ 2) (2 * a ^ 2 * t⁻¹ * t.log) t
l2 : HasDerivAt (fun t => 1 + (a * t.log) ^ 2) (2 * a ^ 2 * t⁻¹ * t.log) t
l1 : HasDerivAt (fun t => t * (1 + (a * t.log) ^ 2)) (1 + 2 * a ^ 2 * t.log + a ^ 2 * t.log ^ 2) t
⊢ HasDerivAt (hh a) (hh' a t) t
Tactic:
convert l1.inv e1 using 1
Proof state after:
case h.e'_7
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : t ≠ 0
e1 : t * (1 + (a * t.log) ^ 2) ≠ 0
l5 : HasDerivAt (fun t => t.log) t⁻¹ t
l4 : HasDerivAt (fun t => a * t.log) (a * t⁻¹) t
l3 : HasDerivAt (fun t => (a * t.log) ^ 2) (2 * a ^ 2 * t⁻¹ * t.log) t
l2 : HasDerivAt (fun t => 1 + (a * t.log) ^ 2) (2 * a ^ 2 * t⁻¹ * t.log) t
l1 : HasDerivAt (fun t => t * (1 + (a * t.log) ^ 2)) (1 + 2 * a ^ 2 * t.log + a ^ 2 * t.log ^ 2) t
⊢ hh' a t = -(1 + 2 * a ^ 2 * t.log + a ^ 2 * t.log ^ 2) / (t * (1 + (a * t.log) ^ 2)) ^ 2
Theorem: hh_deriv
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 t : ℝ
ht : t ≠ 0
e1 : t * (1 + (a * t.log) ^ 2) ≠ 0
l5 : HasDerivAt (fun t => t.log) t⁻¹ t
l4 : HasDerivAt (fun t => a * t.log) (a * t⁻¹) t
l3 : HasDerivAt (fun t => (a * t.log) ^ 2) (2 * a ^ 2 * t⁻¹ * t.log) t
l2 : HasDerivAt (fun t => 1 + (a * t.log) ^ 2) (2 * a ^ 2 * t⁻¹ * t.log) t
l1 : HasDerivAt (fun t => t * (1 + (a * t.log) ^ 2)) (1 + 2 * a ^ 2 * t.log + a ^ 2 * t.log ^ 2) t
⊢ hh' a t = -(1 + 2 * a ^ 2 * t.log + a ^ 2 * t.log ^ 2) / (t * (1 + (a * t.log) ^ 2)) ^ 2
Tactic:
field_simp [hh', hh, pp]
Proof state after:
case h.e'_7
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : t ≠ 0
e1 : t * (1 + (a * t.log) ^ 2) ≠ 0
l5 : HasDerivAt (fun t => t.log) t⁻¹ t
l4 : HasDerivAt (fun t => a * t.log) (a * t⁻¹) t
l3 : HasDerivAt (fun t => (a * t.log) ^ 2) (2 * a ^ 2 * t⁻¹ * t.log) t
l2 : HasDerivAt (fun t => 1 + (a * t.log) ^ 2) (2 * a ^ 2 * t⁻¹ * t.log) t
l1 : HasDerivAt (fun t => t * (1 + (a * t.log) ^ 2)) (1 + 2 * a ^ 2 * t.log + a ^ 2 * t.log ^ 2) t
⊢ -((1 - a) * (1 + a)) + -(a ^ 2 * (t.log + 1) ^ 2) = -(a ^ 2 * t.log ^ 2) + (-(2 * a ^ 2 * t.log) + -1)
Theorem: hh_deriv
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 t : ℝ
ht : t ≠ 0
e1 : t * (1 + (a * t.log) ^ 2) ≠ 0
l5 : HasDerivAt (fun t => t.log) t⁻¹ t
l4 : HasDerivAt (fun t => a * t.log) (a * t⁻¹) t
l3 : HasDerivAt (fun t => (a * t.log) ^ 2) (2 * a ^ 2 * t⁻¹ * t.log) t
l2 : HasDerivAt (fun t => 1 + (a * t.log) ^ 2) (2 * a ^ 2 * t⁻¹ * t.log) t
l1 : HasDerivAt (fun t => t * (1 + (a * t.log) ^ 2)) (1 + 2 * a ^ 2 * t.log + a ^ 2 * t.log ^ 2) t
⊢ -((1 - a) * (1 + a)) + -(a ^ 2 * (t.log + 1) ^ 2) = -(a ^ 2 * t.log ^ 2) + (-(2 * a ^ 2 * t.log) + -1)
Tactic:
ring
Proof state after:
no goals
Theorem: hh_deriv
Proof state before:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : t ≠ 0
⊢ 0 < 1 + (a * t.log) ^ 2
Tactic:
positivity
Proof state after:
no goals
Theorem: hh_deriv
Proof state before:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : t ≠ 0
e1 : t * (1 + (a * t.log) ^ 2) ≠ 0
l5 : HasDerivAt (fun t => t.log) t⁻¹ t
l4 : HasDerivAt (fun t => a * t.log) (a * t⁻¹) t
⊢ HasDerivAt (fun t => (a * t.log) ^ 2) (2 * a ^ 2 * t⁻¹ * t.log) t
Tactic:
convert l4.pow 2 using 1
Proof state after:
case h.e'_7
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : t ≠ 0
e1 : t * (1 + (a * t.log) ^ 2) ≠ 0
l5 : HasDerivAt (fun t => t.log) t⁻¹ t
l4 : HasDerivAt (fun t => a * t.log) (a * t⁻¹) t
⊢ 2 * a ^ 2 * t⁻¹ * t.log = ↑2 * (a * t.log) ^ (2 - 1) * (a * t⁻¹)
Theorem: hh_deriv
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 t : ℝ
ht : t ≠ 0
e1 : t * (1 + (a * t.log) ^ 2) ≠ 0
l5 : HasDerivAt (fun t => t.log) t⁻¹ t
l4 : HasDerivAt (fun t => a * t.log) (a * t⁻¹) t
⊢ 2 * a ^ 2 * t⁻¹ * t.log = ↑2 * (a * t.log) ^ (2 - 1) * (a * t⁻¹)
Tactic:
ring
Proof state after:
no goals
Theorem: hh_deriv
Proof state before:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : t ≠ 0
e1 : t * (1 + (a * t.log) ^ 2) ≠ 0
l5 : HasDerivAt (fun t => t.log) t⁻¹ t
l4 : HasDerivAt (fun t => a * t.log) (a * t⁻¹) t
l3 : HasDerivAt (fun t => (a * t.log) ^ 2) (2 * a ^ 2 * t⁻¹ * t.log) t
l2 : HasDerivAt (fun t => 1 + (a * t.log) ^ 2) (2 * a ^ 2 * t⁻¹ * t.log) t
⊢ HasDerivAt (fun t => t * (1 + (a * t.log) ^ 2)) (1 + 2 * a ^ 2 * t.log + a ^ 2 * t.log ^ 2) t
Tactic:
convert (hasDerivAt_id t).mul l2 using 1
Proof state after:
case h.e'_7
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : t ≠ 0
e1 : t * (1 + (a * t.log) ^ 2) ≠ 0
l5 : HasDerivAt (fun t => t.log) t⁻¹ t
l4 : HasDerivAt (fun t => a * t.log) (a * t⁻¹) t
l3 : HasDerivAt (fun t => (a * t.log) ^ 2) (2 * a ^ 2 * t⁻¹ * t.log) t
l2 : HasDerivAt (fun t => 1 + (a * t.log) ^ 2) (2 * a ^ 2 * t⁻¹ * t.log) t
⊢ 1 + 2 * a ^ 2 * t.log + a ^ 2 * t.log ^ 2 = 1 * (1 + (a * t.log) ^ 2) + _root_.id t * (2 * a ^ 2 * t⁻¹ * t.log)