ZetaNear1BndExact

@[blueprint  (title := "ZetaNear1BndExact")  (statement := /--  There exists a $c>0$ such that for all $1 < \sigma ≤ 2$,  $$  |\zeta(\sigma)| ≤ c/(\sigma-1).  $$  -/)  (proof := /--  Split into two cases, use Lemma \ref{ZetaNear1BndFilter} for $\sigma$ sufficiently small  and continuity on a compact interval otherwise.  -/)  (latexEnv := "lemma")]lemma ZetaNear1BndExact :    ∃ (c : ℝ) (_ : 0 < c), ∀ (σ : ℝ) (_ : σ ∈ Ioc 1 2), ‖ζ σ‖ ≤ c / (σ - 1) := by  have := ZetaNear1BndFilter  rw [Asymptotics.isBigO_iff] at this  obtain ⟨c, U, hU, V, hV, h⟩ := this  obtain ⟨T, hT, T_open, h1T⟩ := mem_nhds_iff.mp hU  obtain ⟨ε, εpos, hε⟩ := Metric.isOpen_iff.mp T_open 1 h1T  simp only [Metric.ball] at hε  replace hε : Ico 1 (1 + ε) ⊆ U := by    refine subset_trans (subset_trans ?_ hε) hT    intro x hx    simp only [mem_Ico] at hx    simp only [dist, abs_lt]    exact ⟨by linarith, by linarith⟩  let W := Icc (1 + ε) 2  have W_compact : IsCompact {ofReal z | z ∈ W} :=    IsCompact.image isCompact_Icc continuous_ofReal  have cont : ContinuousOn ζ {ofReal z | z ∈ W} := by    apply HasDerivAt.continuousOn (f' := ζ')    intro σ hσ    exact (differentiableAt_riemannZeta (by contrapose! hσ; simp [W, hσ, εpos])).hasDerivAt  obtain ⟨C, hC⟩ := IsCompact.exists_bound_of_continuousOn W_compact cont  let C' := max (C + 1) 1  replace hC : ∀ (σ : ℝ), σ ∈ W → ‖ζ σ‖ < C' := by    intro σ hσ    simp only [lt_max_iff, C']    have := hC σ    simp only [mem_setOf_eq, ofReal_inj, exists_eq_right] at this    exact Or.inl <| lt_of_le_of_lt (this hσ) (by norm_num)  have Cpos : 0 < C' := by simp [C']  use max (2 * C') c, (by simp [Cpos])  intro σ ⟨σ_ge, σ_le⟩  by_cases hσ : σ ∈ U ∩ V  · simp only [← h, mem_setOf_eq] at hσ    apply le_trans hσ ?_    norm_cast    have : 0 ≤ 1 / (σ - 1) := by apply one_div_nonneg.mpr; linarith    simp only [Real.norm_eq_abs, abs_eq_self.mpr this, mul_div, mul_one]    exact div_le_div₀ (by simp [Cpos.le]) (by simp) (by linarith) (by rfl)  · replace hσ : σ ∈ W := by      simp only [mem_inter_iff, hV σ_ge, and_true] at hσ      simp only [mem_Icc, σ_le, and_true, W]      contrapose! hσ; exact hε ⟨σ_ge.le, hσ⟩    apply le_trans (hC σ hσ).le ((le_div_iff₀ (by linarith)).mpr ?_)    rw [le_max_iff, mul_comm 2]; exact Or.inl <| mul_le_mul_of_nonneg_left (by linarith) Cpos.le