Complex.cauchySeq_logGammaSeq

lemma cauchySeq_logGammaSeq {z : ℂ} (hz : 0 < z.re) : CauchySeq (logGammaSeq z) := by  apply cauchySeq_of_summable_dist  apply Summable.of_norm_bounded_eventually_nat    (g := fun n => (2 * ‖z‖ + ‖z‖ ^ 2) * (1 / ((n : ℝ) + 1) ^ 2))    (summable_one_div_natCast_add_one_sq.mul_left _)  filter_upwards [eventually_ge_atTop 1, eventually_ge_atTop ⌈2 * ‖z‖⌉₊] with n hn1 hn2  have hnR : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn1  have hn2R : 2 * ‖z‖ ≤ (n : ℝ) := le_trans (Nat.le_ceil _) (by exact_mod_cast hn2)  have hw : ‖z / ((n : ℂ) + 1)‖ = ‖z‖ / ((n : ℝ) + 1) := by    rw [norm_div, norm_natCast_add_one]  have hw2 : ‖z / ((n : ℂ) + 1)‖ ≤ 1 / 2 := by    rw [hw, div_le_iff₀ (by positivity)]    linarith  simp only [Nat.succ_eq_add_one]  rw [Real.norm_of_nonneg dist_nonneg, dist_eq_norm, ← norm_neg, neg_sub,    logGammaSeq_succ_sub hz n]  have key : z * ((Real.log ((n : ℝ) + 1) - Real.log n : ℝ) : ℂ) - log (1 + z / ((n : ℂ) + 1))      = z * ((Real.log ((n : ℝ) + 1) - Real.log n - ((n : ℝ) + 1)⁻¹ : ℝ) : ℂ)        + (z / ((n : ℂ) + 1) - log (1 + z / ((n : ℂ) + 1))) := by    push_cast    ring  rw [key]  have hn0 : (0 : ℝ) < n := by linarith  have hlog_est : |Real.log ((n : ℝ) + 1) - Real.log n - ((n : ℝ) + 1)⁻¹|      ≤ 2 * (1 / ((n : ℝ) + 1) ^ 2) := by    have hdiv : Real.log ((n : ℝ) + 1) - Real.log n = Real.log (((n : ℝ) + 1) / n) :=      (Real.log_div (by positivity) (by positivity)).symm    have l1 : Real.log ((n : ℝ) + 1) - Real.log n ≤ 1 / n := by      rw [hdiv]      have h := Real.log_le_sub_one_of_pos (show (0 : ℝ) < ((n : ℝ) + 1) / n by positivity)      have he : ((n : ℝ) + 1) / n - 1 = 1 / n := by        field_simp        ring      linarith    have l2 : ((n : ℝ) + 1)⁻¹ ≤ Real.log ((n : ℝ) + 1) - Real.log n := by      have h := Real.log_le_sub_one_of_pos (show (0 : ℝ) < (n : ℝ) / ((n : ℝ) + 1) by positivity)      rw [Real.log_div hn0.ne' (by positivity)] at h      have he : (n : ℝ) / ((n : ℝ) + 1) - 1 = -((n : ℝ) + 1)⁻¹ := by        field_simp        ring      rw [he] at h      linarith    have hcomp : 1 / (n : ℝ) - ((n : ℝ) + 1)⁻¹ ≤ 2 * (1 / ((n : ℝ) + 1) ^ 2) := by      have he : 1 / (n : ℝ) - ((n : ℝ) + 1)⁻¹ = 1 / ((n : ℝ) * ((n : ℝ) + 1)) := by        field_simp        ring      rw [he, mul_one_div, div_le_div_iff₀ (by positivity) (by positivity)]      nlinarith    rw [abs_le]    constructor    · have : (0 : ℝ) ≤ 2 * (1 / ((n : ℝ) + 1) ^ 2) := by positivity      linarith    · linarith  calc ‖z * ((Real.log ((n : ℝ) + 1) - Real.log n - ((n : ℝ) + 1)⁻¹ : ℝ) : ℂ)        + (z / ((n : ℂ) + 1) - log (1 + z / ((n : ℂ) + 1)))‖      ≤ ‖z * ((Real.log ((n : ℝ) + 1) - Real.log n - ((n : ℝ) + 1)⁻¹ : ℝ) : ℂ)‖        + ‖z / ((n : ℂ) + 1) - log (1 + z / ((n : ℂ) + 1))‖ := norm_add_le _ _    _ ≤ ‖z‖ * (2 * (1 / ((n : ℝ) + 1) ^ 2)) + ‖z‖ ^ 2 * (1 / ((n : ℝ) + 1) ^ 2) := by        apply _root_.add_le_add        · rw [norm_mul, norm_real, Real.norm_eq_abs]          exact mul_le_mul_of_nonneg_left hlog_est (norm_nonneg z)        · have hlt : ‖z / ((n : ℂ) + 1)‖ < 1 := lt_of_le_of_lt hw2 (by norm_num)          have hb := norm_log_one_add_sub_self_le hlt          rw [← norm_neg, neg_sub]          calc ‖log (1 + z / ((n : ℂ) + 1)) - z / ((n : ℂ) + 1)‖              ≤ ‖z / ((n : ℂ) + 1)‖ ^ 2 * (1 - ‖z / ((n : ℂ) + 1)‖)⁻¹ / 2 := hb            _ ≤ ‖z / ((n : ℂ) + 1)‖ ^ 2 * 2 / 2 := by                have h2 : (1 - ‖z / ((n : ℂ) + 1)‖)⁻¹ ≤ 2 := by                  rw [← one_div]                  have h3 := one_div_le_one_div_of_le (by norm_num : (0 : ℝ) < 1 / 2)                    (by linarith : (1 : ℝ) / 2 ≤ 1 - ‖z / ((n : ℂ) + 1)‖)                  simpa using h3                gcongr            _ = ‖z / ((n : ℂ) + 1)‖ ^ 2 := by ring            _ = ‖z‖ ^ 2 * (1 / ((n : ℝ) + 1) ^ 2) := by                rw [hw, div_pow]                ring    _ = (2 * ‖z‖ + ‖z‖ ^ 2) * (1 / ((n : ℝ) + 1) ^ 2) := by ring