ZetaInvBound2

@[blueprint  (title := "ZetaInvBound2")  (statement := /--  For $\sigma>1$ (and $\sigma \le 2$),  $$  1/|\zeta(\sigma+it)| \ll (\sigma-1)^{-3/4}(\log |t|)^{1/4},  $$  as $|t|\to\infty$.  -/)  (proof := /--  Combine Lemma \ref{ZetaInvBound1} with the bounds in Lemmata \ref{ZetaNear1BndExact} and  \ref{ZetaUpperBnd}.  -/)  (latexEnv := "lemma")]lemma ZetaInvBound2 :    ∃ C > 0, ∀ {σ : ℝ} (_ : σ ∈ Ioc 1 2) (t : ℝ) (_ : 3 < |t|),    1 / ‖ζ (σ + t * I)‖ ≤ C * (σ - 1) ^ (-(3 : ℝ) / 4) * (Real.log |t|) ^ ((1 : ℝ) / 4) := by  obtain ⟨A, ha, C, hC, h⟩ := ZetaUpperBnd  obtain ⟨c, hc, h_inv⟩ := ZetaNear1BndExact  refine ⟨(2 * C) ^ ((1 : ℝ)/ 4) * c ^ ((3 : ℝ)/ 4), by positivity, ?_⟩  intro σ hσ t t_gt  obtain ⟨σ_gt, σ_le⟩ := hσ  have ht' : 3 < |2 * t| := by simp only [abs_mul, Nat.abs_ofNat]; linarith  have hnezero: ((σ - 1) / c) ^ (-3 / 4 : ℝ) ≠ 0 := by    have : (σ - 1) / c ≠ 0 := ne_of_gt <| div_pos (by linarith) hc    contrapose! this    rwa [Real.rpow_eq_zero (div_nonneg (by linarith) hc.le) (by norm_num)] at this  calc    _ ≤ ‖‖ζ σ‖ ^ (3 / 4 : ℝ) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4 : ℝ)‖ := ?_    _ ≤ ‖((σ - 1) / c) ^ (-3 / 4 : ℝ) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4 : ℝ)‖ := ?_    _ ≤ ‖((σ - 1) / c) ^ (-3 / 4 : ℝ) * C ^ (1 / 4 : ℝ) * (Real.log |2 * t|) ^ (1 / 4 : ℝ)‖ := ?_    _ ≤ ‖((σ - 1) / c) ^ (-3 / 4 : ℝ) * C ^ (1 / 4 : ℝ) * (Real.log (|t| ^ 2)) ^ (1 / 4 : ℝ)‖ := ?_    _ = ‖((σ - 1)) ^ (-3 / 4 : ℝ) * c ^ (3 / 4 : ℝ) * (C ^ (1 / 4 : ℝ) * (Real.log (|t| ^ 2)) ^ (1 / 4 : ℝ))‖ := ?_    _ = ‖((σ - 1)) ^ (-3 / 4 : ℝ) * c ^ (3 / 4 : ℝ) * ((2 * C) ^ (1 / 4 : ℝ) * Real.log |t| ^ (1 / 4 : ℝ))‖ := ?_    _ = _ := ?_  · simp only [norm_mul]    convert ZetaInvBound1 σ_gt using 2    <;> exact abs_eq_self.mpr <| Real.rpow_nonneg (norm_nonneg _) _  · have bnd1: ‖ζ σ‖ ^ (3 / 4 : ℝ) ≤ ((σ - 1) / c) ^ (-(3 : ℝ) / 4) := by      have : ((σ - 1) / c) ^ (-(3 : ℝ) / 4) = (((σ - 1) / c) ^ (-1 : ℝ)) ^ (3 / 4 : ℝ) := by        rw [← Real.rpow_mul ?_]        · ring_nf        · exact div_nonneg (by linarith) hc.le      rw [this]      apply Real.rpow_le_rpow (by simp [norm_nonneg]) ?_ (by norm_num)      convert! h_inv σ ⟨σ_gt, σ_le⟩ using 1; simp [Real.rpow_neg_one, inv_div]    simp only [norm_mul]    apply (mul_le_mul_iff_left₀ ?_).mpr    · convert! bnd1 using 1      · exact abs_eq_self.mpr <| Real.rpow_nonneg (norm_nonneg _) _      · exact abs_eq_self.mpr <| Real.rpow_nonneg (div_nonneg (by linarith) hc.le) _    · apply lt_iff_le_and_ne.mpr ⟨(by simp), ?_⟩      have : ζ (↑σ + 2 * ↑t * I) ≠ 0 := by        apply riemannZeta_ne_zero_of_one_le_re (by simp [σ_gt.le])      symm; exact fun h2 ↦ this (by simpa using h2)  · replace h := h σ (2 * t) (by simpa using ht') ⟨?_, σ_le⟩    · have : 0 ≤ Real.log |2 * t| := Real.log_nonneg (by linarith)      conv => rhs; rw [mul_assoc, ← Real.mul_rpow hC.le this]      rw [norm_mul, norm_mul]      conv => rhs; rhs; rw [Real.norm_rpow_of_nonneg <| mul_nonneg hC.le this]      conv => lhs; rhs; rw [Real.norm_rpow_of_nonneg <| norm_nonneg _]      apply (mul_le_mul_iff_right₀ ?_).mpr      · apply Real.rpow_le_rpow (norm_nonneg _) ?_ (by norm_num)        convert h using 1        · simp        · rw [Real.norm_eq_abs, abs_eq_self.mpr <| mul_nonneg hC.le this]      · simpa only [Real.norm_eq_abs, abs_pos]    · linarith [(div_nonneg ha.1.le (Real.log_nonneg (by linarith)) : 0 ≤ A / Real.log |2 * t|)]  · simp only [Real.log_abs, norm_mul]    apply (mul_le_mul_iff_right₀ ?_).mpr    · rw [← Real.log_abs, Real.norm_rpow_of_nonneg <| Real.log_nonneg (by linarith)]      have : 1 ≤ |(|t| ^ 2)| := by        simp only [_root_.sq_abs, _root_.abs_pow, one_le_sq_iff_one_le_abs]        linarith      conv => rhs; rw [← Real.log_abs, Real.norm_rpow_of_nonneg <| Real.log_nonneg this]      apply Real.rpow_le_rpow (abs_nonneg _) ?_ (by norm_num)      · rw [Real.norm_eq_abs, abs_eq_self.mpr <| Real.log_nonneg (by linarith)]        rw [abs_eq_self.mpr <| Real.log_nonneg this, abs_mul, Real.log_abs, Nat.abs_ofNat]        apply Real.log_le_log (mul_pos (by norm_num) (by linarith)) (by nlinarith)    · apply mul_pos (abs_pos.mpr hnezero) (abs_pos.mpr ?_)      have : C ≠ 0 := ne_of_gt hC      contrapose! this; rwa [Real.rpow_eq_zero (by linarith) (by norm_num)] at this  · have : (-3 : ℝ) / 4 = -((3 : ℝ)/ 4) := by norm_num    simp only [norm_mul, mul_eq_mul_right_iff, this, ← mul_assoc]; left; left    conv => lhs; rw [Real.div_rpow (by linarith) hc.le, Real.rpow_neg hc.le, div_inv_eq_mul, norm_mul]  · simp only [Real.log_pow, Nat.cast_ofNat, norm_mul, Real.norm_eq_abs]    congr! 1    rw [Real.mul_rpow (by norm_num) hC.le, Real.mul_rpow (by norm_num) <|        Real.log_nonneg (by linarith), abs_mul, abs_mul, ← mul_assoc, mul_comm _ |2 ^ (1 / 4)|]  · simp only [norm_mul, Real.norm_eq_abs]    have : (2 * C) ^ ((1 : ℝ)/ 4) * c ^ ((3 : ℝ)/ 4) =      |(2 * C) ^ ((1 : ℝ)/ 4) * c ^ ((3 : ℝ)/ 4)| := by      rw [abs_eq_self.mpr (by apply mul_nonneg <;> (apply Real.rpow_nonneg; linarith))]    rw [this, abs_mul, abs_eq_self.mpr (by apply Real.rpow_nonneg; linarith), abs_eq_self.mpr (by positivity),      abs_eq_self.mpr (by positivity), abs_eq_self.mpr (by apply Real.rpow_nonneg (Real.log_nonneg (by linarith)))]    ring_nf