ZetaDerivUpperBnd

@[blueprint  (title := "ZetaDerivUpperBnd")  (statement := /--  For any $s = \sigma + tI \in \C$, $1/2 \le \sigma\le 2, 3 < |t|$,  there is an $A>0$ so that for $1-A/\log t \le \sigma$, we have  $$  |\zeta'(s)| \ll \log^2 t.  $$  -/)  (proof := /--  First replace $\zeta(s)$ by $\zeta_0(N,s)$ for $N = \lfloor |t| \rfloor$.  Differentiating term by term, we get:  $$  \zeta'(s) = -\sum_{1\le n < N} n^{-s} \log n  + \frac{N^{1 - s}}{(1 - s)^2} + \frac{N^{1 - s} \log N} {1 - s}  + \frac{N^{-s}\log N}{2} +  \int_N^\infty \frac{\lfloor x\rfloor + 1/2 - x}{x^{s+1}} \, dx  -s \int_N^\infty \log x \frac{\lfloor x\rfloor + 1/2 - x}{x^{s+1}} \, dx  .  $$  Estimate as before, with an extra factor of $\log |t|$.  -/)  (latexEnv := "lemma")]lemma ZetaDerivUpperBnd :    ∃ (A : ℝ) (_ : A ∈ Ioc 0 (1 / 2)) (C : ℝ) (_ : 0 < C), ∀ (σ : ℝ) (t : ℝ) (_ : 3 < |t|)    (_ : σ ∈ Icc (1 - A / Real.log |t|) 2),    ‖ζ' (σ + t * I)‖ ≤ C * Real.log |t| ^ 2 := by  obtain ⟨A, hA, _, _, _⟩ := ZetaUpperBnd  let C := Real.exp A * 59  refine ⟨A, hA, C, by positivity, ?_⟩  intro σ t t_gt ⟨σ_ge, σ_le⟩  obtain ⟨Npos, N_le_t, _, _, σPos, neOne⟩ := UpperBnd_aux hA t_gt σ_ge  rw [← DerivZeta0EqDerivZeta Npos (by simp [σPos]) neOne]  set N : ℕ := ⌊|t|⌋₊  rw [(HasDerivAtZeta0 Npos (s := σ + t * I) (by simp [σPos]) neOne).deriv]  dsimp only [ζ₀']  rw [← add_assoc]  set aa := ∑ n ∈ Finset.range (N + 1), -1 / (n : ℂ) ^ (σ + t * I) * (Real.log n)  set bb := -(N : ℂ) ^ (1 - (σ + t * I)) / (1 - (σ + t * I)) ^ 2  set cc := (Real.log N) * (N : ℂ) ^ (1 - (σ + t * I)) / (1 - (σ + t * I))  set dd := (Real.log N) * (N : ℂ) ^ (-(σ + t * I)) / 2  set ee := 1 * ∫ x in Ioi (N : ℝ), (⌊x⌋ + 1 / 2 - x) * (x : ℂ) ^ (-(σ + t * I) - 1)  set ff := (σ + t * I) * ∫ x in Ioi (N : ℝ), (⌊x⌋ + 1 / 2 - x) * (x : ℂ) ^ (-(σ + t * I) - 1) * -(Real.log x)  rw [(by ring : aa + (bb + cc) + dd + ee + ff = aa + bb + cc + dd + ee + ff)]  apply le_trans (by apply norm_add₆_le) ?_  convert ZetaDerivUpperBnd' hA t_gt ⟨σ_ge, σ_le⟩