Complex.exists_norm_digamma_le_log

theorem exists_norm_digamma_le_log {a b : ℝ} (ha : 0 < a) :    ∃ C : ℝ, 0 < C ∧ ∀ z : ℂ, a ≤ z.re → z.re ≤ b →      ‖digamma z‖ ≤ C * Real.log (|z.im| + 2) := by  set c : ℝ := min a 1 with hc_def  have hc : 0 < c := lt_min ha one_pos  have hc1 : c ≤ 1 := min_le_right _ _  have hlog2 : 0 < Real.log 2 := Real.log_pos (by norm_num)  set D : ℝ := |Real.eulerMascheroniConstant| + 2 / c + (|b| + 2) / c with hD_def  have hD0 : 0 ≤ D := by positivity  refine ⟨D / Real.log 2 + 2 / c, ?_, fun z hza hzb => ?_⟩  · have h1 : 0 ≤ D / Real.log 2 := div_nonneg hD0 hlog2.le    have h2 : 0 < 2 / c := by positivity    linarith  have hre : 0 < z.re := lt_of_lt_of_le ha hza  have hzc : c ≤ z.re := le_trans (min_le_left _ _) hza  have hb0 : 0 < b := lt_of_lt_of_le hre hzb  have hpoles : ∀ n : ℕ, z ≠ -(n : ℂ) := by    intro n h    rw [h] at hre    simp only [neg_re, natCast_re] at hre    have : (0 : ℝ) ≤ n := Nat.cast_nonneg n    linarith  have hsum : HasSum (fun n : ℕ => ((n : ℂ) + 1)⁻¹ - (z + n)⁻¹)      (digamma z + Real.eulerMascheroniConstant) := by    have h := hasSum_digamma hpoles    have e : (fun n : ℕ => 1 / ((n : ℂ) + 1) - 1 / ((n : ℂ) + z))        = fun m : ℕ => ((m : ℂ) + 1)⁻¹ - (z + m)⁻¹ := by      funext m      rw [one_div, one_div, add_comm (m : ℂ) z]    rwa [e] at h  -- the splitting index  set N : ℕ := ⌈|z.im|⌉₊ + 1 with hN_def  have him0 : (0 : ℝ) ≤ |z.im| := abs_nonneg _  have hN1 : 1 ≤ N := Nat.le_add_left 1 _  have hN1R : (1 : ℝ) ≤ (N : ℝ) := by exact_mod_cast hN1  have hNpos : (0 : ℝ) < (N : ℝ) := by linarith  have hNim : |z.im| ≤ (N : ℝ) := by    rw [hN_def]    push_cast    have := Nat.le_ceil |z.im|    linarith  have hNle : (N : ℝ) ≤ |z.im| + 2 := by    rw [hN_def]    push_cast    have := Nat.ceil_lt_add_one him0    linarith  set L : ℝ := Real.log (|z.im| + 2) with hL_def  have hL2 : Real.log 2 ≤ L := by    rw [hL_def]    exact Real.log_le_log (by norm_num) (by linarith)  -- summability of the norm series and its majorant  have hmaj : Summable (fun m : ℕ => (‖z‖ + 1) / (c * ((m : ℝ) + 1) ^ 2)) := by    refine (summable_one_div_natCast_add_one_sq.mul_left ((‖z‖ + 1) / c)).congr fun m => ?_    rw [mul_one_div, div_div]  have hnormsum : Summable (fun n : ℕ => ‖((n : ℂ) + 1)⁻¹ - (z + n)⁻¹‖) :=    Summable.of_nonneg_of_le (fun n => norm_nonneg _)      (fun n => norm_inv_add_one_sub_inv_le hc hc1 hzc (le_refl ‖z‖) n) hmaj  -- head estimate: the first `N` terms contribute at most a multiple of `log`  have hhead : ∑ n ∈ Finset.range N, ‖((n : ℂ) + 1)⁻¹ - (z + n)⁻¹‖      ≤ 2 / c + 2 / c * L := by    calc ∑ n ∈ Finset.range N, ‖((n : ℂ) + 1)⁻¹ - (z + n)⁻¹‖        ≤ ∑ n ∈ Finset.range N, 2 / (c * ((n : ℝ) + 1)) :=          Finset.sum_le_sum fun n _ => norm_inv_add_one_sub_inv_le' hc hc1 hzc n      _ = 2 / c * ∑ n ∈ Finset.range N, ((n : ℝ) + 1)⁻¹ := by          rw [Finset.mul_sum]          exact Finset.sum_congr rfl fun n _ => by rw [← div_div, div_eq_mul_inv]      _ = 2 / c * ((harmonic N : ℚ) : ℝ) := by rw [sum_inv_natCast_add_one_real]      _ ≤ 2 / c * (1 + Real.log N) :=          mul_le_mul_of_nonneg_left (harmonic_le_one_add_log N) (by positivity)      _ ≤ 2 / c * (1 + L) := by          have h3 : Real.log N ≤ L := by            rw [hL_def]            exact Real.log_le_log hNpos hNle          exact mul_le_mul_of_nonneg_left (by linarith) (by positivity)      _ = 2 / c + 2 / c * L := by ring  -- tail estimate: past `N` the series contributes a bounded amount  have hshift_norm : Summable (fun i : ℕ => ‖(((i + N : ℕ) : ℂ) + 1)⁻¹ - (z + (i + N : ℕ))⁻¹‖) :=    (summable_nat_add_iff N).mpr hnormsum  have hshift_maj : Summable (fun i : ℕ => (‖z‖ + 1) / (c * (((i + N : ℕ) : ℝ) + 1) ^ 2)) :=    (summable_nat_add_iff N).mpr hmaj  have htail : ‖∑' i : ℕ, ((((i + N : ℕ) : ℂ) + 1)⁻¹ - (z + (i + N : ℕ))⁻¹)‖      ≤ (b + 2) / c := by    have hz_norm : ‖z‖ ≤ b + |z.im| := by      have h1 : ‖z‖ ≤ |z.re| + |z.im| := norm_le_abs_re_add_abs_im z      have h2 : |z.re| = z.re := abs_of_pos hre      linarith    have hN_key : ‖z‖ + 1 ≤ (b + 2) * (N : ℝ) := by      have h1 : b * 1 ≤ b * (N : ℝ) := mul_le_mul_of_nonneg_left hN1R hb0.le      have h2 : (b + 2) * (N : ℝ) = b * N + 2 * N := by ring      rw [h2]      linarith    calc ‖∑' i : ℕ, ((((i + N : ℕ) : ℂ) + 1)⁻¹ - (z + (i + N : ℕ))⁻¹)‖        ≤ ∑' i : ℕ, ‖(((i + N : ℕ) : ℂ) + 1)⁻¹ - (z + (i + N : ℕ))⁻¹‖ :=          norm_tsum_le_tsum_norm hshift_norm      _ ≤ ∑' i : ℕ, (‖z‖ + 1) / (c * (((i + N : ℕ) : ℝ) + 1) ^ 2) :=          hshift_norm.tsum_le_tsum            (fun i => norm_inv_add_one_sub_inv_le hc hc1 hzc (le_refl ‖z‖) (i + N)) hshift_maj      _ = (‖z‖ + 1) / c * ∑' i : ℕ, 1 / (((i + N : ℕ) : ℝ) + 1) ^ 2 := by          rw [← tsum_mul_left]          exact tsum_congr fun i => by rw [mul_one_div, div_div]      _ ≤ (‖z‖ + 1) / c * (N : ℝ)⁻¹ :=          mul_le_mul_of_nonneg_left (tsum_one_div_natCast_add_add_one_sq_le hN1)            (by positivity)      _ = ((‖z‖ + 1) * (N : ℝ)⁻¹) / c := by ring      _ ≤ (b + 2) / c := by          have h2 : (‖z‖ + 1) * (N : ℝ)⁻¹ ≤ b + 2 := by            rw [← div_eq_mul_inv, div_le_iff₀ hNpos]            linarith          gcongr  -- split the series and assemble  have hsplit : (∑ n ∈ Finset.range N, (((n : ℂ) + 1)⁻¹ - (z + n)⁻¹))      + ∑' i : ℕ, ((((i + N : ℕ) : ℂ) + 1)⁻¹ - (z + (i + N : ℕ))⁻¹)      = ∑' n : ℕ, (((n : ℂ) + 1)⁻¹ - (z + n)⁻¹) :=    hsum.summable.sum_add_tsum_nat_add N  have h5 : ‖∑' n : ℕ, (((n : ℂ) + 1)⁻¹ - (z + n)⁻¹)‖      ≤ (2 / c + 2 / c * L) + (b + 2) / c := by    rw [← hsplit]    refine le_trans (norm_add_le _ _) ?_    exact _root_.add_le_add (le_trans (norm_sum_le _ _) hhead) htail  have hdig_eq : digamma z = (∑' n : ℕ, (((n : ℂ) + 1)⁻¹ - (z + n)⁻¹))      - (Real.eulerMascheroniConstant : ℂ) := by    rw [hsum.tsum_eq]    ring  have h7 : ‖digamma z‖      ≤ |Real.eulerMascheroniConstant| + ((2 / c + 2 / c * L) + (b + 2) / c) := by    rw [hdig_eq]    refine le_trans (norm_sub_le _ _) ?_    have h8 : ‖((Real.eulerMascheroniConstant : ℝ) : ℂ)‖ = |Real.eulerMascheroniConstant| := by      rw [norm_real, Real.norm_eq_abs]    rw [h8]    linarith [h5]  -- absorb the constants into the logarithm  have habs : D ≤ D / Real.log 2 * L := by    calc D = D / Real.log 2 * Real.log 2 := by field_simp      _ ≤ D / Real.log 2 * L :=          mul_le_mul_of_nonneg_left hL2 (div_nonneg hD0 hlog2.le)  have hb_abs : (b + 2) / c ≤ (|b| + 2) / c := by    gcongr    exact le_abs_self b  have hexpand : (D / Real.log 2 + 2 / c) * L = D / Real.log 2 * L + 2 / c * L := by ring  rw [hexpand]  linarith [h7, habs, hb_abs]