Zeta_diff_Bnd

@[blueprint  (title := "Zeta-diff-Bnd")  (statement := /--  For any $A>0$ sufficiently small, there is a constant $C>0$ so that  whenever $1- A / \log t \le \sigma_1 < \sigma_2\le 2$ and $3 < |t|$, we have that:  $$  |\zeta (\sigma_2 + it) - \zeta (\sigma_1 + it)|  \le C (\log |t|)^2 (\sigma_2 - \sigma_1).  $$  -/)  (proof := /--  Use Lemma \ref{Zeta_eq_int_derivZeta} and  estimate trivially using Lemma \ref{ZetaDerivUpperBnd}.  -/)  (latexEnv := "lemma")]lemma Zeta_diff_Bnd :    ∃ (A : ℝ) (_ : A ∈ Ioc 0 (1 / 2)) (C : ℝ) (_ : 0 < C), ∀ (σ₁ σ₂ : ℝ) (t : ℝ) (_ : 3 < |t|)    (_ : 1 - A / Real.log |t| ≤ σ₁) (_ : σ₂ ≤ 2) (_ : σ₁ < σ₂),    ‖ζ (σ₂ + t * I) - ζ (σ₁ + t * I)‖ ≤  C * Real.log |t| ^ 2 * (σ₂ - σ₁) := by  obtain ⟨A, hA, C, Cpos, hC⟩ := ZetaDerivUpperBnd  refine ⟨A, hA, C, Cpos, ?_⟩  intro σ₁ σ₂ t t_gt σ₁_ge σ₂_le σ₁_lt_σ₂  have t_ne_zero : t ≠ 0 := by contrapose! t_gt; simp only [t_gt, abs_zero, Nat.ofNat_nonneg]  rw [← Zeta_eq_int_derivZeta t_ne_zero]  convert intervalIntegral.norm_integral_le_of_norm_le_const ?_ using 1  · congr; rw [_root_.abs_of_nonneg (by linarith)]  · intro σ hσ; rw [uIoc_of_le σ₁_lt_σ₂.le, mem_Ioc] at hσ    exact hC σ t t_gt ⟨le_trans σ₁_ge hσ.1.le, le_trans hσ.2 σ₂_le⟩