LogDerivZetaBdd_of_Re_ge_three_halves

lemma LogDerivZetaBdd_of_Re_ge_three_halves :    ∃ C, ∀ (s : ℂ), 3/2 ≤ s.re → ‖deriv riemannZeta s / riemannZeta s‖ ≤ C := by  have h_sum_converges : Summable (fun n : ℕ ↦ vonMangoldt n / (n : ℝ) ^ (3 / 2 : ℝ)) := by    have h_summable : Summable (fun n : ℕ ↦ (Real.log n : ℝ) / (n : ℝ) ^ (3 / 2 : ℝ)) := by      obtain ⟨C, hC_pos, hC⟩ : ∃ C > 0, ∀ n : ℕ, n ≥ 2 → Real.log n ≤ C * (n : ℝ) ^ (1/4 : ℝ) := by        use 4, by grind, fun n hn ↦ by          have := Real.log_le_sub_one_of_pos (by positivity : 0 < (n : ℝ) ^ (1/4 : ℝ))          rw [Real.log_rpow (by positivity)] at this          nlinarith [Real.rpow_pos_of_pos (by positivity : 0 < (n : ℝ)) (1/4 : ℝ)]      have hBound : ∀ n : ℕ, n ≥ 2 →          (Real.log n : ℝ) / (n : ℝ) ^ (3 / 2 : ℝ) ≤ C / (n : ℝ) ^ (5 / 4 : ℝ) := fun n hn ↦ by        rw [div_le_div_iff₀ (by positivity) (by positivity)]        convert mul_le_mul_of_nonneg_right (hC n hn)          (by positivity : 0 ≤ (n : ℝ) ^ (5 / 4 : ℝ)) using 1        rw [mul_assoc, ← Real.rpow_add (by positivity)]        grind      rw [← summable_nat_add_iff 2]      exact Summable.of_nonneg_of_le        (fun n ↦ div_nonneg (Real.log_nonneg (by grind))          (Real.rpow_nonneg (Nat.cast_nonneg _) _))        (fun n ↦ hBound _ (by grind))        (Summable.mul_left _ <| by simpa using summable_nat_add_iff 2 |>.2 <|          Real.summable_one_div_nat_rpow.2 <| by grind)    refine .of_nonneg_of_le (fun n ↦ ?_) (fun n ↦ ?_) h_summable    · exact div_nonneg (by exact_mod_cast ArithmeticFunction.vonMangoldt_nonneg)        (by positivity)    · rcases eq_or_ne n 0 with (rfl | hn) <;>        simp_all [ArithmeticFunction.vonMangoldt]      field_simp      split_ifs      · exact Real.log_le_log (Nat.cast_pos.mpr (Nat.minFac_pos _))          (Nat.cast_le.mpr (Nat.minFac_le (Nat.pos_of_ne_zero hn)))      · exact Real.log_nonneg (Nat.one_le_cast.mpr (Nat.pos_of_ne_zero hn))  have h_log_deriv_sum : ∀ s : ℂ, 3 / 2 ≤ s.re →      deriv riemannZeta s / riemannZeta s = -∑' n : ℕ, (vonMangoldt n : ℂ) / (n : ℂ) ^ s := by    intro s hs; have h := LogDerivativeDirichlet s (by grind); linear_combination -h  have h_triangle : ∀ s : ℂ,      ‖∑' n : ℕ, (vonMangoldt n : ℂ) / (n : ℂ) ^ s‖ ≤        ∑' n : ℕ, ‖(vonMangoldt n : ℂ) / (n : ℂ) ^ s‖ := fun s ↦ by    by_cases h : Summable fun n ↦ (ArithmeticFunction.vonMangoldt n : ℂ) / (n : ℂ) ^ s    · exact norm_tsum_le_tsum_norm h.norm    · simp only [tsum_eq_zero_of_not_summable h, norm_zero]      exact tsum_nonneg fun _ ↦ by positivity  have h_norm_summand : ∀ s : ℂ, 3 / 2 ≤ s.re → ∀ n : ℕ,      ‖(vonMangoldt n : ℂ) / (n : ℂ) ^ s‖ ≤ (vonMangoldt n : ℝ) / (n : ℝ) ^ (3 / 2 : ℝ) := by    intro s hs n    by_cases hn : n = 0 <;> simp_all [Complex.norm_cpow_of_ne_zero]    ring_nf; norm_num    rw [abs_of_nonneg ArithmeticFunction.vonMangoldt_nonneg]    exact mul_le_mul_of_nonneg_left (inv_anti₀ (by positivity)      (Real.rpow_le_rpow_of_exponent_le (mod_cast Nat.one_le_iff_ne_zero.mpr hn) hs))      ArithmeticFunction.vonMangoldt_nonneg  refine ⟨∑' n : ℕ, (ArithmeticFunction.vonMangoldt n : ℝ) / (n : ℝ) ^ (3 / 2 : ℝ),    fun s hs ↦ ?_⟩  have hSum : Summable fun n ↦ ‖(vonMangoldt n : ℂ) / (n : ℂ) ^ s‖ :=    Summable.of_nonneg_of_le (fun n ↦ by positivity)      (fun n ↦ h_norm_summand s hs n) h_sum_converges  simpa [neg_div, h_log_deriv_sum s hs] using (h_triangle s).trans    (hSum.tsum_le_tsum (fun n ↦ h_norm_summand s hs n) h_sum_converges)