ZetaNoZerosInBox

@[blueprint  (title := "ZetaNoZerosInBox")  (statement := /--  For any $T>0$, there is a constant $\sigma<1$ so that  $$  \zeta(\sigma'+it) \ne 0  $$  for all $|t| \leq T$ and $\sigma' \ge \sigma$.  -/)  (proof := /--  Assume not. Then there is a sequence $|t_n| \le T$ and $\sigma_n \to 1$ so that  $\zeta(\sigma_n + it_n) = 0$.  By compactness, there is a subsequence $t_{n_k} \to t_0$ along which  $\zeta(\sigma_{n_k} + it_{n_k}) = 0$.  If $t_0\ne0$, use the continuity of $\zeta$ to get that $\zeta(1 + it_0) = 0$;  this is a contradiction.  If $t_0=0$, $\zeta$ blows up near $1$, so can't be zero nearby.  -/)  (latexEnv := "lemma")]lemma ZetaNoZerosInBox (T : ℝ) :    ∃ (σ : ℝ) (_ : σ < 1), ∀ (t : ℝ) (_ : |t| ≤ T)    (σ' : ℝ) (_ : σ' ≥ σ), ζ (σ' + t * I) ≠ 0 := by  by_contra! h  have hn (n : ℕ) := h (1 - 1 / (n + 1)) (sub_lt_self _ (by positivity))   have : ∃ (tn : ℕ → ℝ) (σn : ℕ → ℝ), (∀ n, σn n ≤ 1) ∧    (∀ n, (1 : ℝ) - 1 / (n + 1) ≤ σn n) ∧ (∀ n, |tn n| ≤ T) ∧    (∀ n, ζ (σn n + tn n * I) = 0) := by    choose t ht σ' hσ' hζ using hn    refine ⟨t, σ', ?_, hσ', ht, hζ⟩    intro n    by_contra! hσn    have := riemannZeta_ne_zero_of_one_lt_re (s := σ' n + t n * I)    simp only [add_re, ofReal_re, mul_re, I_re, mul_zero, ofReal_im, I_im, mul_one, sub_self,      add_zero, ne_eq] at this    exact this hσn (hζ n)   choose t σ' hσ'_le hσ'_ge ht hζ using this   have σTo1 : Filter.Tendsto σ' Filter.atTop (𝓝 1) := by    use sub_zero (1: ℝ)▸tendsto_order.2 ⟨fun A B=>? _,fun A B=>?_⟩    · apply (((tendsto_inv_atTop_nhds_zero_nat.comp        (Filter.tendsto_add_atTop_nat (1))).congr (by norm_num)).const_sub 1).eventually_const_lt          B|>.mono (hσ'_ge ·|>.trans_lt')    · norm_num[(hσ'_le _).trans_lt, B.trans_le']   have : ∃ (t₀ : ℝ) (subseq : ℕ → ℕ),      Filter.Tendsto (t ∘ subseq) Filter.atTop (𝓝 t₀) ∧      Filter.Tendsto subseq Filter.atTop Filter.atTop := by    refine (isCompact_Icc.isSeqCompact fun and => abs_le.1 (ht and)).imp fun and ⟨x, A, B, _⟩ => ?_    use A, by omega, B.tendsto_atTop   obtain ⟨t₀, subseq, tTendsto, subseqTendsto⟩ := this   have σTo1 : Filter.Tendsto (σ' ∘ subseq) Filter.atTop (𝓝 1) :=    σTo1.comp subseqTendsto   have (n : ℕ) : ζ (σ' (subseq n) + I * (t (subseq n))) = 0 := by    convert hζ (subseq n) using 3    ring   have ToOneT0 : Filter.Tendsto (fun n ↦ (σ' (subseq n) : ℂ) + Complex.I * (t (subseq n))) Filter.atTop      (𝓝[≠]((1 : ℂ) + I * t₀)) := by    simp_rw [tendsto_nhdsWithin_iff, Function.comp_def] at tTendsto ⊢    constructor    · exact (σTo1.ofReal.add (tTendsto.ofReal.const_mul _)).trans (by simp)    · filter_upwards with n      apply ne_of_apply_ne ζ      rw [this]      apply Ne.symm      apply riemannZeta_ne_zero_of_one_le_re      simp only [add_re, one_re, mul_re, I_re, ofReal_re, zero_mul, I_im, ofReal_im, mul_zero,        sub_self, add_zero, le_refl]   by_cases ht₀ : t₀ = 0  · have ZetaBlowsUp : ∀ᶠ s in 𝓝[≠](1 : ℂ), ‖ζ s‖ ≥ 1 := by      simp_all only [ge_iff_le, one_div, tsub_le_iff_right, Function.comp_def, ofReal_zero,        mul_zero, add_zero, norm_eq_sqrt_real_inner, Complex.inner, mul_re, conj_re, conj_im,        mul_neg, sub_neg_eq_add, Real.one_le_sqrt, eventually_nhdsWithin_iff, mem_compl_iff,        mem_singleton_iff]      contrapose! h      simp_all only [ne_eq]      delta abs at*      exfalso      simp_rw [Metric.nhds_basis_ball.frequently_iff]at*      choose! I A B using h      choose a s using exists_seq_strictAnti_tendsto (0: ℝ)      apply ((isCompact_closedBall _ _).isSeqCompact        fun and=>(A _ (s.2.1 and)).le.trans (s.2.2.bddAbove_range.some_mem ⟨and, rfl⟩)).elim      simp only [Metric.mem_ball, dist_eq_norm_sub] at A      refine fun and ⟨a, H, S, M⟩=> ?_      refine absurd (tendsto_nhds_unique M (tendsto_sub_nhds_zero_iff.1        (( squeeze_zero_norm fun and=>le_of_lt (A _ (s.2.1 _) ) )          (s.2.2.comp S.tendsto_atTop)))) fun and=>?_      norm_num[*,Function.comp_def] at M      have:=@riemannZeta_residue_one      use one_ne_zero (tendsto_nhds_unique (this.comp (tendsto_nhdsWithin_iff.2        ⟨ M,.of_forall (by norm_num[*])⟩)) ( squeeze_zero_norm ?_          ((M.sub_const 1).norm.trans (by rw [sub_self,norm_zero]))))      use fun and =>.trans (norm_mul_le_of_le ↑(le_rfl) (Complex.norm_def _▸Real.sqrt_le_one.mpr        (B ↑_ (s.2.1 ↑_)).right.le)) (by rw [mul_one])     have ZetaNonZ : ∀ᶠ s in 𝓝[≠](1 : ℂ), ζ s ≠ 0 := by      filter_upwards [ZetaBlowsUp]      intro s hs hfalse      rw [hfalse] at hs      simp only [norm_zero, ge_iff_le] at hs      linarith     rw [ht₀] at ToOneT0    simp only [ofReal_zero, mul_zero, add_zero] at ToOneT0    rcases (ToOneT0.eventually ZetaNonZ).exists with ⟨n, hn⟩    exact hn (this n)   · have zetaIsZero : ζ (1 + Complex.I * t₀) = 0 := by      have cont := @ZetaCont      use isClosed_singleton.isSeqClosed        this        (.comp          (cont.continuousAt.comp (eventually_ne_nhds (by field_simp; simp [ht₀])).mono            fun and=>.intro ⟨⟩)          (ToOneT0.trans (inf_le_left)))     exact riemannZeta_ne_zero_of_one_le_re (s := 1 + I * t₀) (by simp) zetaIsZero