ZetaInvBnd

@[blueprint  (title := "ZetaInvBnd")  (statement := /--  For any $A>0$ sufficiently small, there is a constant $C>0$ so that  whenever $1- A / \log^9 |t| \le \sigma < 1+A/\log^9 |t|$ and $3 < |t|$, we have that:  $$  1/|\zeta(\sigma+it)| \le C \log^7 |t|.  $$  -/)  (proof := /--  Let $\sigma$ be given in the prescribed range, and set $\sigma' := 1+ A / \log^9 |t|$.  Then  $$  |\zeta(\sigma+it)| \ge  |\zeta(\sigma'+it)| - |\zeta(\sigma+it) - \zeta(\sigma'+it)|  \ge  C (\sigma'-1)^{3/4}\log |t|^{-1/4} - C \log^2 |t| (\sigma'-\sigma)  $$  $$  \ge  C A^{3/4} \log |t|^{-7} - C \log^2 |t| (2 A / \log^9 |t|),  $$  where we used Lemma \ref{ZetaInvBound2}  and Lemma \ref{Zeta_diff_Bnd}.  Now by making $A$ sufficiently small (in particular, something like $A = 1/16$ should work), we can guarantee that  $$  |\zeta(\sigma+it)| \ge \frac C 2 (\log |t|)^{-7},  $$  as desired.  -/)  (latexEnv := "lemma")]lemma ZetaInvBnd :    ∃ (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)),    1 / ‖ζ (σ + t * I)‖ ≤ C * (Real.log |t|) ^ (7 : ℝ) := by  obtain ⟨C', C'pos, hC₁⟩ := ZetaInvBound2  obtain ⟨A', hA', C₂, C₂pos, hC₂⟩ := Zeta_diff_Bnd  set C₁ := 1 / C'  let A := min A' <| (1 / 2 : ℝ) * (C₁ / (C₂ * 2)) ^ (4 : ℝ)  have Apos : 0 < A := by have := hA'.1; positivity  have Ale : A ≤ 1 / 2 := by dsimp only [A]; apply min_le_iff.mpr; left; exact hA'.2  set C := (C₁ * A ^ (3 / 4 : ℝ) - C₂ * 2 * A)⁻¹  have Cpos : 0 < C := by    refine ZetaInvBnd_aux2 (by positivity) (by positivity) (by positivity) ?_    apply min_le_right  refine ⟨A, ⟨Apos, by linarith [hA'.2]⟩ , C, Cpos, ?_⟩  intro σ t t_gt hσ  have logt_gt_one := logt_gt_one t_gt.le  have σ_ge : 1 - A / Real.log |t| ≤ σ := by    apply le_trans ?_ hσ.1    suffices A / Real.log |t| ^ 9 ≤ A / Real.log |t| by linarith    exact div_le_div₀ Apos.le (by rfl) (by positivity) <| ZetaInvBnd_aux logt_gt_one  obtain ⟨_, _, neOne⟩ := UpperBnd_aux ⟨Apos, Ale⟩ t_gt σ_ge  set σ' := 1 + A / Real.log |t| ^ 9  have σ'_gt : 1 < σ' := by simp only [σ', lt_add_iff_pos_right]; positivity  have σ'_le : σ' ≤ 2 := by    simp only [σ']    suffices A / Real.log |t| ^ 9 < 1 by linarith    apply div_lt_one (by positivity) |>.mpr    exact lt_trans₄ (by linarith) logt_gt_one <| ZetaInvBnd_aux' logt_gt_one  set s := σ + t * I  set s' := σ' + t * I  by_cases h0 : ‖ζ s‖ ≠ 0  swap  · simp only [ne_eq, not_not] at h0; simp only [h0, div_zero]; positivity  apply div_le_iff₀ (by positivity) |>.mpr <| div_le_iff₀' (by positivity) |>.mp ?_  have pos_aux : 0 < (σ' - 1) := by linarith  calc    _ ≥ ‖ζ s'‖ - ‖ζ s - ζ s'‖ := ?_    _ ≥ C₁ * (σ' - 1) ^ ((3 : ℝ)/ 4) * Real.log |t|  ^ ((-1 : ℝ)/ 4) - C₂ * Real.log |t| ^ 2 * (σ' - σ) := ?_    _ ≥ C₁ * (A / Real.log |t| ^ (9 : ℝ)) ^ ((3 : ℝ)/ 4) * Real.log |t| ^ ((-1 : ℝ)/ 4) - C₂ * Real.log |t| ^ (2 : ℝ) * 2 * A / Real.log |t| ^ (9 : ℝ) := ?_    _ ≥ C₁ * A ^ ((3 : ℝ)/ 4) * Real.log |t| ^ (-7 : ℝ) - C₂ * 2 * A * Real.log |t| ^ (-7 : ℝ) := ?_    _ = (C₁ * A ^ ((3 : ℝ)/ 4) - C₂ * 2 * A) * Real.log |t| ^ (-7 : ℝ) := by ring    _ ≥ _ := ?_  · apply ge_iff_le.mpr    convert norm_sub_norm_le (a := ζ s') (b := ζ s' - ζ s) using 1    · rw [(by simp : ζ s' - ζ s = -(ζ s - ζ s'))]; simp only [norm_neg]    · simp  · apply sub_le_sub    · have := one_div_le ?_ (by positivity) |>.mp <| hC₁ ⟨σ'_gt, σ'_le⟩ t t_gt      · convert this using 1        rw [one_div, mul_inv_rev, mul_comm, mul_inv_rev, mul_comm _ C'⁻¹]        simp only [one_div C', C₁]        congr <;> (rw [← Real.rpow_neg (by linarith), neg_div]); rw [neg_neg]      · apply norm_pos_iff.mpr <| riemannZeta_ne_zero_of_one_lt_re (by simp [σ'_gt])    · rw [(by simp : ζ s - ζ s' = -(ζ s' - ζ s)), norm_neg]      refine hC₂ σ σ' t t_gt ?_ σ'_le <| by rw [Set.mem_Ico] at hσ; exact hσ.2      apply le_trans ?_ hσ.1      rw [tsub_le_iff_right, ← add_sub_right_comm, le_sub_iff_add_le, add_le_add_iff_left]      exact div_le_div₀ hA'.1.le (by simp [A]) (by positivity) <| ZetaInvBnd_aux logt_gt_one  · apply sub_le_sub (by simp only [add_sub_cancel_left, σ']; exact_mod_cast le_rfl) ?_    rw [mul_div_assoc, mul_assoc _ 2 _]    apply mul_le_mul (by exact_mod_cast le_rfl) ?_ (by linarith [hσ.2]) (by positivity)    suffices h : σ' + (1 - A / Real.log |t| ^ 9) ≤ (1 + A / Real.log |t| ^ 9) + σ by      simp only [tsub_le_iff_right]      convert! le_sub_right_of_add_le h using 1; ring_nf; norm_cast; simp    exact add_le_add (by linarith) (by linarith [hσ.1])  · simp_rw [tsub_le_iff_right, div_eq_mul_inv _ (Real.log |t| ^ (9 : ℝ))]    rw [← Real.rpow_neg (by positivity), Real.mul_rpow (by positivity) (by positivity)]    rw [← Real.rpow_mul (by positivity)]    ring_nf    conv => rhs; lhs; rw [mul_assoc, ← Real.rpow_add (by positivity)]    rw [(by ring : C₂ * Real.log |t| ^ (2 : ℝ) * A * Real.log |t| ^ (-9 : ℝ) * 2 = C₂ * (Real.log |t| ^ (2 : ℝ) * Real.log |t| ^ (-9 : ℝ) ) * A * 2)]    rw [← Real.rpow_add (by positivity)]; norm_num; group; exact le_rfl  · apply div_le_iff₀ (by positivity) |>.mpr    conv => rw [mul_assoc]; rhs; rhs; rw [mul_comm C, ← mul_assoc, ← Real.rpow_add (by positivity)]    have := inv_inv C ▸ mul_inv_cancel₀ (a := C⁻¹) (by positivity) |>.symm.le    simpa [C] using this