triv_bound_zeta

theorem triv_bound_zeta :  ∃C ≥ 0, ∀(σ₀ t : ℝ), 1 < σ₀ →    ‖- ζ' (σ₀ + t * I) / ζ (σ₀ + t * I)‖ ≤ (σ₀ - 1)⁻¹ + C := by  let ⟨U, ⟨U_in_nhds, zeta_residue_on_U⟩⟩ := riemannZetaLogDerivResidue  let ⟨open_in_U, ⟨open_in_U_subs_U, open_in_U_is_open, one_in_open_U⟩⟩ :=    mem_nhds_iff.mp U_in_nhds  let ⟨ε₀, ⟨ε_pos, metric_ball_around_1_is_in_U'⟩⟩ :=    EMetric.isOpen_iff.mp open_in_U_is_open (1 : ℂ) one_in_open_U   let ε := if ε₀ = ⊤ then ENNReal.ofReal 1 else ε₀  have O1 : ε ≠ ⊤ := by    unfold ε    by_cases h : ε₀ = ⊤ <;> simp [*]   have metric_ball_around_1_is_in_U :    Metric.eball (1 : ℂ) ε ⊆ U := by      unfold ε      by_cases h : ε₀ = ⊤      · simp only [↓reduceIte, ENNReal.ofReal_one, h]        have T : Metric.eball (1 : ℂ) 1 ⊆ Metric.eball 1 ε₀ := by          simp [*]        exact subset_trans (subset_trans T metric_ball_around_1_is_in_U') open_in_U_subs_U       · simp only [h, ↓reduceIte]        exact subset_trans metric_ball_around_1_is_in_U' open_in_U_subs_U   have O2 : ε ≠ 0 := by    unfold ε    by_cases h : ε₀ = ⊤    · simp [*]    · simp only [↓reduceIte, ne_eq, h]      exact pos_iff_ne_zero.mp ε_pos   let metric_ball_around_1 := Metric.eball (1 : ℂ) ε  let ε_div_two := ε / 2  let boundary := ENNReal.toReal (1 + ε_div_two)   let ⟨bound, ⟨bound_pos, bound_prop⟩⟩ :=      BddAbove.exists_ge zeta_residue_on_U 0   have boundary_geq_one : 1 < boundary := by      unfold boundary      have Z : (1 : ENNReal).toReal = 1 := by rfl      rw [←Z]      have U : ε_div_two ≠ ⊤ := by        refine ENNReal.div_ne_top O1 ?_        simp      simp only [ENNReal.toReal_one, ne_eq, ENNReal.one_ne_top, not_false_eq_true,        ENNReal.toReal_add _ U, lt_add_iff_pos_right, gt_iff_lt]      refine ENNReal.toReal_pos ?_ ?_      · unfold ε_div_two        simp [*]      · exact U   let const : ℝ := bound  let final_const : ℝ := (boundary - 1)⁻¹ + const  have final_const_pos : final_const ≥ 0 := by bound  have const_le_final_const : const ≤ final_const := by bound   /- final const is actually the constant that we will use -/   refine ⟨final_const, final_const_pos, fun σ₀ t σ₀_gt ↦ ?_⟩  have U4 : ENNReal.ofReal 1 ≠ ⊤ := by exact ENNReal.ofReal_ne_top  have Z0 : ε_div_two.toReal < ε.toReal := by    exact ENNReal.toReal_strict_mono O1 <| ENNReal.half_lt_self O2 O1   -- Pick a neighborhood, if in neighborhood then we are good  -- If outside of the neighborhood then use that ζ' / ζ is monotonic  -- and take the bound to be the edge but this will require some more work   by_cases! h : σ₀ ≤ boundary  · have σ₀_in_ball : (↑σ₀ : ℂ) ∈ metric_ball_around_1 := by      unfold metric_ball_around_1      unfold Metric.eball      simp only [mem_setOf_eq]      rw [edist_dist, dist_eq_norm]      norm_cast      have U : 0 ≤ σ₀ - 1 := by linarith      simp only [Real.norm_of_nonneg U, gt_iff_lt]      simp only [ENNReal.ofReal_lt_iff_lt_toReal U O1]      calc        _ ≤ boundary - 1 := by linarith        _ = ENNReal.toReal (1 + ε_div_two) - 1 := rfl        _ = ENNReal.toReal (1 + ε_div_two) - ENNReal.toReal (ENNReal.ofReal 1) := by simp        _ ≤ ENNReal.toReal (1 + ε_div_two - ENNReal.ofReal 1) := ENNReal.le_toReal_sub U4        _ = ENNReal.toReal (ε_div_two) := by          simp only [ENNReal.ofReal_one, ENNReal.addLECancellable_iff_ne, ne_eq,            ENNReal.one_ne_top, not_false_eq_true, AddLECancellable.add_tsub_cancel_left]        _ < ε.toReal := Z0     have σ₀_in_U : (↑σ₀ : ℂ) ∈ (U \ {1}) := by      refine Set.mem_sdiff_singleton.mpr ?_      constructor      · exact metric_ball_around_1_is_in_U σ₀_in_ball      · by_contra a        have U : σ₀ = 1 := by exact ofReal_eq_one.mp a        rw [U] at σ₀_gt        linarith     have bdd := Set.forall_mem_image.mp bound_prop (σ₀_in_U)    simp only [Function.comp_apply, Pi.sub_apply, Pi.neg_apply, Pi.div_apply] at bdd     calc      _ ≤ ‖ζ' σ₀ / ζ σ₀‖ := by        exact dlog_riemannZeta_bdd_on_vertical_lines_generalized σ₀ σ₀ t (σ₀_gt) (by simp)      _ = ‖- ζ' σ₀ / ζ σ₀‖ := by simp only [Complex.norm_div, norm_neg]      _ = ‖(- ζ' σ₀ / ζ σ₀ - (σ₀ - 1)⁻¹) + (σ₀ - 1)⁻¹‖ := by        simp only [Complex.norm_div, norm_neg, ofReal_inv, ofReal_sub, ofReal_one, sub_add_cancel]      _ ≤ ‖(- ζ' σ₀ / ζ σ₀ - (σ₀ - 1)⁻¹)‖ + ‖(σ₀ - 1)⁻¹‖ := by        have Z := norm_add_le (- ζ' σ₀ / ζ σ₀ - (σ₀ - 1)⁻¹) ((σ₀ - 1)⁻¹)        norm_cast at Z      _ ≤ const + ‖(σ₀ - 1)⁻¹‖ := by        have U := add_le_add_left bdd ‖(σ₀ - 1)⁻¹‖        ring_nf at U        ring_nf        norm_cast at U        norm_cast      _ ≤ const + (σ₀ - 1)⁻¹ := by        simp [norm_inv]        have pos : 0 ≤ σ₀ - 1 := by          linarith        simp [abs_of_nonneg pos]      _ = (σ₀ - 1)⁻¹ + const := by        rw [add_comm]      _ ≤ (σ₀ - 1)⁻¹ + final_const := by        simp [const_le_final_const]   · have boundary_in_ball : (↑boundary : ℂ) ∈ metric_ball_around_1 := by      unfold metric_ball_around_1      unfold Metric.eball      simp only [mem_setOf_eq]      rw [edist_dist, dist_eq_norm]      norm_cast      have U : 0 ≤ boundary - 1 := by linarith      simp only [Real.norm_of_nonneg U, gt_iff_lt]      simp only [ENNReal.ofReal_lt_iff_lt_toReal U O1]      calc        _ = ENNReal.toReal (1 + ε_div_two) - 1 := rfl        _ = ENNReal.toReal (1 + ε_div_two) - ENNReal.toReal (ENNReal.ofReal 1) := by simp        _ ≤ ENNReal.toReal (1 + ε_div_two - ENNReal.ofReal 1) := ENNReal.le_toReal_sub U4        _ = ENNReal.toReal (ε_div_two) := by          simp only [ENNReal.ofReal_one, ENNReal.addLECancellable_iff_ne, ne_eq,            ENNReal.one_ne_top, not_false_eq_true, AddLECancellable.add_tsub_cancel_left]        _ < ε.toReal := Z0     have boundary_in_U : (↑boundary : ℂ) ∈ U \ {1} := by      refine Set.mem_sdiff_singleton.mpr ?_      constructor      · exact metric_ball_around_1_is_in_U boundary_in_ball      · by_contra a        norm_cast at a        norm_cast at boundary_geq_one        simp [←a] at boundary_geq_one     have bdd := Set.forall_mem_image.mp bound_prop (boundary_in_U)     calc      _ ≤ ‖ζ' boundary / ζ boundary‖ := by        exact dlog_riemannZeta_bdd_on_vertical_lines_generalized boundary σ₀ t          (boundary_geq_one) (by linarith)      _ = ‖- ζ' boundary / ζ boundary‖ := by simp only [Complex.norm_div, norm_neg]      _ = ‖(- ζ' boundary / ζ boundary - (boundary - 1)⁻¹) + (boundary - 1)⁻¹‖ := by        simp only [Complex.norm_div, norm_neg, ofReal_inv, ofReal_sub, ofReal_one, sub_add_cancel]      _ ≤ ‖(- ζ' boundary / ζ boundary - (boundary - 1)⁻¹)‖ + ‖(boundary - 1)⁻¹‖ := by        have Z := norm_add_le (- ζ' boundary / ζ boundary - (boundary - 1)⁻¹) ((boundary - 1)⁻¹)        norm_cast at Z      _ ≤ const + ‖(boundary - 1)⁻¹‖ := by        have U9 := add_le_add_left bdd ‖(boundary - 1)⁻¹‖        ring_nf at U9        ring_nf        norm_cast at U9        norm_cast        simpa [*] using! U9      _ ≤ const + (boundary - 1)⁻¹ := by        simp [norm_inv]        have pos : 0 ≤ boundary - 1 := by          linarith        simp [abs_of_nonneg pos]      _ = (boundary - 1)⁻¹ + const := by        rw [add_comm]      _ = final_const := by rfl      _ ≤ _ := by bound