LogDerivZetaBndUnif

@[blueprint  (title := "LogDerivZetaBndUnif")  (statement := /--  There exist $A, C > 0$ such that  $$|\frac{\zeta'}{\zeta}(\sigma + it)|\leq C \log |t|^9$$  whenever $|t|>3$ and $\sigma > 1 - A/\log |t|^9$.  -/)  (proof := /--  For $\sigma$ close to $1$ use Lemma \ref{LogDerivZetaBnd}, otherwise estimate trivially.  -/)  (latexEnv := "lemma")]lemma LogDerivZetaBndUnif :    ∃ (A : ℝ) (_ : A ∈ Ioc 0 (1 / 2)) (C : ℝ) (_ : 0 < C), ∀ (σ : ℝ) (t : ℝ) (_ : 3 < |t|)    (_ : σ ∈ Ici (1 - A / Real.log |t| ^ 9)), ‖ζ' (σ + t * I) / ζ (σ + t * I)‖ ≤      C * Real.log |t| ^ 9 := by  let ⟨A, pf_A, C, C_pos, ζbd_in⟩ := LogDerivZetaBnd  let ⟨C_triv, ⟨pf_C_triv, ζbd_out⟩⟩ := triv_bound_zeta  have T0 : A > 0 := pf_A.1   have ha : 1 ≤ A⁻¹ := by    simp only [one_div, mem_Ioc, true_and, T0] at pf_A    have U := (inv_le_inv₀ (by positivity) (by positivity)).mpr pf_A    simp only [inv_inv] at U    linarith   refine ⟨A, pf_A, ((1 + C + C_triv) * A⁻¹), (by positivity), fun σ t hyp_t hyp_σ ↦ ?_⟩  have logt_gt' : (1 : ℝ) < Real.log |t| ^ 9 := by    calc      1 < Real.log |t| := logt_gt_one hyp_t.le      _ ≤ (Real.log |t|) ^ 9 := ZetaInvBnd_aux (logt_gt_one hyp_t.le)   have logt_gt'' : (1 : ℝ) < 1 + A / Real.log |t| ^ 9 := by    simp only [lt_add_iff_pos_right, div_pos_iff_of_pos_left, T0]    positivity   have T1 : ∀⦃σ : ℝ⦄, 1 + A / Real.log |t| ^ 9 ≤ σ → 1 < σ := by    intros    linarith   have T2 : ∀⦃σ : ℝ⦄, 1 + A / Real.log |t| ^ 9 ≤ σ → A / Real.log |t| ^ 9 ≤ σ - 1 := by    intro σ' hyp_σ'    calc      A / Real.log |t| ^ 9 = (1 + A / Real.log |t| ^ 9) - 1 := by ring_nf      _ ≤ σ' - 1 := by gcongr    by_cases h : σ ∈ Ico (1 - A / Real.log |t| ^ 9) (1 + A / Real.log |t| ^ 9)  · calc      ‖ζ' (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * Real.log |t| ^ 9 := ζbd_in σ t hyp_t h      _ ≤ ((1 + C + C_triv) * A⁻¹) * Real.log |t| ^ 9 := by          gcongr          · calc              C ≤ 1 + C := by simp only [le_add_iff_nonneg_left, zero_le_one]              _ ≤ (1 + C + C_triv) * 1 := by simp only [mul_one, le_add_iff_nonneg_right]; positivity              _ ≤ (1 + C + C_triv) * A⁻¹ := by gcongr   · simp only [mem_Ico, tsub_le_iff_right, not_and, not_lt, mem_Ici] at h hyp_σ    replace h := h hyp_σ    calc      ‖ζ' (σ + t * I) / ζ (σ + t * I)‖ = ‖-ζ' (σ + t * I) / ζ (σ + t * I)‖ := by simp only [Complex.norm_div,        norm_neg]       _ ≤ (σ - 1)⁻¹ + C_triv := ζbd_out σ t (by exact T1 h)       _ ≤ (A / Real.log |t| ^ 9)⁻¹ + C_triv := by          gcongr          · exact T2 h       _ ≤ (A / Real.log |t| ^ 9)⁻¹ + C_triv * A⁻¹ := by          gcongr          exact le_mul_of_one_le_right pf_C_triv ha       _ ≤ (1 + C_triv) * A⁻¹ * Real.log |t| ^ 9 := by          simp only [inv_div]          ring_nf          gcongr          · simp only [inv_pos, le_mul_iff_one_le_left, T0]            linarith       _ ≤ (1 + C + C_triv) * A⁻¹ * Real.log |t| ^ 9 := by gcongr; simp only [le_add_iff_nonneg_right]; positivity