LiDigammaLeft.lean

Declarations

Source

/-
NguyenRH1/LiDigammaLeft.lean — tier ii′ sub-stage 5e-ii (D-068 §1 C2):
the two digamma bounds feeding the circle estimate of ii′-5e-v.

* §1 `tsum_one_div_sub_telescope`: ∑'ₙ (1/(n+N) − 1/(n+N+1)) = 1/N
  (partial-sum telescope + squeeze).
* §2 `norm_digamma_le_of_two_le_re`: ‖ψ(w)‖ ≤ 20·log(2+‖w‖) for
  re w ≥ 2, |im w| ≤ 5 — the Weierstrass-series route (Zeta23
  `DigammaSeries.digamma_series`): Σ'_n w/((n+1)(w+n+1)) split at
  N = ⌈re w⌉₊ (head via the harmonic bound `harmonic_le_one_add_log`,
  tail via §1's telescope); the positive-integer case via `digamma_one`
  + the recurrence (`digamma_natCast_eq`).
* §3 (C): `digamma_recip_sum_le` — the separated reciprocal sum bound
  Σ_{j<m} ‖w+j‖⁻¹ ≤ 2/c + 2 + 2·log m for dist(w, −ℕ) ≥ c (V-split).
* §4 (A): `norm_digamma_le_of_dist_nat` — the near-axis left-plane bound
  for re w ≤ 2, dist(w,−ℕ) ≥ c (recurrence `digamma_add_natCast` + §3 +
  the landing-zone bound via §2 or StirlingVert).
* §5 (G): `logDeriv_Gammaℝ_eq` — logDeriv ΓR s = −(log π)/2 + ½ψ(s/2)
  for im s ≠ 0 (the m-fold shift: `gamma_mul_prod` + the EventuallyEq
  machinery of 5d).

Archive references: D-068 §1 (C2) + §7, journal-025/026.
-/
import Mathlib
import Zeta23.GammaFacts.Series
import Zeta23.GammaFacts.StirlingVert
import NguyenRH1.LiReflect
import NguyenRH1.LiTrivialZeros

open Zeta23 Complex Filter Topology MeasureTheory
open scoped Nat

noncomputable section

namespace NguyenRH1

/-! ## 1. The telescoping tail -/

/-- The partial sums of the telescoping series. -/
theorem sum_range_one_div_sub (N M : ℕ) :
    ∑ n ∈ Finset.range M, ((1 : ℝ) / ((n : ℝ) + N) - 1 / ((n : ℝ) + N + 1))
      = 1 / (N : ℝ) - 1 / ((M : ℝ) + N) := by
  have h := Finset.sum_range_sub' (fun n : ℕ => (1 : ℝ) / ((n : ℝ) + N)) M
  rw [Nat.cast_zero, zero_add] at h
  rw [← h]
  apply Finset.sum_congr rfl
  intro n _
  push_cast
  ring_nf

/-- **The telescoping tail, HasSum form**. -/
theorem hasSum_one_div_sub_telescope (N : ℕ) (hN : 1 ≤ N) :
    HasSum (fun n : ℕ => (1 : ℝ) / ((n : ℝ) + N) - 1 / ((n : ℝ) + N + 1))
      (1 / (N : ℝ)) := by
  have hNR : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hN
  have hnonneg : ∀ n : ℕ, (0 : ℝ) ≤ 1 / ((n : ℝ) + N) - 1 / ((n : ℝ) + N + 1) := by
    intro n
    have h1 : (0 : ℝ) < (n : ℝ) + N := by
      have h2 : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg n
      linarith [hNR, h2]
    have h3 : 1 / ((n : ℝ) + N + 1) ≤ 1 / ((n : ℝ) + N) :=
      one_div_le_one_div_of_le h1 (by linarith)
    linarith [h3]
  have hlim0 : Tendsto (fun M : ℕ => (1 : ℝ) / ((M : ℝ) + N)) atTop (𝓝 0) := by
    have h1 : Tendsto (fun M : ℕ => (1 : ℝ) / ((M : ℝ) + 1)) atTop (𝓝 0) :=
      tendsto_one_div_add_atTop_nhds_zero_nat
    refine squeeze_zero (f := fun M : ℕ => (1 : ℝ) / ((M : ℝ) + N))
      (g := fun M : ℕ => (1 : ℝ) / ((M : ℝ) + 1)) ?_ ?_ h1
    · intro M
      positivity
    · intro M
      apply one_div_le_one_div_of_le (by positivity)
      have hN1R : (1 : ℝ) ≤ (N : ℝ) := by exact_mod_cast hN
      linarith [hN1R]
  have hlim : Tendsto (fun M : ℕ => (1 : ℝ) / (N : ℝ) - 1 / ((M : ℝ) + N)) atTop
      (𝓝 (1 / (N : ℝ))) := by
    have h := hlim0.const_sub (1 / (N : ℝ))
    rwa [sub_zero] at h
  rw [hasSum_iff_tendsto_nat_of_nonneg hnonneg]
  convert hlim using 1
  ext M
  exact sum_range_one_div_sub N M

/-- **The telescoping tail**: ∑'ₙ (1/(n+N) − 1/(n+N+1)) = 1/N for N ≥ 1. -/
theorem tsum_one_div_sub_telescope (N : ℕ) (hN : 1 ≤ N) :
    ∑' n : ℕ, ((1 : ℝ) / ((n : ℝ) + N) - 1 / ((n : ℝ) + N + 1)) = 1 / (N : ℝ) :=
  (hasSum_one_div_sub_telescope N hN).tsum_eq

/-! ## 2. The right-half-plane bound (B) -/

/-- ψ at positive integers: ψ(n) = −γ + H_{n−1} for n ≥ 1. -/
theorem digamma_natCast_eq (n : ℕ) (hn : 1 ≤ n) :
    Complex.digamma (n : ℂ)
      = -(Real.eulerMascheroniConstant : ℂ) + ((harmonic (n - 1) : ℚ) : ℂ) := by
  induction n with
  | zero => omega
  | succ k ih =>
    rcases eq_or_ne k 0 with hk | hk
    · subst hk
      simp [Complex.digamma_one, harmonic]
    · have hk1 : 1 ≤ k := Nat.one_le_iff_ne_zero.mpr hk
      have h1 := ih hk1
      have hside : ∀ m : ℕ, (k : ℂ) ≠ -(m : ℂ) := by
        intro m h
        have hre := congrArg Complex.re h
        simp [Complex.neg_re, Complex.natCast_re] at hre
        have hmk : (1 : ℝ) ≤ (k : ℝ) := by exact_mod_cast hk1
        have hm0 : (0 : ℝ) ≤ (m : ℝ) := by positivity
        linarith
      have h2 := Complex.digamma_apply_add_one (k : ℂ) hside
      rw [show ((k + 1 : ℕ) : ℂ) = (k : ℂ) + 1 by push_cast; ring, h2, h1]
      have hharm : ((harmonic (k + 1 - 1) : ℚ) : ℂ)
          = ((harmonic (k - 1) : ℚ) : ℂ) + ((k : ℝ) : ℂ)⁻¹ := by
        have h3 : k + 1 - 1 = k := by omega
        rw [h3]
        have h4 : harmonic k = harmonic (k - 1) + ((k : ℚ))⁻¹ := by
          conv_lhs => rw [show k = (k - 1) + 1 by omega]
          rw [harmonic, Finset.sum_range_succ]
          have h5 : k - 1 + 1 = k := by omega
          rw [h5]
          rw [harmonic]
        rw [h4]
        push_cast
        ring
      rw [hharm]
      push_cast
      ring

/-- The digamma-series majorant g n = ‖w‖/((n+1)(re w+n+1)) is summable
(dominated by ‖w‖/(n+1)²) for re w ≥ 2. -/
theorem summable_digamma_majorant {w : ℂ} (hwre : 2 ≤ w.re) :
    Summable (fun n : ℕ => ‖w‖ / (((n : ℝ) + 1) * (w.re + (n : ℝ) + 1))) := by
  have h1 : Summable (fun n : ℕ => (((n : ℝ) + 1) ^ 2)⁻¹) := by
    have h2 : Summable (fun n : ℕ => (((n : ℝ)) ^ 2)⁻¹) := by
      have h3 := Real.summable_nat_rpow_inv.mpr (by norm_num : (1 : ℝ) < 2)
      have heq : (fun n : ℕ => ((n : ℝ) ^ (2 : ℝ))⁻¹) = fun n : ℕ => (((n : ℝ)) ^ 2)⁻¹ := by
        funext n
        rw [show ((2 : ℝ)) = ((2 : ℕ) : ℝ) by norm_num, Real.rpow_natCast]
      rwa [heq] at h3
    have h4 := (summable_nat_add_iff 1).mpr h2
    simpa [add_comm] using h4
  refine Summable.of_nonneg_of_le (fun n => by positivity) ?_ (h1.mul_left ‖w‖)
  intro n
  have hstep : ((n : ℝ) + 1) ^ 2 ≤ ((n : ℝ) + 1) * (w.re + (n : ℝ) + 1) := by
    rw [sq]
    apply mul_le_mul_of_nonneg_left _ (by positivity)
    have h2 : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg n
    linarith [hwre, h2]
  calc ‖w‖ / (((n : ℝ) + 1) * (w.re + (n : ℝ) + 1))
      ≤ ‖w‖ / (((n : ℝ) + 1) ^ 2) := by
        apply div_le_div_of_nonneg_left (norm_nonneg _)
          (show (0 : ℝ) < ((n : ℝ) + 1) ^ 2 by positivity) hstep
    _ = ‖w‖ * ((((n : ℝ) + 1) ^ 2)⁻¹) := by rw [div_eq_mul_inv]

/-- The per-term bound: ‖1/(n+1) − 1/(w+n+1)‖ ≤ ‖w‖/((n+1)(re w+n+1)). -/
theorem norm_digamma_term_le {w : ℂ} (hwre : 2 ≤ w.re) (n : ℕ) :
    ‖1 / ((n : ℂ) + 1) - 1 / (w + n + 1)‖
      ≤ ‖w‖ / (((n : ℝ) + 1) * (w.re + (n : ℝ) + 1)) := by
  have hwn1 : w + (n : ℂ) + 1 ≠ 0 := by
    intro h
    have h2 := congrArg Complex.re h
    simp [Complex.add_re, Complex.natCast_re, Complex.one_re] at h2
    have h3 : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg n
    linarith [hwre, h3, h2]
  have hident : 1 / ((n : ℂ) + 1) - 1 / (w + n + 1)
      = w / (((n : ℂ) + 1) * (w + n + 1)) := by
    field_simp [Nat.cast_add_one_ne_zero n, hwn1]
    ring
  have hrew : (w + (n : ℂ) + 1).re = w.re + (n : ℝ) + 1 := by
    simp [Complex.add_re, Complex.natCast_re, Complex.one_re]
  have hle : w.re + (n : ℝ) + 1 ≤ ‖w + (n : ℂ) + 1‖ := by
    have hpos : (0 : ℝ) ≤ (w + (n : ℂ) + 1).re := by
      rw [hrew]
      have h3 : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg n
      linarith [hwre, h3]
    have h2 := Complex.abs_re_le_norm (w + (n : ℂ) + 1)
    rwa [abs_of_nonneg hpos, hrew] at h2
  rw [hident, norm_div, norm_mul, DigammaSeries.norm_natCast_add_one]
  apply div_le_div_of_nonneg_left (norm_nonneg _)
  · apply mul_pos (by positivity)
    have h3 : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg n
    linarith [hwre, h3]
  · apply mul_le_mul_of_nonneg_left hle (by positivity)

/-- The harmonic-sum form used in the head split. -/
theorem sum_one_div_le_one_add_log (N : ℕ) :
    ∑ n ∈ Finset.range N, (1 : ℝ) / ((n : ℝ) + 1) ≤ 1 + Real.log N := by
  have h1 : (∑ n ∈ Finset.range N, (1 : ℝ) / ((n : ℝ) + 1)) = (harmonic N : ℝ) := by
    rw [harmonic, Rat.cast_sum]
    apply Finset.sum_congr rfl
    intro i _
    rw [Rat.cast_inv, Rat.cast_natCast, Nat.cast_add_one, one_div]
  rw [h1]
  exact harmonic_le_one_add_log N
/-- **The right-half-plane digamma bound (B)**: for re w ≥ 2, |im w| ≤ 5,
‖ψ(w)‖ ≤ 20·log(2+‖w‖). Weierstrass series + split at N = ⌈re w⌉₊;
positive integers via the harmonic identity. -/
theorem norm_digamma_le_of_two_le_re {w : ℂ} (hwre : 2 ≤ w.re) (hwim : |w.im| ≤ 5) :
    ‖Complex.digamma w‖ ≤ 20 * Real.log (2 + ‖w‖) := by
  have hw_norm_ge : 2 ≤ ‖w‖ := by
    have h1 := Complex.abs_re_le_norm w
    rw [abs_of_nonneg (by linarith [hwre])] at h1
    linarith [hwre, h1]
  have h1log4 : Real.log 4 ≤ Real.log (2 + ‖w‖) :=
    Real.log_le_log (by norm_num) (by linarith [hw_norm_ge])
  have hlog4gt : (1 : ℝ) < Real.log 4 := by
    have h4 := Real.log_two_gt_d9.le
    have h5 : Real.log 4 = 2 * Real.log 2 := by
      rw [show (4 : ℝ) = 2 ^ 2 by norm_num, Real.log_pow]
      push_cast
      ring
    linarith [h4, h5]
  have hlog4 : (5 : ℝ) / 3 ≤ 19 * Real.log (2 + ‖w‖) := by nlinarith [h1log4, hlog4gt]
  by_cases hwint : ∃ m : ℤ, (m : ℂ) = w
  · -- the positive-integer case: w = ↑n, n ≥ 2
    obtain ⟨m, hm⟩ := hwint
    have hmre : w.re = (m : ℝ) := by rw [← hm]; simp
    have hm2 : 2 ≤ m := by
      by_contra h
      push Not at h
      have h1 : (m : ℝ) ≤ 1 := by exact_mod_cast (show m ≤ 1 by omega)
      linarith [hwre, hmre, h1]
    have hn2 : 2 ≤ m.toNat := by
      have h1 : (m : ℤ) = ((m.toNat : ℕ) : ℤ) := (Int.toNat_of_nonneg (by omega)).symm
      rw [h1] at hm2
      exact_mod_cast hm2
    set n := m.toNat with hn_def
    have hwn : w = (n : ℂ) := by
      rw [← hm, hn_def]
      exact_mod_cast (Int.toNat_of_nonneg (by omega : (0 : ℤ) ≤ m)).symm
    rw [hwn, digamma_natCast_eq n (by omega)]
    have hγ0 : (0 : ℝ) ≤ Real.eulerMascheroniConstant :=
      (by norm_num : (0 : ℝ) ≤ 1 / 2).trans Real.one_half_lt_eulerMascheroniConstant.le
    have hreal : |(-Real.eulerMascheroniConstant + (harmonic (n - 1) : ℚ) : ℝ)|
        ≤ Real.eulerMascheroniConstant + (1 + Real.log ((n : ℝ) - 1)) := by
      have hH0ℚ : (0 : ℚ) ≤ harmonic (n - 1) :=
        Finset.sum_nonneg (fun i _ => by positivity)
      have hH0 : (0 : ℝ) ≤ ((harmonic (n - 1) : ℚ) : ℝ) := by exact_mod_cast hH0ℚ
      have hcast2 : ((n - 1 : ℕ) : ℝ) = (n : ℝ) - 1 := by
        rw [Nat.cast_sub (by omega : 1 ≤ n)]
        push_cast
        ring
      have hHbound : ((harmonic (n - 1) : ℚ) : ℝ) ≤ 1 + Real.log ((n : ℝ) - 1) := by
        have h := harmonic_le_one_add_log (n - 1)
        rw [hcast2] at h
        exact h
      have hlog0 : (0 : ℝ) ≤ Real.log ((n : ℝ) - 1) := by
        apply Real.log_nonneg
        have h1 : (1 : ℝ) ≤ ((n - 1 : ℕ) : ℝ) := by exact_mod_cast (by omega : 1 ≤ n - 1)
        linarith [h1, hcast2]
      apply abs_le.mpr
      constructor <;> linarith [hγ0, hH0, hHbound, hlog0]
    have hnrm : ‖-(Real.eulerMascheroniConstant : ℂ) + ((harmonic (n - 1) : ℚ) : ℂ)‖
        = |(-Real.eulerMascheroniConstant + (harmonic (n - 1) : ℚ) : ℝ)| := by
      rw [← Complex.ofReal_ratCast, ← Complex.ofReal_neg, ← Complex.ofReal_add,
        Complex.norm_real, Real.norm_eq_abs]
    rw [hnrm]
    have hlogn1 : Real.log ((n : ℝ) - 1) ≤ Real.log (2 + ‖w‖) := by
      have h2 : ((n - 1 : ℕ) : ℝ) = (n : ℝ) - 1 := by
        rw [Nat.cast_sub (by omega : 1 ≤ n)]
        push_cast
        ring
      have hpos : (0 : ℝ) < (n : ℝ) - 1 := by
        have h1 : (1 : ℝ) ≤ ((n - 1 : ℕ) : ℝ) := by exact_mod_cast (by omega : 1 ≤ n - 1)
        linarith [h1, h2]
      apply Real.log_le_log hpos
      have hwnorm : ‖w‖ = (n : ℝ) := by rw [hwn, RCLike.norm_natCast]
      rw [hwnorm]
      linarith [h2]
    have hγ1 : Real.eulerMascheroniConstant ≤ 1 :=
      Real.eulerMascheroniConstant_lt_two_thirds.le.trans (by norm_num)
    rw [hwn] at hlogn1 h1log4
    have hlogbig : (2 : ℝ) ≤ 19 * Real.log (2 + ‖(n : ℂ)‖) := by nlinarith [h1log4, hlog4gt]
    linarith [hreal, hγ1, hlogn1, hlogbig]
  · -- the series case: w off the integers
    have hcomp : w ∈ Complex.integerComplement := hwint
    rw [DigammaSeries.digamma_series hcomp]
    set A := w.re with hA_def
    set N := ⌈w.re⌉₊ with hN_def
    have hA0 : (0 : ℝ) < A := by linarith [hwre]
    have hNA : A ≤ (N : ℝ) := by rw [hN_def]; exact Nat.le_ceil _
    have hNA1 : (N : ℝ) ≤ A + 1 := by
      have h := Nat.ceil_lt_add_one (show (0 : ℝ) ≤ w.re by linarith [hwre])
      have h2 : ((⌈w.re⌉₊ : ℕ) : ℝ) < w.re + 1 := by exact_mod_cast h
      rw [hN_def]
      linarith [h2]
    have hN1 : 1 ≤ N := by
      have h1 : (2 : ℕ) ≤ N := by
        rw [hN_def]
        have h2 := Nat.ceil_mono hwre
        rwa [Nat.ceil_ofNat] at h2
      omega
    have hterm_summ : Summable (fun n : ℕ => ‖1 / ((n : ℂ) + 1) - 1 / (w + n + 1)‖) :=
      Summable.of_nonneg_of_le (fun n => norm_nonneg _) (fun n => norm_digamma_term_le hwre n)
        (summable_digamma_majorant hwre)
    -- the kernel: summable + the split bound
    have hker_summ : Summable (fun n : ℕ => (((n : ℝ) + 1) * (A + (n : ℝ) + 1))⁻¹) := by
      have h1 : Summable (fun n : ℕ => (((n : ℝ) + 1) ^ 2)⁻¹) := by
        have h2 : Summable (fun n : ℕ => (((n : ℝ)) ^ 2)⁻¹) := by
          have h3 := Real.summable_nat_rpow_inv.mpr (by norm_num : (1 : ℝ) < 2)
          have heq : (fun n : ℕ => ((n : ℝ) ^ (2 : ℝ))⁻¹)
              = fun n : ℕ => (((n : ℝ)) ^ 2)⁻¹ := by
            funext n
            rw [show ((2 : ℝ)) = ((2 : ℕ) : ℝ) by norm_num, Real.rpow_natCast]
          rwa [heq] at h3
        have h4 := (summable_nat_add_iff 1).mpr h2
        simpa [add_comm] using h4
      refine Summable.of_nonneg_of_le (fun n => by positivity) ?_ h1
      intro n
      apply (inv_le_inv₀ (by positivity) (by positivity)).mpr
      rw [sq]
      apply mul_le_mul_of_nonneg_left _ (by positivity)
      have h2 : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg n
      linarith [hA0, h2]
    have hsplit : (∑' n : ℕ, (((n : ℝ) + 1) * (A + (n : ℝ) + 1))⁻¹)
        = ∑ n ∈ Finset.range N, (((n : ℝ) + 1) * (A + (n : ℝ) + 1))⁻¹
          + ∑' n : ℕ, (fun m : ℕ => (((m : ℝ) + 1) * (A + (m : ℝ) + 1))⁻¹) (n + N) := by
      exact (hker_summ.sum_add_tsum_nat_add N).symm
    -- the head bound
    have hhead : ∑ n ∈ Finset.range N, (((n : ℝ) + 1) * (A + (n : ℝ) + 1))⁻¹
        ≤ (1 + Real.log (N : ℝ)) / A := by
      have hper : ∀ n : ℕ, (((n : ℝ) + 1) * (A + (n : ℝ) + 1))⁻¹
          ≤ ((n : ℝ) + 1)⁻¹ * A⁻¹ := by
        intro n
        have h1 : (0 : ℝ) < ((n : ℝ) + 1) * A := mul_pos (by positivity) hA0
        have h2 : (0 : ℝ) < ((n : ℝ) + 1) * (A + (n : ℝ) + 1) := by
          apply mul_pos (by positivity)
          have h3 : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg n
          linarith [hA0, h3]
        rw [← mul_inv]
        apply (inv_le_inv₀ h2 h1).mpr
        apply mul_le_mul_of_nonneg_left _ (by positivity)
        have h3 : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg n
        linarith [hA0, h3]
      have hS' : (∑ n ∈ Finset.range N, ((n : ℝ) + 1)⁻¹) ≤ 1 + Real.log (N : ℝ) := by
        have h := sum_one_div_le_one_add_log N
        simpa [one_div] using h
      calc ∑ n ∈ Finset.range N, (((n : ℝ) + 1) * (A + (n : ℝ) + 1))⁻¹
          ≤ ∑ n ∈ Finset.range N, ((n : ℝ) + 1)⁻¹ * A⁻¹ :=
            Finset.sum_le_sum fun n _ => hper n
        _ = (∑ n ∈ Finset.range N, ((n : ℝ) + 1)⁻¹) * A⁻¹ := by rw [← Finset.sum_mul]
        _ ≤ (1 + Real.log (N : ℝ)) * A⁻¹ :=
            mul_le_mul_of_nonneg_right hS' (inv_nonneg.mpr hA0.le)
        _ = (1 + Real.log (N : ℝ)) / A := by rw [div_eq_mul_inv]
    -- the tail bound
    have htail : (∑' n : ℕ, (fun m : ℕ => (((m : ℝ) + 1) * (A + (m : ℝ) + 1))⁻¹) (n + N))
        ≤ 1 / (N : ℝ) := by
      have h1 : Summable (fun n : ℕ => (fun m : ℕ => (((m : ℝ) + 1) * (A + (m : ℝ) + 1))⁻¹)
          (n + N)) :=
        (summable_nat_add_iff N).mpr hker_summ
      have hterm : ∀ n : ℕ, (fun m : ℕ => (((m : ℝ) + 1) * (A + (m : ℝ) + 1))⁻¹) (n + N)
          ≤ 1 / ((n : ℝ) + N) - 1 / ((n : ℝ) + N + 1) := by
        intro n
        show ((((n + N : ℕ) : ℝ) + 1) * (A + ((n + N : ℕ) : ℝ) + 1))⁻¹
          ≤ 1 / ((n : ℝ) + N) - 1 / ((n : ℝ) + N + 1)
        have hN0 : (0 : ℝ) < (n : ℝ) + N := by
          have h2 : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg n
          have h3 : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hN1
          linarith [h2, h3]
        have htele : (1 : ℝ) / ((n : ℝ) + N) - 1 / ((n : ℝ) + N + 1)
            = (((n : ℝ) + N) * ((n : ℝ) + N + 1))⁻¹ := by
          rw [div_sub_div _ _ hN0.ne' (by positivity)]
          rw [div_eq_iff (by positivity : ((n : ℝ) + N) * ((n : ℝ) + N + 1) ≠ 0)]
          rw [inv_mul_cancel₀ (by positivity : ((n : ℝ) + N) * ((n : ℝ) + N + 1) ≠ 0)]
          ring
        rw [htele]
        have h2 : (0 : ℝ) < ((n : ℝ) + N) * ((n : ℝ) + N + 1) := by positivity
        have h3 : (0 : ℝ) < (((n + N : ℕ) : ℝ) + 1) * (A + ((n + N : ℕ) : ℝ) + 1) := by
          apply mul_pos
          · push_cast
            have h4 : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg n
            have h5 : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hN1
            positivity
          · push_cast
            have h4 : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg n
            have h5 : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hN1
            linarith [hA0, h4, h5]
        apply (inv_le_inv₀ h3 h2).mpr
        push_cast
        have h4 : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg n
        nlinarith [hA0, h4, hN0]
      calc (∑' n : ℕ, (fun m : ℕ => (((m : ℝ) + 1) * (A + (m : ℝ) + 1))⁻¹) (n + N))
          ≤ ∑' n : ℕ, (1 / ((n : ℝ) + N) - 1 / ((n : ℝ) + N + 1)) :=
            Summable.tsum_le_tsum hterm h1 (hasSum_one_div_sub_telescope N hN1).summable
        _ = 1 / (N : ℝ) := (hasSum_one_div_sub_telescope N hN1).tsum_eq
    -- the kernel bound
    have hN0R : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hN1
    have hkernel_bound : (∑' n : ℕ, (((n : ℝ) + 1) * (A + (n : ℝ) + 1))⁻¹)
        ≤ (2 + Real.log (A + 1)) / A := by
      rw [hsplit]
      have h1 : (1 + Real.log (N : ℝ)) / A ≤ (1 + Real.log (A + 1)) / A := by
        have h2 : Real.log (N : ℝ) ≤ Real.log (A + 1) := Real.log_le_log hN0R hNA1
        rw [div_eq_mul_inv, div_eq_mul_inv]
        apply mul_le_mul_of_nonneg_right _ (inv_nonneg.mpr hA0.le)
        linarith [h2]
      have h2 : (1 : ℝ) / (N : ℝ) ≤ 1 / A := one_div_le_one_div_of_le hA0 hNA
      have h3 : (2 + Real.log (A + 1)) / A = (1 + Real.log (A + 1)) / A + 1 / A := by
        rw [← add_div]
        congr 1
        ring
      rw [h3]
      linarith [h1, h2, hhead, htail]
    -- the norm of the series
    have hser : ‖∑' n : ℕ, (1 / ((n : ℂ) + 1) - 1 / (w + n + 1))‖
        ≤ (‖w‖ / A) * (2 + Real.log (A + 1)) := by
      calc ‖∑' n : ℕ, (1 / ((n : ℂ) + 1) - 1 / (w + n + 1))‖
          ≤ ∑' n : ℕ, ‖1 / ((n : ℂ) + 1) - 1 / (w + n + 1)‖ :=
            norm_tsum_le_tsum_norm hterm_summ
        _ ≤ ∑' n : ℕ, ‖w‖ / (((n : ℝ) + 1) * (A + (n : ℝ) + 1)) :=
            Summable.tsum_le_tsum (fun n => norm_digamma_term_le hwre n) hterm_summ
              (summable_digamma_majorant hwre)
        _ = ‖w‖ * ∑' n : ℕ, (((n : ℝ) + 1) * (A + (n : ℝ) + 1))⁻¹ := by
            rw [show (∑' n : ℕ, ‖w‖ / (((n : ℝ) + 1) * (A + (n : ℝ) + 1)))
                = ∑' n : ℕ, ‖w‖ * (((n : ℝ) + 1) * (A + (n : ℝ) + 1))⁻¹ from
              tsum_congr fun n => by rw [div_eq_mul_inv]]
            exact tsum_mul_left
        _ ≤ ‖w‖ * ((2 + Real.log (A + 1)) / A) :=
            mul_le_mul_of_nonneg_left hkernel_bound (norm_nonneg _)
        _ = (‖w‖ / A) * (2 + Real.log (A + 1)) := by ring
    -- the ratio ‖w‖/A ≤ 3
    have hratio : ‖w‖ / A ≤ 3 := by
      have h1 : ‖w‖ ≤ 3 * A := by
        have hnormsq : ‖w‖ ^ 2 = w.re ^ 2 + w.im ^ 2 := by
          rw [← Complex.normSq_eq_norm_sq, Complex.normSq_apply]
          ring
        have him5 : w.im ^ 2 ≤ 25 := by
          calc w.im ^ 2 = |w.im| ^ 2 := by rw [sq_abs]
            _ ≤ 5 ^ 2 := pow_le_pow_left₀ (abs_nonneg _) hwim _
            _ = 25 := by norm_num
        have h2 : ‖w‖ ^ 2 ≤ (3 * A) ^ 2 := by
          rw [hnormsq]
          have hA2 : 2 ≤ A := hwre
          nlinarith [him5, hA2]
        exact le_of_pow_le_pow_left₀ (two_ne_zero) (by positivity) h2
      rw [div_le_iff₀ hA0]
      linarith [h1]
    have hlogA : Real.log (A + 1) ≤ Real.log (‖w‖ + 1) := by
      apply Real.log_le_log (by linarith [hA0])
      have h1 : w.re ≤ ‖w‖ := by
        have h2 := Complex.abs_re_le_norm w
        rwa [abs_of_nonneg (by linarith [hwre])] at h2
      linarith [h1]
    -- the final assembly
    have hγ1 : Real.eulerMascheroniConstant ≤ 1 :=
      Real.eulerMascheroniConstant_lt_two_thirds.le.trans (by norm_num)
    have h1w : ‖(1 : ℂ) / w‖ ≤ 1 := by
      rw [norm_div, norm_one]
      rw [div_le_one (by linarith [hw_norm_ge] : (0 : ℝ) < ‖w‖)]
      linarith [hw_norm_ge]
    calc ‖-(Real.eulerMascheroniConstant : ℂ) - 1 / w
          + ∑' n : ℕ, (1 / ((n : ℂ) + 1) - 1 / (w + n + 1))‖
        ≤ Real.eulerMascheroniConstant + ‖(1 : ℂ) / w‖
          + ‖∑' n : ℕ, (1 / ((n : ℂ) + 1) - 1 / (w + n + 1))‖ := by
          refine (norm_add_le _ _).trans ?_
          refine add_le_add_left ?_ _
          refine (norm_sub_le _ _).trans ?_
          refine add_le_add_left ?_ _
          rw [norm_neg,
            show (Real.eulerMascheroniConstant : ℂ)
              = ((Real.eulerMascheroniConstant : ℝ) : ℂ) from rfl,
            Complex.norm_real, Real.norm_eq_abs,
            abs_of_nonneg ((by norm_num : (0 : ℝ) ≤ 1 / 2).trans
              Real.one_half_lt_eulerMascheroniConstant.le)]
      _ ≤ 1 + 1 + (‖w‖ / A) * (2 + Real.log (A + 1)) := by
          linarith [hγ1, h1w, hser]
      _ ≤ 20 * Real.log (2 + ‖w‖) := by
          have h2 : (‖w‖ / A) * (2 + Real.log (A + 1)) ≤ 3 * (2 + Real.log (‖w‖ + 1)) := by
            have h5 : (0 : ℝ) ≤ Real.log (A + 1) :=
              Real.log_nonneg (by linarith [hwre] : (1 : ℝ) ≤ A + 1)
            have h3 : (0 : ℝ) ≤ 2 + Real.log (A + 1) := by linarith [h5]
            exact mul_le_mul hratio (by linarith [hlogA]) h3 (by norm_num)
          have h3 : Real.log (‖w‖ + 1) ≤ Real.log (2 + ‖w‖) :=
            Real.log_le_log (by positivity) (by linarith)
          have hlognonneg : (0 : ℝ) ≤ Real.log (2 + ‖w‖) :=
            Real.log_nonneg (by linarith [hw_norm_ge])
          nlinarith [h2, h3, hlog4, hlognonneg]

/-! ## 3. The separated reciprocal sum (C) -/

/-- The right half of the V-split: for j₀ = ⌈−re w⌉₊ and j > j₀,
‖(w+j)⁻¹‖ ≤ 1/(j−j₀) (real parts are 1-separated and j₀ catches up to
−re w). -/
theorem recip_norm_le_right {w : ℂ} {c : ℝ} (_hdist : ∀ m : ℕ, c ≤ ‖w + (m : ℂ)‖)
    {j₀ : ℕ} (hj₀ : j₀ = ⌈-w.re⌉₊) {j : ℕ} (hj : j₀ + 1 ≤ j) :
    ‖(w + (j : ℂ))⁻¹‖ ≤ ((j - j₀ : ℕ) : ℝ)⁻¹ := by
  have hj₀ge : -(w.re) ≤ (j₀ : ℝ) := by rw [hj₀]; exact Nat.le_ceil _
  have hrewj : (w + (j : ℂ)).re = w.re + (j : ℝ) := by
    simp [Complex.add_re, Complex.natCast_re]
  rw [norm_inv]
  have hge : ((j - j₀ : ℕ) : ℝ) ≤ ‖w + (j : ℂ)‖ := by
    have h1 : (w + (j : ℂ)).re ≤ ‖w + (j : ℂ)‖ := by
      have h2 := Complex.abs_re_le_norm (w + (j : ℂ))
      rwa [abs_of_nonneg (by
        rw [hrewj]
        have h3 : (0 : ℝ) ≤ w.re + (j₀ : ℝ) := by linarith [hj₀ge]
        have h4 : ((j₀ : ℝ) + 1) ≤ (j : ℝ) := by exact_mod_cast hj
        linarith [h3, h4])] at h2
    refine le_trans ?_ h1
    rw [hrewj]
    have h3 : (0 : ℝ) ≤ w.re + (j₀ : ℝ) := by linarith [hj₀ge]
    have h4 : ((j - j₀ : ℕ) : ℝ) = (j : ℝ) - (j₀ : ℝ) := by
      rw [Nat.cast_sub (by omega : j₀ ≤ j)]
    rw [h4]
    linarith [h3]
  have hpos : (0 : ℝ) < ((j - j₀ : ℕ) : ℝ) := by
    have h1 : (1 : ℕ) ≤ j - j₀ := by omega
    have h2 : (0 : ℝ) < ((j - j₀ : ℕ) : ℝ) := by exact_mod_cast h1
    exact h2
  exact (inv_le_inv₀ (by linarith [hge, hpos]) hpos).mpr hge

/-- The left half: for j < j₀ − 1 (so j₀ ≥ 2 and the real part is still
negative), ‖(w+j)⁻¹‖ ≤ 1/(j₀−1−j). -/
theorem recip_norm_le_left {w : ℂ} {c : ℝ} (_hdist : ∀ m : ℕ, c ≤ ‖w + (m : ℂ)‖)
    {j₀ : ℕ} (hj₀ : j₀ = ⌈-w.re⌉₊) {j : ℕ} (hj : j + 1 ≤ j₀ - 1) :
    ‖(w + (j : ℂ))⁻¹‖ ≤ ((j₀ - 1 - j : ℕ) : ℝ)⁻¹ := by
  have hj₀lt : (j₀ : ℝ) < -w.re + 1 := by
    rw [hj₀]
    by_cases hre : 0 ≤ -w.re
    · have h := Nat.ceil_lt_add_one hre
      have h2 : ((⌈-w.re⌉₊ : ℕ) : ℝ) < -w.re + 1 := by exact_mod_cast h
      exact h2
    · push Not at hre
      have h1 : ⌈-w.re⌉₊ = 0 := by
        apply Nat.ceil_eq_zero.mpr
        linarith [hre]
      rw [h1] at hj₀
      -- j₀ = 0 but j + 1 ≤ j₀ − 1 = 0 − 1 = 0 in ℕ: impossible
      omega
  have hrewj : (w + (j : ℂ)).re = w.re + (j : ℝ) := by
    simp [Complex.add_re, Complex.natCast_re]
  have hneg : (w + (j : ℂ)).re < 0 := by
    rw [hrewj]
    have hj₀2 : 2 ≤ j₀ := by omega
    have h5 : ((j₀ - 1 : ℕ) : ℝ) = (j₀ : ℝ) - 1 := by
      rw [Nat.cast_sub (by omega : 1 ≤ j₀)]
      push_cast
      ring
    have h6 : ((j + 1 : ℕ) : ℝ) ≤ ((j₀ - 1 : ℕ) : ℝ) := by exact_mod_cast hj
    rw [Nat.cast_add_one] at h6
    linarith [hj₀lt, h5, h6]
  rw [norm_inv]
  have hge : ((j₀ - 1 - j : ℕ) : ℝ) ≤ ‖w + (j : ℂ)‖ := by
    have h1 : |(w + (j : ℂ)).re| ≤ ‖w + (j : ℂ)‖ := Complex.abs_re_le_norm _
    rw [hrewj] at h1
    have h2 : |(w.re + (j : ℝ))| = -(w.re + (j : ℝ)) := abs_of_neg (by rwa [← hrewj])
    rw [h2] at h1
    refine le_trans ?_ h1
    have h4 : ((j₀ - 1 - j : ℕ) : ℝ) = (j₀ : ℝ) - 1 - (j : ℝ) := by
      rw [Nat.cast_sub (by omega : j ≤ j₀ - 1), Nat.cast_sub (by omega : 1 ≤ j₀)]
      push_cast
      ring
    rw [h4]
    linarith [hj₀lt]
  have hpos : (0 : ℝ) < ((j₀ - 1 - j : ℕ) : ℝ) := by
    have h1 : (1 : ℕ) ≤ j₀ - 1 - j := by omega
    exact_mod_cast h1
  exact (inv_le_inv₀ (by linarith [hge, hpos]) hpos).mpr hge

/-- **The separated reciprocal sum bound (C)**: for dist(w, −ℕ) ≥ c > 0,
Σ_{j<m} ‖w+j‖⁻¹ ≤ 2/c + 2 + 2·log m (the V-split: at most one term per
side needs the dist condition; the rest telescope into the harmonic bound). -/
theorem digamma_recip_sum_le {c : ℝ} (hc : 0 < c) {w : ℂ}
    (hdist : ∀ m : ℕ, c ≤ ‖w + (m : ℂ)‖) {m : ℕ} (hm : ⌈-w.re⌉₊ + 1 ≤ m) :
    ∑ j ∈ Finset.range m, ‖(w + (j : ℂ))⁻¹‖ ≤ 2 / c + 2 + 2 * Real.log m := by
  set j₀ := ⌈-w.re⌉₊ with hj₀
  have hj₀m : j₀ ≤ m := by omega
  have hm1 : 1 ≤ m := by omega
  have hHarm : ∀ K : ℕ, ∑ i ∈ Finset.range K, ((i : ℝ) + 1)⁻¹ ≤ 1 + Real.log K := by
    intro K
    have h := sum_one_div_le_one_add_log K
    simpa [one_div] using h
  have hlogmono : ∀ {a b : ℕ}, 1 ≤ a → a ≤ b →
      1 + Real.log (a : ℝ) ≤ 1 + Real.log (b : ℝ) := by
    intro a b ha hab
    have h1 : (0 : ℝ) < (a : ℝ) := by exact_mod_cast ha
    have h2 : (a : ℝ) ≤ (b : ℝ) := by exact_mod_cast hab
    have h3 := Real.log_le_log h1 h2
    linarith [h3]
  have hlogmono0 : ∀ {a b : ℕ}, a ≤ b → 1 ≤ b →
      1 + Real.log (a : ℝ) ≤ 1 + Real.log (b : ℝ) := by
    intro a b hab hb
    rcases eq_or_ne a 0 with ha | ha
    · rw [ha, Nat.cast_zero, Real.log_zero]
      have h2 : (0 : ℝ) ≤ Real.log (b : ℝ) := Real.log_nonneg (by exact_mod_cast hb)
      linarith [h2]
    · exact hlogmono (Nat.one_le_iff_ne_zero.mpr ha) hab
  have hsplit : ∑ j ∈ Finset.range m, ‖(w + (j : ℂ))⁻¹‖
      = ∑ j ∈ Finset.range j₀, ‖(w + (j : ℂ))⁻¹‖
        + ∑ j ∈ Finset.Ico j₀ m, ‖(w + (j : ℂ))⁻¹‖ := by
    rw [Finset.range_eq_Ico, Finset.range_eq_Ico,
      ← Finset.sum_Ico_consecutive _ (Nat.zero_le j₀) hj₀m]
  rw [hsplit]
  -- RIGHT side
  have hfirst_r : ‖(w + (j₀ : ℂ))⁻¹‖ ≤ 1 / c := by
    rw [norm_inv, show (1 : ℝ) / c = c⁻¹ by rw [one_div]]
    have hpos : (0 : ℝ) < ‖w + (j₀ : ℂ)‖ := lt_of_lt_of_le hc (hdist j₀)
    exact (inv_le_inv₀ hpos hc).mpr (hdist j₀)
  have hrest_r : ∑ j ∈ Finset.Ico (j₀ + 1) m, ‖(w + (j : ℂ))⁻¹‖ ≤ 1 + Real.log m := by
    calc ∑ j ∈ Finset.Ico (j₀ + 1) m, ‖(w + (j : ℂ))⁻¹‖
        ≤ ∑ j ∈ Finset.Ico (j₀ + 1) m, ((j - j₀ : ℕ) : ℝ)⁻¹ :=
          Finset.sum_le_sum fun j hj => recip_norm_le_right hdist hj₀ (by
            rw [Finset.mem_Ico] at hj; exact hj.1)
      _ = ∑ i ∈ Finset.range (m - (j₀ + 1)), ((i : ℝ) + 1)⁻¹ := by
          rw [Finset.sum_Ico_eq_sum_range]
          apply Finset.sum_congr rfl
          intro i _
          have h1 : (j₀ + 1 + i) - j₀ = i + 1 := by omega
          rw [h1, Nat.cast_add_one]
      _ ≤ 1 + Real.log (↑(m - (j₀ + 1)) : ℝ) := hHarm _
      _ ≤ 1 + Real.log m := hlogmono0 (show m - (j₀ + 1) ≤ m by omega) hm1
  have hright : ∑ j ∈ Finset.Ico j₀ m, ‖(w + (j : ℂ))⁻¹‖ ≤ 1 / c + (1 + Real.log m) := by
    have hsplit0 : ∑ j ∈ Finset.Ico j₀ m, ‖(w + (j : ℂ))⁻¹‖
        = (∑ i ∈ Finset.range (m - j₀ - 1), ‖(w + ((j₀ + (i + 1) : ℕ)) : ℂ)⁻¹‖)
          + ‖(w + (j₀ : ℂ))⁻¹‖ := by
      rw [Finset.sum_Ico_eq_sum_range]
      conv_lhs => rw [show m - j₀ = (m - j₀ - 1) + 1 by omega]
      rw [Finset.sum_range_succ']
      rw [add_zero]
    have hrest' : ∑ i ∈ Finset.range (m - j₀ - 1), ‖(w + ((j₀ + (i + 1) : ℕ)) : ℂ)⁻¹‖
        ≤ 1 + Real.log m := by
      calc ∑ i ∈ Finset.range (m - j₀ - 1), ‖(w + ((j₀ + (i + 1) : ℕ)) : ℂ)⁻¹‖
          ≤ ∑ i ∈ Finset.range (m - j₀ - 1), ((i : ℝ) + 1)⁻¹ := by
            apply Finset.sum_le_sum
            intro i _
            have h1 := recip_norm_le_right hdist hj₀ (j := j₀ + (i + 1)) (by omega)
            have h2 : (j₀ + (i + 1)) - j₀ = i + 1 := by omega
            rw [h2] at h1
            have h3 : (((i + 1 : ℕ)) : ℝ)⁻¹ = ((i : ℝ) + 1)⁻¹ := by rw [Nat.cast_add_one]
            rwa [h3] at h1
        _ ≤ 1 + Real.log (↑(m - j₀ - 1) : ℝ) := hHarm _
        _ ≤ 1 + Real.log m := hlogmono0 (show m - j₀ - 1 ≤ m by omega) hm1
    rw [hsplit0]
    calc (∑ i ∈ Finset.range (m - j₀ - 1), ‖(w + ((j₀ + (i + 1) : ℕ)) : ℂ)⁻¹‖)
          + ‖(w + (j₀ : ℂ))⁻¹‖
        ≤ (1 + Real.log m) + 1 / c := add_le_add hrest' hfirst_r
      _ = 1 / c + (1 + Real.log m) := by ring
  -- LEFT side
  have hleft : ∑ j ∈ Finset.range j₀, ‖(w + (j : ℂ))⁻¹‖ ≤ 1 / c + (1 + Real.log m) := by
    by_cases hj₀0 : j₀ = 0
    · rw [hj₀0]
      simp only [Finset.range_zero, Finset.sum_empty]
      have h1 : (0 : ℝ) ≤ 1 / c := by positivity
      have h2 : (0 : ℝ) ≤ Real.log m := Real.log_nonneg (by exact_mod_cast hm1)
      linarith [h1, h2]
    · have hj₀1 : 1 ≤ j₀ := Nat.one_le_iff_ne_zero.mpr hj₀0
      have hdecomp : ∑ j ∈ Finset.range j₀, ‖(w + (j : ℂ))⁻¹‖
          = ∑ j ∈ Finset.range (j₀ - 1), ‖(w + (j : ℂ))⁻¹‖
            + ‖(w + ((j₀ - 1 : ℕ) : ℂ))⁻¹‖ := by
        conv_lhs => rw [show j₀ = (j₀ - 1) + 1 by omega]
        rw [Finset.sum_range_succ]
      have hlast : ‖(w + ((j₀ - 1 : ℕ) : ℂ))⁻¹‖ ≤ 1 / c := by
        have hpos : (0 : ℝ) < ‖w + ((j₀ - 1 : ℕ) : ℂ)‖ := lt_of_lt_of_le hc (hdist (j₀ - 1))
        rw [norm_inv, show (1 : ℝ) / c = c⁻¹ by rw [one_div]]
        exact (inv_le_inv₀ hpos hc).mpr (hdist (j₀ - 1))
      have hrest_l : ∑ j ∈ Finset.range (j₀ - 1), ‖(w + (j : ℂ))⁻¹‖ ≤ 1 + Real.log m := by
        calc ∑ j ∈ Finset.range (j₀ - 1), ‖(w + (j : ℂ))⁻¹‖
            ≤ ∑ j ∈ Finset.range (j₀ - 1), ((j₀ - 1 - j : ℕ) : ℝ)⁻¹ :=
              Finset.sum_le_sum fun j hj => recip_norm_le_left hdist hj₀ (by
                rw [Finset.mem_range] at hj; omega)
          _ = ∑ i ∈ Finset.range (j₀ - 1), ((i : ℝ) + 1)⁻¹ := by
              apply Finset.sum_bij (fun j _ => j₀ - 2 - j)
              · intro j hj
                rw [Finset.mem_range] at hj
                exact Finset.mem_range.mpr (by omega)
              · intro j₁ hj₁ j₂ hj₂ h
                rw [Finset.mem_range] at hj₁ hj₂
                omega
              · intro i hi
                rw [Finset.mem_range] at hi
                exact ⟨j₀ - 2 - i, Finset.mem_range.mpr (by omega), by omega⟩
              · intro j hj
                rw [Finset.mem_range] at hj
                have h1 : ((j₀ - 1 - j : ℕ) : ℝ) = ((j₀ - 2 - j : ℕ) : ℝ) + 1 := by
                  rw [Nat.cast_sub (by omega : j ≤ j₀ - 1),
                    Nat.cast_sub (by omega : j ≤ j₀ - 2),
                    Nat.cast_sub hj₀1,
                    Nat.cast_sub (by omega : (2 : ℕ) ≤ j₀)]
                  push_cast
                  ring
                rw [h1]
          _ ≤ 1 + Real.log (↑(j₀ - 1) : ℝ) := hHarm _
          _ ≤ 1 + Real.log m := hlogmono0 (show j₀ - 1 ≤ m by omega) hm1
      calc ∑ j ∈ Finset.range j₀, ‖(w + (j : ℂ))⁻¹‖
          = ∑ j ∈ Finset.range (j₀ - 1), ‖(w + (j : ℂ))⁻¹‖
            + ‖(w + ((j₀ - 1 : ℕ) : ℂ))⁻¹‖ := hdecomp
        _ ≤ (1 + Real.log m) + 1 / c := add_le_add hrest_l hlast
        _ = 1 / c + (1 + Real.log m) := by ring
  have hcc : (2 : ℝ) / c = 1 / c + 1 / c := by ring
  rw [hcc]
  linarith [hleft, hright]

/-! ## 4. The near-axis left-plane bound (A) -/

/-- The digamma recurrence over a natural shift, pole-avoidance form
(weaker hypothesis than LiReflect's `digamma_add_natCast`, which needs
im w ≠ 0 — the near-axis application includes real points). -/
theorem digamma_add_natCast' {w : ℂ} (hw : ∀ k : ℕ, w ≠ -(k : ℂ)) (n : ℕ) :
    Complex.digamma (w + n) = Complex.digamma w + ∑ j ∈ Finset.range n, (w + (j : ℂ))⁻¹ := by
  induction n with
  | zero => simp
  | succ k ih =>
    have hne : ∀ m : ℕ, w + (k : ℂ) ≠ -(m : ℂ) := by
      intro m h
      apply hw (k + m)
      have h3 : w = -(m : ℂ) - (k : ℂ) := by
        have h4 := congrArg (· - (k : ℂ)) h
        rwa [add_sub_cancel_right] at h4
      rw [h3]
      push_cast
      ring
    have h1 := Complex.digamma_apply_add_one (w + (k : ℂ)) hne
    rw [show w + ((k + 1 : ℕ) : ℂ) = (w + (k : ℂ)) + 1 by push_cast; ring, h1, ih,
      Finset.sum_range_succ]
    ring

/-- **The near-axis left-plane digamma bound (A)**: for re w ≤ 2 and
dist(w, −ℕ) ≥ c > 0, ‖ψ(w)‖ ≤ (46 + 2/c) + 23·log(2+‖w‖). Recurrence
to re ∈ [3, 4] (`digamma_add_natCast'`) + §3's sum bound + the
landing-zone bound (StirlingVert for |im| ≥ 1/2, §2's (B) for |im| < 1/2). -/
theorem norm_digamma_le_of_dist_nat {c : ℝ} (hc : 0 < c) {w : ℂ}
    (hwre : w.re ≤ 2) (hdist : ∀ m : ℕ, c ≤ ‖w + (m : ℂ)‖) :
    ‖Complex.digamma w‖ ≤ (46 + 2 / c) + 23 * Real.log (2 + ‖w‖) := by
  -- pole-avoidance from the dist condition
  have hpoles : ∀ k : ℕ, w ≠ -(k : ℂ) := by
    intro k h
    have h1 := hdist k
    rw [h] at h1
    rw [show (-(k : ℂ)) + (k : ℂ) = 0 by ring, norm_zero] at h1
    linarith [hc, h1]
  -- the shift count: lands re(w + m) ∈ [3, 4)
  set m := ⌈2 - w.re⌉₊ + 1 with hm_def
  have hm1 : 1 ≤ m := by omega
  have hm_ge : (2 : ℝ) - w.re + 1 ≤ (m : ℝ) := by
    have h := Nat.le_ceil (2 - w.re)
    rw [hm_def]
    push_cast
    linarith [h]
  have hm_lt : (m : ℝ) < (2 - w.re) + 2 := by
    have h := Nat.ceil_lt_add_one (show (0 : ℝ) ≤ 2 - w.re by linarith [hwre])
    have h2 : ((⌈2 - w.re⌉₊ : ℕ) : ℝ) < (2 - w.re) + 1 := by exact_mod_cast h
    rw [hm_def]
    push_cast
    linarith [h2]
  set v := w + (m : ℂ) with hv_def
  have hvre : 3 ≤ v.re ∧ v.re < 4 := by
    have h1 : v.re = w.re + (m : ℝ) := by
      rw [hv_def]
      simp [Complex.add_re, Complex.natCast_re]
    rw [h1]
    constructor <;> linarith [hm_ge, hm_lt]
  have hvim : v.im = w.im := by
    rw [hv_def]
    simp [Complex.add_im, Complex.natCast_im]
  have hvnorm3 : 3 ≤ ‖v‖ := by
    have h1 := Complex.abs_re_le_norm v
    rw [abs_of_nonneg (by linarith [hvre.1])] at h1
    linarith [hvre.1, h1]
  -- j₀ for the sum bound
  have hj₀m : ⌈-w.re⌉₊ + 1 ≤ m := by
    by_cases hre : 0 ≤ -w.re
    · have h1 : ((⌈-w.re⌉₊ : ℕ) : ℝ) < -w.re + 1 := by
        have h := Nat.ceil_lt_add_one hre
        exact_mod_cast h
      have h2 : ((⌈-w.re⌉₊ + 1 : ℕ) : ℝ) < (m : ℝ) := by
        have h3 : ((⌈-w.re⌉₊ + 1 : ℕ) : ℝ) = ((⌈-w.re⌉₊ : ℕ) : ℝ) + 1 := Nat.cast_add_one _
        linarith [h1, hm_ge, h3]
      have h3 : ⌈-w.re⌉₊ + 1 < m := by exact_mod_cast h2
      omega
    · push Not at hre
      have h1 : ⌈-w.re⌉₊ = 0 := Nat.ceil_eq_zero.mpr (by linarith [hre])
      rw [h1]
      omega
  -- the recurrence + the sum bound
  have hshift : Complex.digamma v
      = Complex.digamma w + ∑ j ∈ Finset.range m, (w + (j : ℂ))⁻¹ := by
    rw [hv_def]
    exact digamma_add_natCast' hpoles m
  have hsum : ∑ j ∈ Finset.range m, ‖(w + (j : ℂ))⁻¹‖ ≤ 2 / c + 2 + 2 * Real.log m :=
    digamma_recip_sum_le hc hdist hj₀m
  -- the landing-zone bound
  have hLZ : ‖Complex.digamma v‖ ≤ 21 * Real.log (2 + ‖v‖) := by
    by_cases him : 1 / 2 ≤ |v.im|
    · have hst := StirlingVert.digamma_stirling (by linarith [hvre.1] : (0 : ℝ) < v.re) him
      have hnorm12 : ‖(1 / 2 : ℂ)‖ = 1 / 2 := by
        rw [show (1 / 2 : ℂ) = ((1 / 2 : ℝ) : ℂ) by norm_num, Complex.norm_real,
          Real.norm_eq_abs, abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 1 / 2)]
      calc ‖Complex.digamma v‖
          = ‖(Complex.digamma v - Complex.log v + (1 / 2 : ℂ) / v) + Complex.log v
              - (1 / 2 : ℂ) / v‖ := by
            congr 1; ring
        _ ≤ ‖Complex.digamma v - Complex.log v + (1 / 2 : ℂ) / v‖ + ‖Complex.log v‖
              + ‖(1 / 2 : ℂ) / v‖ := by
            refine (norm_sub_le _ _).trans ?_
            exact add_le_add_left (norm_add_le _ _) _
        _ ≤ 3 / v.im ^ 2 + (Real.log ‖v‖ + Real.pi) + (1 / 2) / ‖v‖ := by
            refine add_le_add (add_le_add hst (norm_log_le_of_one_le (by linarith [hvnorm3]))) ?_
            rw [norm_div, hnorm12]
        _ ≤ 21 * Real.log (2 + ‖v‖) := by
            have him2 : (1 : ℝ) / 4 ≤ v.im ^ 2 := by
              calc (1 : ℝ) / 4 = (1 / 2) ^ 2 := by norm_num
                _ ≤ |v.im| ^ 2 := pow_le_pow_left₀ (by norm_num) him _
                _ = v.im ^ 2 := by rw [sq_abs]
            have hlogv : Real.log ‖v‖ ≤ Real.log (2 + ‖v‖) :=
              Real.log_le_log (by linarith [hvnorm3]) (by linarith)
            have hlog5 : (0 : ℝ) ≤ Real.log (2 + ‖v‖) :=
              Real.log_nonneg (by linarith [hvnorm3])
            have hpi : Real.pi ≤ 4 := Real.pi_lt_d2.le.trans (by norm_num)
            have h1 : 3 / v.im ^ 2 ≤ 12 := by
              rw [div_le_iff₀ (by linarith [him2] : (0 : ℝ) < v.im ^ 2)]
              nlinarith [him2]
            have h2 : (1 / 2 : ℝ) / ‖v‖ ≤ 1 := by
              rw [div_le_one (by linarith [hvnorm3] : (0 : ℝ) < ‖v‖)]
              linarith [hvnorm3]
            have hlogbig : (1 : ℝ) < Real.log (2 + ‖v‖) := by
              have h5 := Real.log_le_log (by norm_num : (0 : ℝ) < 4)
                (by linarith [hvnorm3] : (4 : ℝ) ≤ 2 + ‖v‖)
              have h6 : (1 : ℝ) < Real.log 4 := by
                have h7 := Real.log_two_gt_d9
                have h8 : Real.log 4 = 2 * Real.log 2 := by
                  rw [show (4 : ℝ) = 2 ^ 2 by norm_num, Real.log_pow]
                  push_cast
                  ring
                linarith [h7, h8]
              linarith [h5, h6]
            nlinarith [h1, h2, hlogv, hpi, hlog5, hlogbig]
    · push Not at him
      have hB := norm_digamma_le_of_two_le_re (by linarith [hvre.1] : (2 : ℝ) ≤ v.re)
        (by linarith [him.le] : |v.im| ≤ 5)
      have hlognonneg : (0 : ℝ) ≤ Real.log (2 + ‖v‖) :=
        Real.log_nonneg (by linarith [hvnorm3])
      nlinarith [hB, hlognonneg]
  -- norms and log comparisons
  have hwm : (m : ℝ) ≤ 4 + ‖w‖ := by
    have h1 : (m : ℝ) ≤ (2 - w.re) + 2 := hm_lt.le
    have h2 : -w.re ≤ ‖w‖ := (neg_le_abs w.re).trans (Complex.abs_re_le_norm w)
    linarith [h1, h2]
  have hvnorm : ‖v‖ ≤ 2 * ‖w‖ + 4 := by
    rw [hv_def]
    calc ‖w + (m : ℂ)‖ ≤ ‖w‖ + ‖(m : ℂ)‖ := norm_add_le _ _
      _ = ‖w‖ + (m : ℝ) := by rw [RCLike.norm_natCast]
      _ ≤ 2 * ‖w‖ + 4 := by linarith [hwm]
  have hlogv_le : Real.log (2 + ‖v‖) ≤ 2 + Real.log (2 + ‖w‖) := by
    have h1 : 2 + ‖v‖ ≤ 4 * (2 + ‖w‖) := by linarith [hvnorm]
    have hposv : (0 : ℝ) < 2 + ‖v‖ := by linarith [hvnorm3]
    have h2 : Real.log (2 + ‖v‖) ≤ Real.log (4 * (2 + ‖w‖)) := Real.log_le_log hposv h1
    have h3 : Real.log (4 * (2 + ‖w‖)) = Real.log 4 + Real.log (2 + ‖w‖) :=
      Real.log_mul (by norm_num : (4 : ℝ) ≠ 0) (by positivity : (2 + ‖w‖) ≠ 0)
    have h4 : Real.log 4 ≤ 2 := by
      have h5 := Real.log_two_lt_d9.le
      have h6 : Real.log 4 = 2 * Real.log 2 := by
        rw [show (4 : ℝ) = 2 ^ 2 by norm_num, Real.log_pow]
        push_cast
        ring
      linarith [h5, h6]
    linarith [h2, h3, h4]
  have hlogm : Real.log m ≤ 1 + Real.log (2 + ‖w‖) := by
    have hmpos : (0 : ℝ) < (m : ℝ) := by exact_mod_cast hm1
    have h1 : (m : ℝ) ≤ 2 * (2 + ‖w‖) := by linarith [hwm, norm_nonneg w]
    have h2 : Real.log (m : ℝ) ≤ Real.log (2 * (2 + ‖w‖)) := Real.log_le_log hmpos h1
    have h3 : Real.log (2 * (2 + ‖w‖)) = Real.log 2 + Real.log (2 + ‖w‖) :=
      Real.log_mul (by norm_num) (by positivity)
    have h4 : Real.log 2 ≤ 1 := Real.log_two_lt_d9.le.trans (by norm_num)
    linarith [h2, h3, h4]
  -- the final assembly
  have hpsi : Complex.digamma w
      = Complex.digamma v - ∑ j ∈ Finset.range m, (w + (j : ℂ))⁻¹ := by
    linear_combination -hshift
  rw [hpsi]
  calc ‖Complex.digamma v - ∑ j ∈ Finset.range m, (w + (j : ℂ))⁻¹‖
      ≤ ‖Complex.digamma v‖ + ‖∑ j ∈ Finset.range m, (w + (j : ℂ))⁻¹‖ := norm_sub_le _ _
    _ ≤ 21 * Real.log (2 + ‖v‖) + (2 / c + 2 + 2 * Real.log m) :=
        add_le_add hLZ ((norm_sum_le _ _).trans hsum)
    _ ≤ (46 + 2 / c) + 23 * Real.log (2 + ‖w‖) := by
        linarith [hlogv_le, hlogm]

/-! ## 5. The general logDeriv ΓR identity (G) -/

/-- logDeriv of a finite product of the linear factors (z/2 + j),
valid for im s ≠ 0 (each factor nonzero). -/
theorem logDeriv_prod_range_linear {s : ℂ} (hs : s.im ≠ 0) (m : ℕ) :
    logDeriv (fun z : ℂ => ∏ j ∈ Finset.range m, (z / 2 + (j : ℂ))) s
      = ∑ j ∈ Finset.range m, (1 / 2 : ℂ) / (s / 2 + (j : ℂ)) := by
  have hne : ∀ j : ℕ, (s / 2 + (j : ℂ)) ≠ 0 := by
    intro j h
    apply hs
    have h1 : (s / 2 + (j : ℂ)).im = 0 := by rw [h]; simp
    have h2 : (s / 2 + (j : ℂ)).im = s.im / 2 := by
      simp [Complex.add_im, Complex.natCast_im, Complex.div_ofNat_im]
    rw [h2] at h1
    linarith [h1]
  induction m with
  | zero => simp [logDeriv_const]
  | succ k ih =>
    have hprod : (fun z : ℂ => ∏ j ∈ Finset.range (k + 1), (z / 2 + (j : ℂ)))
        = fun z : ℂ => (∏ j ∈ Finset.range k, (z / 2 + (j : ℂ))) * (z / 2 + (k : ℂ)) :=
      funext fun z => Finset.prod_range_succ _ k
    rw [hprod]
    rw [logDeriv_mul s (Finset.prod_ne_zero_iff.mpr fun j _ => hne j) (hne k)
      (by fun_prop) (by fun_prop)]
    rw [ih]
    have hfac : logDeriv (fun z : ℂ => z / 2 + (k : ℂ)) s = (1 / 2 : ℂ) / (s / 2 + (k : ℂ)) := by
      have h1 : HasDerivAt (fun z : ℂ => z / 2 + (k : ℂ)) (1 / 2 : ℂ) s :=
        ((hasDerivAt_id' s).div_const 2).add_const (k : ℂ)
      rw [logDeriv_apply, h1.deriv]
    rw [hfac, Finset.sum_range_succ]

/-- **(G) the general logDeriv ΓR identity**: for im s ≠ 0,
logDeriv ΓR s = −(log π)/2 + ½ψ(s/2) — the m-fold shift landing in
re > 0 (`gamma_mul_prod` + `digamma_add_natCast` + 5d's EventuallyEq
machinery). -/
theorem logDeriv_Gammaℝ_eq {s : ℂ} (hs : s.im ≠ 0) :
    logDeriv Complex.Gammaℝ s
      = -(Real.log Real.pi : ℂ) / 2 + (1 / 2 : ℂ) * Complex.digamma (s / 2) := by
  set m := ⌈max 0 (-(s.re / 2))⌉₊ + 1 with hm_def
  have hmge : (2 : ℝ) ≤ s.re + 2 * (m : ℝ) := by
    have h1 : max 0 (-(s.re / 2)) ≤ ((⌈max 0 (-(s.re / 2))⌉₊ : ℕ) : ℝ) := Nat.le_ceil _
    have h2 : -(s.re / 2) ≤ max 0 (-(s.re / 2)) := le_max_right _ _
    rw [hm_def]
    push_cast
    linarith [h1, h2]
  have hres2 : (0 : ℝ) < (s + 2 * (m : ℂ)).re := by
    have h1 : (s + 2 * (m : ℂ)).re = s.re + 2 * (m : ℝ) := by
      simp [Complex.add_re, Complex.mul_re, Complex.natCast_re]
    rw [h1]
    linarith [hmge]
  have hs2im : (s / 2).im ≠ 0 := by
    have h1 : (s / 2).im = s.im / 2 := by simp [Complex.div_ofNat_im]
    rw [h1]
    exact div_ne_zero hs (by norm_num : (2 : ℝ) ≠ 0)
  -- the pointwise identity on U = {im ≠ 0}
  have hU : IsOpen {z : ℂ | z.im ≠ 0} := isOpen_ne_fun Complex.continuous_im continuous_const
  have hPne : ∀ z : ℂ, z.im ≠ 0 → (∏ j ∈ Finset.range m, (z / 2 + (j : ℂ))) ≠ 0 := by
    intro z hz
    apply Finset.prod_ne_zero_iff.mpr
    intro j _ h
    apply hz
    have h1 : (z / 2 + (j : ℂ)).im = 0 := by rw [h]; simp
    have h2 : (z / 2 + (j : ℂ)).im = z.im / 2 := by
      simp [Complex.add_im, Complex.natCast_im, Complex.div_ofNat_im]
    rw [h2] at h1
    linarith [h1]
  have hpt : ∀ z : ℂ, z.im ≠ 0 → Complex.Gammaℝ z
      = ((Real.pi ^ m : ℝ) : ℂ) * Complex.Gammaℝ (z + 2 * (m : ℂ))
        / ∏ j ∈ Finset.range m, (z / 2 + (j : ℂ)) := by
    intro z hz
    have hside : ∀ k : ℕ, k < m → z / 2 ≠ -(k : ℂ) := by
      intro k _ h
      apply hz
      have h1 : (z / 2).im = 0 := by
        have h2 := congrArg Complex.im h
        simpa [Complex.neg_im, Complex.natCast_im] using h2
      simp [Complex.div_ofNat_im] at h1
      linarith [h1]
    have hrec := gamma_mul_prod (z / 2) m hside
    -- ΓR(z+2m) = π^{−(z+2m)/2}·Γ(z/2+m) = (π^m)⁻¹·ΓR(z)·∏
    have hG2 : Complex.Gammaℝ (z + 2 * (m : ℂ))
        = ((Real.pi ^ m : ℝ) : ℂ)⁻¹ * Complex.Gammaℝ z
          * ∏ j ∈ Finset.range m, (z / 2 + (j : ℂ)) := by
      rw [Complex.Gammaℝ_def, Complex.Gammaℝ_def]
      rw [show (-(z + 2 * (m : ℂ)) / 2) = -z / 2 - (m : ℂ) by ring]
      rw [show ((z + 2 * (m : ℂ)) / 2) = z / 2 + (m : ℂ) by ring]
      -- the cpow split
      have hpi : (Real.pi : ℂ) ^ (-z / 2 - (m : ℂ))
          = (Real.pi : ℂ) ^ (-z / 2) * ((Real.pi ^ m : ℝ) : ℂ)⁻¹ := by
        have hlog : Complex.log (Real.pi : ℂ) = (Real.log Real.pi : ℂ) :=
          (Complex.ofReal_log Real.pi_nonneg).symm
        rw [Complex.cpow_def_of_ne_zero (by exact_mod_cast Real.pi_ne_zero : (Real.pi : ℂ) ≠ 0) _,
          Complex.cpow_def_of_ne_zero (by exact_mod_cast Real.pi_ne_zero : (Real.pi : ℂ) ≠ 0) _,
          hlog]
        have harg : (Real.log Real.pi : ℂ) * (-z / 2 - (m : ℂ))
            = (Real.log Real.pi : ℂ) * (-z / 2) + ((-(m : ℝ) * Real.log Real.pi : ℝ) : ℂ) := by
          push_cast
          ring
        rw [harg, Complex.exp_add, ← Complex.ofReal_exp]
        have hexp : Real.exp (-(m : ℝ) * Real.log Real.pi) = (Real.pi ^ m)⁻¹ := by
          have h1 : (-(m : ℝ) * Real.log Real.pi) = Real.log ((Real.pi ^ m)⁻¹) := by
            rw [Real.log_inv, Real.log_pow]
            ring
          rw [h1, Real.exp_log (by positivity)]
        rw [hexp, Complex.ofReal_inv, Complex.ofReal_pow]
      rw [hpi, ← hrec]
      ring
    rw [eq_div_iff (hPne z hz), hG2]
    field_simp [show ((Real.pi ^ m : ℝ) : ℂ) ≠ 0 by exact_mod_cast pow_ne_zero m Real.pi_ne_zero]
  -- the EventuallyEq + the logDeriv computation
  have hEv : Complex.Gammaℝ =ᶠ[𝓝 s]
      fun z => ((Real.pi ^ m : ℝ) : ℂ) * Complex.Gammaℝ (z + 2 * (m : ℂ))
        / ∏ j ∈ Finset.range m, (z / 2 + (j : ℂ)) := by
    filter_upwards [hU.mem_nhds hs] with z hz using hpt z hz
  have hG2m : Complex.Gammaℝ (s + 2 * (m : ℂ)) ≠ 0 :=
    Complex.Gammaℝ_ne_zero_of_re_pos hres2
  have hπne : ((Real.pi ^ m : ℝ) : ℂ) ≠ 0 := by exact_mod_cast pow_ne_zero m Real.pi_ne_zero
  have hdG2m : DifferentiableAt ℂ (fun z : ℂ => Complex.Gammaℝ (z + 2 * (m : ℂ))) s := by
    have h1 : (s + 2 * (m : ℂ)).im ≠ 0 := by
      have h2 : (s + 2 * (m : ℂ)).im = s.im := by
        simp [Complex.add_im, Complex.mul_im, Complex.natCast_im]
      rwa [h2]
    exact (differentiableAt_Gammaℝ_of_im_ne_zero' h1).comp s
      (differentiableAt_id.add_const _)
  have hdP : DifferentiableAt ℂ (fun z : ℂ => ∏ j ∈ Finset.range m, (z / 2 + (j : ℂ))) s := by
    fun_prop
  rw [logDeriv_congr hEv]
  have hstep1 : logDeriv (fun z : ℂ => ((Real.pi ^ m : ℝ) : ℂ) * Complex.Gammaℝ (z + 2 * (m : ℂ))
        / ∏ j ∈ Finset.range m, (z / 2 + (j : ℂ))) s
      = logDeriv (fun z : ℂ => ((Real.pi ^ m : ℝ) : ℂ) * Complex.Gammaℝ (z + 2 * (m : ℂ))) s
        - logDeriv (fun z : ℂ => ∏ j ∈ Finset.range m, (z / 2 + (j : ℂ))) s :=
    logDeriv_div s (mul_ne_zero hπne hG2m) (hPne s hs)
      ((differentiableAt_const _).mul hdG2m) hdP
  have hstep2 : logDeriv (fun z : ℂ => ((Real.pi ^ m : ℝ) : ℂ) * Complex.Gammaℝ (z + 2 * (m : ℂ))) s
      = logDeriv Complex.Gammaℝ (s + 2 * (m : ℂ)) := by
    rw [logDeriv_const_mul s _ hπne]
    have hder : deriv (fun z : ℂ => Complex.Gammaℝ (z + 2 * (m : ℂ))) s
        = deriv Complex.Gammaℝ (s + 2 * (m : ℂ)) := by
      have h1 : (s + 2 * (m : ℂ)).im ≠ 0 := by
        have h2 : (s + 2 * (m : ℂ)).im = s.im := by
          simp [Complex.add_im, Complex.mul_im, Complex.natCast_im]
        rwa [h2]
      have h3 := ((differentiableAt_Gammaℝ_of_im_ne_zero' h1).hasDerivAt).comp s
        ((hasDerivAt_id' s).add_const (2 * (m : ℂ)))
      have h4 : deriv (fun z : ℂ => Complex.Gammaℝ (z + 2 * (m : ℂ))) s
          = deriv Complex.Gammaℝ (s + 2 * (m : ℂ)) * 1 := h3.deriv
      rwa [mul_one] at h4
    simp only [logDeriv_apply, hder]
  rw [hstep1, hstep2]
  have hev : logDeriv Complex.Gammaℝ (s + 2 * (m : ℂ))
      = -(Real.log Real.pi : ℂ) / 2 + (1 / 2 : ℂ) * Complex.digamma ((s + 2 * (m : ℂ)) / 2) :=
    RvM.logDeriv_Gammaℝ hres2
  rw [hev, logDeriv_prod_range_linear hs m]
  rw [show (s + 2 * (m : ℂ)) / 2 = s / 2 + (m : ℂ) by ring, digamma_add_natCast hs2im m]
  have hsumform : ∑ j ∈ Finset.range m, (1 / 2 : ℂ) / (s / 2 + (j : ℂ))
      = (1 / 2 : ℂ) * ∑ j ∈ Finset.range m, (s / 2 + (j : ℂ))⁻¹ := by
    rw [Finset.mul_sum]
    apply Finset.sum_congr rfl
    intro j _
    rw [div_eq_mul_inv]
  rw [hsumform]
  ring

end NguyenRH1

end