Theorem: NormDerivZeta0Le (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
N : ℕ
Npos : 0 < N
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ t : ℝ
σ_ge : 1 - A / |t|.log ≤ σ
σpos : 0 < σ
t_gt : 3 < |t|
⊢ let s := ↑σ + ↑t * I;
  ‖deriv (ζ₀ N) s‖ ≤
    4 * (↑N).log *
      (‖∑ 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)‖)
Tactic:
set s := σ + t * I
State after:
N : ℕ
Npos : 0 < N
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ t : ℝ
σ_ge : 1 - A / |t|.log ≤ σ
σpos : 0 < σ
t_gt : 3 < |t|
s : ℂ := ↑σ + ↑t * I
⊢ let s := s;
  ‖deriv (ζ₀ N) s‖ ≤
    4 * (↑N).log *
      (‖∑ 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)‖)

State before:
N : ℕ
Npos : 0 < N
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ t : ℝ
σ_ge : 1 - A / |t|.log ≤ σ
σpos : 0 < σ
t_gt : 3 < |t|
s : ℂ := ↑σ + ↑t * I
⊢ let s := s;
  ‖deriv (ζ₀ N) s‖ ≤
    4 * (↑N).log *
      (‖∑ 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)‖)
Tactic:
sorry
State after:
no goals