Theorem: ZetaSum_aux1φderiv (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
⊢ deriv (fun t => 1 / ↑t ^ s) x = (fun x => -s * ↑x ^ (-(s + 1))) x
Tactic:
let r := -s - 1
State after:
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
⊢ deriv (fun t => 1 / ↑t ^ s) x = (fun x => -s * ↑x ^ (-(s + 1))) x

State before:
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
⊢ deriv (fun t => 1 / ↑t ^ s) x = (fun x => -s * ↑x ^ (-(s + 1))) x
Tactic:
have r_add1_ne_zero : r + 1 ≠ 0 := fun hr ↦ by simp [neg_ne_zero.mpr s_ne_zero, r] at hr
State after:
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
⊢ deriv (fun t => 1 / ↑t ^ s) x = (fun x => -s * ↑x ^ (-(s + 1))) x

State before:
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
⊢ deriv (fun t => 1 / ↑t ^ s) x = (fun x => -s * ↑x ^ (-(s + 1))) x
Tactic:
have r_ne_neg1 : r ≠ -1 := fun hr ↦ (hr ▸ r_add1_ne_zero) <| by norm_num
State after:
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
⊢ deriv (fun t => 1 / ↑t ^ s) x = (fun x => -s * ↑x ^ (-(s + 1))) x

State before:
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
⊢ deriv (fun t => 1 / ↑t ^ s) x = (fun x => -s * ↑x ^ (-(s + 1))) x
Tactic:
have hasDeriv := hasDerivAt_ofReal_cpow xpos.ne' r_ne_neg1
State after:
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
⊢ deriv (fun t => 1 / ↑t ^ s) x = (fun x => -s * ↑x ^ (-(s + 1))) x

State before:
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
⊢ deriv (fun t => 1 / ↑t ^ s) x = (fun x => -s * ↑x ^ (-(s + 1))) x
Tactic:
have := hasDeriv.deriv ▸ deriv_const_mul (-s) (hasDeriv).differentiableAt
State after:
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
this : deriv (fun y => -s * (↑y ^ (r + 1) / (r + 1))) x = -s * ↑x ^ r
⊢ deriv (fun t => 1 / ↑t ^ s) x = (fun x => -s * ↑x ^ (-(s + 1))) x

State before:
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
this : deriv (fun y => -s * (↑y ^ (r + 1) / (r + 1))) x = -s * ↑x ^ r
⊢ deriv (fun t => 1 / ↑t ^ s) x = (fun x => -s * ↑x ^ (-(s + 1))) x
Tactic:
convert this using 2
State after:
case h.e'_2.h.e'_6
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
this : deriv (fun y => -s * (↑y ^ (r + 1) / (r + 1))) x = -s * ↑x ^ r
⊢ (fun t => 1 / ↑t ^ s) = fun y => -s * (↑y ^ (r + 1) / (r + 1))

case h.e'_3.h.e'_6
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
this : deriv (fun y => -s * (↑y ^ (r + 1) / (r + 1))) x = -s * ↑x ^ r
⊢ ↑x ^ (-(s + 1)) = ↑x ^ r

State before:
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
hr : r + 1 = 0
⊢ False
Tactic:
simp [neg_ne_zero.mpr s_ne_zero, r] at hr
State after:
no goals

State before:
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
hr : r = -1
⊢ -1 + 1 = 0
Tactic:
norm_num
State after:
no goals

State before:
case h.e'_2.h.e'_6
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
this : deriv (fun y => -s * (↑y ^ (r + 1) / (r + 1))) x = -s * ↑x ^ r
⊢ (fun t => 1 / ↑t ^ s) = fun y => -s * (↑y ^ (r + 1) / (r + 1))
Tactic:
ext y
State after:
case h.e'_2.h.e'_6.h
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
this : deriv (fun y => -s * (↑y ^ (r + 1) / (r + 1))) x = -s * ↑x ^ r
y : ℝ
⊢ 1 / ↑y ^ s = -s * (↑y ^ (r + 1) / (r + 1))

State before:
case h.e'_2.h.e'_6.h
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
this : deriv (fun y => -s * (↑y ^ (r + 1) / (r + 1))) x = -s * ↑x ^ r
y : ℝ
⊢ 1 / ↑y ^ s = -s * (↑y ^ (r + 1) / (r + 1))
Tactic:
by_cases y_zero : (y : ℂ) = 0
State after:
case pos
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
this : deriv (fun y => -s * (↑y ^ (r + 1) / (r + 1))) x = -s * ↑x ^ r
y : ℝ
y_zero : ↑y = 0
⊢ 1 / ↑y ^ s = -s * (↑y ^ (r + 1) / (r + 1))

case neg
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
this : deriv (fun y => -s * (↑y ^ (r + 1) / (r + 1))) x = -s * ↑x ^ r
y : ℝ
y_zero : ¬↑y = 0
⊢ 1 / ↑y ^ s = -s * (↑y ^ (r + 1) / (r + 1))

State before:
case pos
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
this : deriv (fun y => -s * (↑y ^ (r + 1) / (r + 1))) x = -s * ↑x ^ r
y : ℝ
y_zero : ↑y = 0
⊢ 1 / ↑y ^ s = -s * (↑y ^ (r + 1) / (r + 1))
Tactic:
simp only [y_zero, ofReal_zero, ne_eq, s_ne_zero, not_false_eq_true, zero_cpow, div_zero,
r_add1_ne_zero, zero_div, mul_zero]
State after:
no goals

State before:
case neg
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
this : deriv (fun y => -s * (↑y ^ (r + 1) / (r + 1))) x = -s * ↑x ^ r
y : ℝ
y_zero : ¬↑y = 0
⊢ 1 / ↑y ^ s = -s * (↑y ^ (r + 1) / (r + 1))
Tactic:
have : (y : ℂ) ^ s ≠ 0 := fun hy ↦ y_zero ((cpow_eq_zero_iff _ _).mp hy).1
State after:
case neg
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
this✝ : deriv (fun y => -s * (↑y ^ (r + 1) / (r + 1))) x = -s * ↑x ^ r
y : ℝ
y_zero : ¬↑y = 0
this : ↑y ^ s ≠ 0
⊢ 1 / ↑y ^ s = -s * (↑y ^ (r + 1) / (r + 1))

State before:
case neg
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
this✝ : deriv (fun y => -s * (↑y ^ (r + 1) / (r + 1))) x = -s * ↑x ^ r
y : ℝ
y_zero : ¬↑y = 0
this : ↑y ^ s ≠ 0
⊢ 1 / ↑y ^ s = -s * (↑y ^ (r + 1) / (r + 1))
Tactic:
field_simp [r, mul_assoc, ← Complex.cpow_add]
State after:
no goals

State before:
case h.e'_3.h.e'_6
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
this : deriv (fun y => -s * (↑y ^ (r + 1) / (r + 1))) x = -s * ↑x ^ r
⊢ ↑x ^ (-(s + 1)) = ↑x ^ r
Tactic:
ring_nf
State after:
no goals