ZetaZeroFree

@[blueprint  (title := "ZetaZeroFree")  (statement := /--  There is an $A>0$ so that for $1-A/\log^9 |t| \le \sigma < 1$ and $3 < |t|$,  $$  \zeta(\sigma+it) \ne 0.  $$  -/)  (proof := /-- Apply Lemma \ref{ZetaLowerBnd}. -/)  (latexEnv := "lemma")]lemma ZetaZeroFree :    ∃ (A : ℝ) (_ : A ∈ Ioc 0 (1 / 2)),    ∀ (σ : ℝ)    (t : ℝ) (_ : 3 < |t|)    (_ : σ ∈ Ico (1 - A / (Real.log |t|) ^ 9) 1),    ζ (σ + t * I) ≠ 0 := by  obtain ⟨A, hA, c, hc, h_lower⟩ := ZetaLowerBnd   -- Use the same A for our result  refine ⟨A, hA, ?_⟩   -- Now prove that ζ has no zeros in this region  intro σ t ht hσ h_zero   have := h_lower σ t ht hσ   rw [h_zero, norm_zero] at this   have pos_bound : 0 < c / (Real.log |t|) ^ (7 : ℝ) := by    apply div_pos hc    apply Real.rpow_pos_of_pos    apply Real.log_pos    linarith   linarith