Theorem: HasDerivAtZeta0 (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (ζ₀ N) (ζ₀' N s) s
Tactic:
unfold riemannZeta0 ζ₀'
State after:
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt
    (fun s =>
      ∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ s + -↑N ^ (1 - s) / (1 - s) + -↑N ^ (-s) / 2 +
        s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1))
    (∑ n ∈ Finset.range (N + 1), -1 / ↑n ^ s * ↑(↑n).log +
          (-↑N ^ (1 - s) / (1 - s) ^ 2 + ↑(↑N).log * ↑N ^ (1 - s) / (1 - s)) +
        ↑(↑N).log * ↑N ^ (-s) / 2 +
      ((1 * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1)) +
        s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑x.log))
    s

State before:
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt
    (fun s =>
      ∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ s + -↑N ^ (1 - s) / (1 - s) + -↑N ^ (-s) / 2 +
        s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1))
    (∑ n ∈ Finset.range (N + 1), -1 / ↑n ^ s * ↑(↑n).log +
          (-↑N ^ (1 - s) / (1 - s) ^ 2 + ↑(↑N).log * ↑N ^ (1 - s) / (1 - s)) +
        ↑(↑N).log * ↑N ^ (-s) / 2 +
      ((1 * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1)) +
        s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑x.log))
    s
Tactic:
apply HasDerivAt.sum ?_ |>.add ?_ |>.add ?_ |>.add ?_
State after:
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ ∀ i ∈ Finset.range (N + 1), HasDerivAt (fun x => 1 / ↑i ^ x) (-1 / ↑i ^ s * ↑(↑i).log) s

N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun x => -↑N ^ (1 - x) / (1 - x)) (-↑N ^ (1 - s) / (1 - s) ^ 2 + ↑(↑N).log * ↑N ^ (1 - s) / (1 - s)) s

N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun x => -↑N ^ (-x) / 2) (↑(↑N).log * ↑N ^ (-s) / 2) s

N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun x => x * ∫ (x_1 : ℝ) in Ioi ↑N, (↑⌊x_1⌋ + 1 / 2 - ↑x_1) / ↑x_1 ^ (x + 1))
    ((1 * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1)) +
      s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑x.log)
    s

State before:
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ ∀ i ∈ Finset.range (N + 1), HasDerivAt (fun x => 1 / ↑i ^ x) (-1 / ↑i ^ s * ↑(↑i).log) s
Tactic:
intro n _
State after:
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
n : ℕ
a✝ : n ∈ Finset.range (N + 1)
⊢ HasDerivAt (fun x => 1 / ↑n ^ x) (-1 / ↑n ^ s * ↑(↑n).log) s

State before:
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
n : ℕ
a✝ : n ∈ Finset.range (N + 1)
⊢ HasDerivAt (fun x => 1 / ↑n ^ x) (-1 / ↑n ^ s * ↑(↑n).log) s
Tactic:
convert hasDerivAt_neg' s |>.const_cpow (c := n) (by aesop) using 1
State after:
case h.e'_6
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
n : ℕ
a✝ : n ∈ Finset.range (N + 1)
⊢ (fun x => 1 / ↑n ^ x) = fun x => ↑n ^ (-x)

case h.e'_7
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
n : ℕ
a✝ : n ∈ Finset.range (N + 1)
⊢ -1 / ↑n ^ s * ↑(↑n).log = ↑n ^ (-s) * (↑n).log * -1

State before:
case h.e'_6
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
n : ℕ
a✝ : n ∈ Finset.range (N + 1)
⊢ (fun x => 1 / ↑n ^ x) = fun x => ↑n ^ (-x)

case h.e'_7
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
n : ℕ
a✝ : n ∈ Finset.range (N + 1)
⊢ -1 / ↑n ^ s * ↑(↑n).log = ↑n ^ (-s) * (↑n).log * -1
Tactic:
all_goals (ring_nf; simp [cpow_neg])
State after:
no goals

State before:
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
n : ℕ
a✝ : n ∈ Finset.range (N + 1)
⊢ ↑n ≠ 0 ∨ -s ≠ 0
Tactic:
aesop
State after:
no goals

State before:
case h.e'_7
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
n : ℕ
a✝ : n ∈ Finset.range (N + 1)
⊢ -1 / ↑n ^ s * ↑(↑n).log = ↑n ^ (-s) * (↑n).log * -1
Tactic:
(ring_nf; simp [cpow_neg])
State after:
no goals

State before:
case h.e'_7
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
n : ℕ
a✝ : n ∈ Finset.range (N + 1)
⊢ -1 / ↑n ^ s * ↑(↑n).log = ↑n ^ (-s) * (↑n).log * -1
Tactic:
ring_nf
State after:
case h.e'_7
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
n : ℕ
a✝ : n ∈ Finset.range (N + 1)
⊢ -((↑n ^ s)⁻¹ * ↑(↑n).log) = -(↑n ^ (-s) * (↑n).log)

State before:
case h.e'_7
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
n : ℕ
a✝ : n ∈ Finset.range (N + 1)
⊢ -((↑n ^ s)⁻¹ * ↑(↑n).log) = -(↑n ^ (-s) * (↑n).log)
Tactic:
simp [cpow_neg]
State after:
no goals

State before:
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun x => -↑N ^ (1 - x) / (1 - x)) (-↑N ^ (1 - s) / (1 - s) ^ 2 + ↑(↑N).log * ↑N ^ (1 - s) / (1 - s)) s
Tactic:
convert HasDerivAt.comp (h₂ := fun z ↦ -(N : ℂ) ^ z / z) (h := fun z ↦ 1 - z) (h' := -1)
  (h₂' := ((N : ℂ) ^ (1 - s) / (1 - s) ^ 2 - Real.log (N : ℝ) * (N : ℂ) ^ (1 - s) / (1 - s)))
  (x := s) ?_ ?_ using 1
State after:
case h.e'_7
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ -↑N ^ (1 - s) / (1 - s) ^ 2 + ↑(↑N).log * ↑N ^ (1 - s) / (1 - s) =
    (↑N ^ (1 - s) / (1 - s) ^ 2 - ↑(↑N).log * ↑N ^ (1 - s) / (1 - s)) * -1

case convert_1
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun z => -↑N ^ z / z) (↑N ^ (1 - s) / (1 - s) ^ 2 - ↑(↑N).log * ↑N ^ (1 - s) / (1 - s))
    ((fun z => 1 - z) s)

case convert_2
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun z => 1 - z) (-1) s

State before:
case h.e'_7
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ -↑N ^ (1 - s) / (1 - s) ^ 2 + ↑(↑N).log * ↑N ^ (1 - s) / (1 - s) =
    (↑N ^ (1 - s) / (1 - s) ^ 2 - ↑(↑N).log * ↑N ^ (1 - s) / (1 - s)) * -1

case convert_1
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun z => -↑N ^ z / z) (↑N ^ (1 - s) / (1 - s) ^ 2 - ↑(↑N).log * ↑N ^ (1 - s) / (1 - s))
    ((fun z => 1 - z) s)

case convert_2
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun z => 1 - z) (-1) s
Tactic:
ring_nf
State after:
case convert_1
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun z => -↑N ^ z / z) (↑N ^ (1 - s) / (1 - s) ^ 2 - ↑(↑N).log * ↑N ^ (1 - s) / (1 - s))
    ((fun z => 1 - z) s)

case convert_2
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun z => 1 - z) (-1) s

State before:
case convert_1
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun z => -↑N ^ z / z) (↑N ^ (1 - s) / (1 - s) ^ 2 - ↑(↑N).log * ↑N ^ (1 - s) / (1 - s))
    ((fun z => 1 - z) s)
Tactic:
exact HasDerivAt_cpow_over_var N (by rw [sub_ne_zero]; exact s_ne_one.symm)
State after:
no goals

State before:
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ 1 - s ≠ 0
Tactic:
rw [sub_ne_zero]
State after:
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ 1 ≠ s

State before:
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ 1 ≠ s
Tactic:
exact s_ne_one.symm
State after:
no goals

State before:
case convert_2
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun z => 1 - z) (-1) s
Tactic:
convert hasDerivAt_const s _ |>.sub (hasDerivAt_id _) using 1
State after:
case h.e'_7
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ -1 = 0 - 1

State before:
case h.e'_7
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ -1 = 0 - 1
Tactic:
simp
State after:
no goals

State before:
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun x => -↑N ^ (-x) / 2) (↑(↑N).log * ↑N ^ (-s) / 2) s
Tactic:
convert HasDerivAt_neg_cpow_over2 Npos s using 1
State after:
case h.e'_7
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ ↑(↑N).log * ↑N ^ (-s) / 2 = -(-↑(↑N).log * ↑N ^ (-s)) / 2

State before:
case h.e'_7
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ ↑(↑N).log * ↑N ^ (-s) / 2 = -(-↑(↑N).log * ↑N ^ (-s)) / 2
Tactic:
simp only [natCast_log, neg_mul, neg_neg]
State after:
no goals

State before:
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun x => x * ∫ (x_1 : ℝ) in Ioi ↑N, (↑⌊x_1⌋ + 1 / 2 - ↑x_1) / ↑x_1 ^ (x + 1))
    ((1 * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1)) +
      s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑x.log)
    s
Tactic:
simp_rw [div_cpow_eq_cpow_neg, neg_add, ← sub_eq_add_neg]
State after:
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun x => x * ∫ (x_1 : ℝ) in Ioi ↑N, (↑⌊x_1⌋ + 1 / 2 - ↑x_1) * ↑x_1 ^ (-x - 1))
    ((1 * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1)) +
      s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑x.log)
    s

State before:
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun x => x * ∫ (x_1 : ℝ) in Ioi ↑N, (↑⌊x_1⌋ + 1 / 2 - ↑x_1) * ↑x_1 ^ (-x - 1))
    ((1 * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1)) +
      s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑x.log)
    s
Tactic:
convert hasDerivAt_id s |>.mul <| hasDerivAt_Zeta0Integral Npos reS_pos using 1
State after:
no goals