dlog_riemannZeta_bdd_on_vertical_lines_generalized

theorem dlog_riemannZeta_bdd_on_vertical_lines_generalized    (σ₀ σ₁ t : ℝ) (σ₀_gt_one : 1 < σ₀) (σ₀_lt_σ₁ : σ₀ ≤ σ₁) :    ‖(- ζ' (σ₁ + t * I) / ζ (σ₁ + t * I))‖ ≤ ‖ζ' σ₀ / ζ σ₀‖ := by  let s₁ := σ₁ + t * I  have s₁_re_eq_sigma : s₁.re = σ₁ := by    rw [add_re, ofReal_re, mul_I_re, ofReal_im]    ring   have s₀_re_eq_sigma : (↑σ₀ : ℂ).re = σ₀ := by    rw [ofReal_re]   let s₀ := σ₀   have σ₁_gt_one : 1 < σ₁ := by exact lt_of_le_of_lt' σ₀_lt_σ₁ σ₀_gt_one  have s₀_gt_one : 1 < (↑σ₀ : ℂ).re := by exact σ₀_gt_one   have s₁_re_geq_one : 1 < s₁.re := by exact lt_of_lt_of_eq σ₁_gt_one (id (Eq.symm s₁_re_eq_sigma))  rw [← (ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div s₁_re_geq_one)]  unfold LSeries   have summable_von_mangoldt_at_σ₀ : Summable (fun i ↦ LSeries.term (fun n ↦ ↑(Λ n)) σ₀ i) := by    exact ArithmeticFunction.LSeriesSummable_vonMangoldt σ₀_gt_one   have summable_re_von_mangoldt_at_σ₀ :      Summable (fun i ↦ (LSeries.term (fun n ↦ ↑(Λ n)) σ₀ i).re) := by    exact summable_complex_then_summable_real_part (LSeries.term (fun n ↦ ↑(Λ n)) σ₀)      summable_von_mangoldt_at_σ₀   have summable_abs_value : Summable (fun i ↦ ‖LSeries.term (fun n ↦ ↑(Λ n)) s₁ i‖) := by    rw [summable_norm_iff]    exact ArithmeticFunction.LSeriesSummable_vonMangoldt s₁_re_geq_one  apply le_trans <| norm_tsum_le_tsum_norm summable_abs_value  rw [← norm_neg, ← neg_div, ← ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div s₀_gt_one]  unfold LSeries  rw [← re_eq_norm.mpr, re_tsum summable_von_mangoldt_at_σ₀]  · apply Summable.tsum_mono summable_abs_value summable_re_von_mangoldt_at_σ₀    intro n    beta_reduce    apply le_trans <| LSeries.norm_term_le_of_re_le_re (s := σ₀) _ _ _    · rw [re_eq_norm.mpr]      apply LSeries.term_nonneg      exact_mod_cast ArithmeticFunction.vonMangoldt_nonneg    · rwa [s₁_re_eq_sigma, s₀_re_eq_sigma]  · apply tsum_nonneg    intro n    apply LSeries.term_nonneg    exact_mod_cast ArithmeticFunction.vonMangoldt_nonneg