LogDerivZetaBnd

@[blueprint  (title := "LogDerivZetaBnd")  (statement := /--  There is an $A>0$ so that for $1-A/\log^9 |t| \le \sigma < 1+A/\log^9 |t|$ and $3 < |t|$,  $$  |\frac {\zeta'}{\zeta} (\sigma+it)| \ll \log^9 |t|.  $$  -/)  (proof := /--  Combine the bound on $|\zeta'|$ from Lemma \ref{ZetaDerivUpperBnd} with the  bound on $1/|\zeta|$ from Lemma \ref{ZetaInvBnd}.  -/)  (latexEnv := "lemma")]lemma LogDerivZetaBnd :    ∃ (A : ℝ) (_ : A ∈ Ioc 0 (1 / 2)) (C : ℝ) (_ : 0 < C), ∀ (σ : ℝ) (t : ℝ) (_ : 3 < |t|)    (_ : σ ∈ Ico (1 - A / Real.log |t| ^ 9) (1 + A / Real.log |t| ^ 9)), ‖ζ' (σ + t * I) / ζ (σ + t * I)‖ ≤      C * Real.log |t| ^ 9 := by  obtain ⟨A, hA, C, hC, h⟩ := ZetaInvBnd  obtain ⟨A', hA', C', hC', h'⟩ := ZetaDerivUpperBnd  use min A A', ⟨lt_min hA.1 hA'.1, min_le_of_right_le hA'.2⟩, C * C', mul_pos hC hC'  intro σ t t_gt ⟨σ_ge, σ_lt⟩  have logt_gt : (1 : ℝ) < Real.log |t| := logt_gt_one t_gt.le  have σ_ge' : 1 - A / Real.log |t| ^ 9 ≤ σ := by    apply le_trans (tsub_le_tsub_left ?_ 1) σ_ge    apply div_le_div_of_nonneg_right (min_le_left A A')    exact pow_nonneg (zero_le_one.trans logt_gt.le) _  have σ_ge'' : 1 - A' / Real.log |t| ≤ σ := by    apply le_trans (tsub_le_tsub_left ?_ 1) σ_ge    apply div_le_div₀ hA'.1.le (min_le_right A A') (lt_trans (by norm_num) logt_gt) ?_    exact le_self_pow₀ logt_gt.le (by norm_num)  replace h := h σ t t_gt ⟨σ_ge', by calc    σ < 1 + min A A' / Real.log |t| ^ 9 := σ_lt    _ ≤ 1 + A / Real.log |t| ^ 9 := by gcongr; simp⟩  replace h' := h' σ t t_gt ⟨σ_ge'', by   calc    σ ≤ 1 + min A A' / Real.log |t| ^ 9 := by linarith [σ_lt]     _ ≤ 1 + (1/2) / Real.log |t| ^ 9 := by gcongr; simp [Set.mem_Ioc] at hA' hA ⊢ ; simp [hA.2]     _ ≤ 1 + (1/2) / 1 := by          gcongr          calc            1 ≤ Real.log |t| := by linarith            _ ≤ (Real.log |t|)^9 := Real.self_le_rpow_of_one_le (by linarith) (by linarith)          norm_cast     _ ≤ 2 := by linarith    ⟩  simp only [norm_div]  convert! mul_le_mul h h' (by simp) ?_ using 1 <;> (norm_cast; ring_nf); positivity