Theorem: hh_deriv (PrimeNumberTheoremAnd/Wiener.lean)

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
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

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
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

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 _
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

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
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

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 _
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

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
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

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
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

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]
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)

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
State after:
no goals

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
State after:
no goals

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
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⁻¹)

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
State after:
no goals

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
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)

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
⊢ 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)
Tactic:
field_simp
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 + (a * t.log) ^ 2 + 2 * a ^ 2 * t.log

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
⊢ 1 + 2 * a ^ 2 * t.log + a ^ 2 * t.log ^ 2 = 1 + (a * t.log) ^ 2 + 2 * a ^ 2 * t.log
Tactic:
ring
State after:
no goals