ZetaUpperBnd

@[blueprint  (title := "ZetaUpperBnd")  (statement := /--  For any $s = \sigma + tI \in \C$, $1/2 \le \sigma\le 2, 3 < |t|$  and any $0 < A < 1$ sufficiently small, and $1-A/\log |t| \le \sigma$, we have  $$  |\zeta(s)| \ll \log t.  $$  -/)  (proof := /--  First replace $\zeta(s)$ by $\zeta_0(N,s)$ for $N = \lfloor |t| \rfloor$.  We estimate:  $$  |\zeta_0(N,s)| \ll  \sum_{1\le n \le |t|} |n^{-s}|  +  \frac{- |t|^{1-\sigma}}{|1-s|} + \frac{-|t|^{-\sigma}}{2} +  |t| \cdot |t| ^ {-σ} / σ  $$  $$  \ll  e^A \sum_{1\le n < |t|} n^{-1}  +|t|^{1-\sigma}  $$  ,  where we used Lemma \ref{ZetaBnd_aux2} and Lemma \ref{ZetaBnd_aux1}.  The first term is $\ll \log |t|$.  For the second term, estimate  $$  |t|^{1-\sigma}  \le |t|^{1-(1-A/\log |t|)}  = |t|^{A/\log |t|} \ll 1.  $$  -/)  (latexEnv := "lemma")]lemma ZetaUpperBnd :    ∃ (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| := by  let A := (1 / 2 : ℝ)  let C := Real.exp A * (5 + 8 * 2) -- the 2 comes from ZetaBnd_aux1  refine ⟨A, ⟨by norm_num, by norm_num⟩, C, (by positivity), ?_⟩  intro σ t t_gt ⟨σ_ge, σ_le⟩  obtain ⟨Npos, _, _, _, σPos, neOne⟩ := UpperBnd_aux ⟨by norm_num, by norm_num⟩ t_gt σ_ge  rw [← Zeta0EqZeta Npos (by simp [σPos]) neOne]  apply le_trans (by apply norm_add₄_le) ?_  convert! ZetaUpperBnd' ⟨by norm_num, le_rfl⟩ t_gt ⟨σ_ge, σ_le⟩ using 1; simp