{
  "file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigamma.lean",
  "old_string": "  rw [lagariasA, if_neg hj1]\n  push_cast\n  congr 1\n  have hcast : (\u2191(\u2211' m : {m : \u2115 // Odd m \u2227 3 \u2264 m}, (1 / (m : \u211d)) ^ (j + 1)) : \u2102) =\n      \u2211' m : {m : \u2115 // Odd m \u2227 3 \u2264 m}, (((m : \u2115) : \u2102)) ^ (-(j : \u2124) - 1) := by\n    have h2 := Complex.ofRealCLM.map_tsum (oddSlice_summable (j + 1) (by omega))\n    rw [Complex.ofRealCLM_apply] at h2\n    rw [h2]\n    apply tsum_congr\n    intro m\n    rw [Complex.ofRealCLM_apply]\n    push_cast\n    have hexp : (-(j : \u2124) - 1 : \u2124) = -(((j + 1 : \u2115) : \u2124)) := by push_cast; ring\n    rw [hexp]\n    rw [show (((m : \u2115) : \u2102)) ^ (-(((j + 1 : \u2115) : \u2124))) = ((((m : \u2115) : \u2102) ^ (j + 1))\u207b\u00b9) from by\n      rw [zpow_neg, zpow_natCast]]\n    rw [one_div_pow, inv_eq_one_div]\n  rw [hcast]",
  "new_string": "  rw [lagariasA, if_neg hj1]\n  push_cast\n  congr 1\n  apply tsum_congr\n  intro m\n  push_cast\n  have hexp : (-(j : \u2124) - 1 : \u2124) = -(((j + 1 : \u2115) : \u2124)) := by push_cast; ring\n  rw [hexp]\n  rw [show (((m : \u2115) : \u2102)) ^ (-(((j + 1 : \u2115) : \u2124))) = ((((m : \u2115) : \u2102) ^ (j + 1))\u207b\u00b9) from by\n    rw [zpow_neg, zpow_natCast]]\n  rw [one_div_pow, inv_eq_one_div]"
}

{
  "filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigamma.lean",
  "oldString": "  rw [lagariasA, if_neg hj1]\n  push_cast\n  congr 1\n  have hcast : (\u2191(\u2211' m : {m : \u2115 // Odd m \u2227 3 \u2264 m}, (1 / (m : \u211d)) ^ (j + 1)) : \u2102) =\n      \u2211' m : {m : \u2115 // Odd m \u2227 3 \u2264 m}, (((m : \u2115) : \u2102)) ^ (-(j : \u2124) - 1) := by\n    have h2 := Complex.ofRealCLM.map_tsum (oddSlice_summable (j + 1) (by omega))\n    rw [Complex.ofRealCLM_apply] at h2\n    rw [h2]\n    apply tsum_congr\n    intro m\n    rw [Complex.ofRealCLM_apply]\n    push_cast\n    have hexp : (-(j : \u2124) - 1 : \u2124) = -(((j + 1 : \u2115) : \u2124)) := by push_cast; ring\n    rw [hexp]\n    rw [show (((m : \u2115) : \u2102)) ^ (-(((j + 1 : \u2115) : \u2124))) = ((((m : \u2115) : \u2102) ^ (j + 1))\u207b\u00b9) from by\n      rw [zpow_neg, zpow_natCast]]\n    rw [one_div_pow, inv_eq_one_div]\n  rw [hcast]",
  "newString": "  rw [lagariasA, if_neg hj1]\n  push_cast\n  congr 1\n  apply tsum_congr\n  intro m\n  push_cast\n  have hexp : (-(j : \u2124) - 1 : \u2124) = -(((j + 1 : \u2115) : \u2124)) := by push_cast; ring\n  rw [hexp]\n  rw [show (((m : \u2115) : \u2102)) ^ (-(((j + 1 : \u2115) : \u2124))) = ((((m : \u2115) : \u2102) ^ (j + 1))\u207b\u00b9) from by\n    rw [zpow_neg, zpow_natCast]]\n  rw [one_div_pow, inv_eq_one_div]",
  "originalFile": "/-\nNguyenRH1/LiDigamma.lean \u2014 tier ii\u2032 sub-stage ii\u2032-3a, piece (A) core\n(D-066 \u00a74): the digamma partial-fraction series and the polygamma values\nat 1/2.\n\nMathlib has no digamma series; we build it from BohrMollerup's\n`logGammaSeq x n = x\u00b7log n + log n! \u2212 \u03a3_{m=0}^n log(x+m)` with\n`tendsto_log_gamma`. The derivative sequence\n  d/dx[logGammaSeq x n] = log n \u2212 \u03a3_{m=0}^n 1/(x+m)\n  = (log n \u2212 H_n) + [\u22121/x + \u03a3_{m=1}^n (1/m \u2212 1/(x+m))]\nconverges locally uniformly on (0,\u221e) (the harmonic piece to \u2212\u03b3 by\n`Real.tendsto_harmonic_sub_log`; the series piece by the Weierstrass\nM-test with \u03a3 1/m\u00b2), so the deriv-limit interchange\n(`hasDerivAt_of_tendstoLocallyUniformlyOn`) yields the real identity\n  (log \u0393)'(x) = \u2212\u03b3 \u2212 1/x + \u03a3_{m\u22651} (1/m \u2212 1/(x+m))   (x > 0).\nThe complex series converges locally uniformly on the right half-plane\n{0 < re s}, hence is analytic there and agrees with Complex.digamma by\nthe identity principle (`AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq`\nthrough the real segment); termwise iterated derivation\n(`iteratedDerivWithin_tsum`) then gives the polygamma values\n  digamma^{(j)}(1/2) = (\u22121)^{j+1}\u00b7j!\u00b7\u03a3_{m\u22650} (m + 1/2)^{\u2212(j+1)}   (j \u2265 1),\nand the odd-m reindexing identifies the sum as 2^{j+1}\u00b7lagariasA (j+1).\n\nArchive references: D-066 (route \u03b24, piece A), journal-020.\n-/\nimport Mathlib\nimport NguyenRH1.LiSwaps\n\nopen Zeta23 Complex Filter Topology Real\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. The real series: summability -/\n\n/-- The digamma series summand: 1/(m+1) \u2212 1/(x+m+1) (m : \u2115, x : \u211d). -/\ndef dpsiTermR (x : \u211d) (m : \u2115) : \u211d := 1 / (m + 1 : \u211d) - 1 / (x + m + 1)\n\n/-- The real digamma series: \u2212\u03b3 \u2212 1/x + \u03a3_{m\u22650} dpsiTermR x m. -/\ndef DinfR (x : \u211d) : \u211d :=\n  -Real.eulerMascheroniConstant - 1 / x + \u2211' m : \u2115, dpsiTermR x m\n\n/-- For 0 < x the summand is x/((m+1)(x+m+1)) \u2265 0, \u2264 x/(m+1)\u00b2. -/\nlemma dpsiTermR_eq {x : \u211d} (hx : 0 < x) (m : \u2115) :\n    dpsiTermR x m = x / ((m + 1 : \u211d) * (x + m + 1)) := by\n  have hm0 : (0 : \u211d) < (m : \u211d) + 1 := by positivity\n  have hxm : (0 : \u211d) < x + m + 1 := by positivity\n  rw [dpsiTermR]\n  field_simp\n  ring\n\nlemma dpsiTermR_nonneg {x : \u211d} (hx : 0 < x) (m : \u2115) : 0 \u2264 dpsiTermR x m := by\n  rw [dpsiTermR_eq hx]\n  positivity\n\nlemma dpsiTermR_le {x : \u211d} (hx : 0 < x) (m : \u2115) :\n    dpsiTermR x m \u2264 x / ((m : \u211d) + 1) ^ 2 := by\n  have hm0 : (0 : \u211d) < (m : \u211d) + 1 := by positivity\n  have hxm : (0 : \u211d) < x + m + 1 := by positivity\n  rw [dpsiTermR_eq hx]\n  have hCB : ((m : \u211d) + 1) ^ 2 \u2264 ((m : \u211d) + 1) * (x + m + 1) := by\n    rw [pow_two]\n    apply mul_le_mul_of_nonneg_left _ hm0.le\n    linarith [Nat.cast_nonneg (\u03b1 := \u211d) m]\n  have h4 : 1 / ((\u2191m + 1) * (x + \u2191m + 1)) \u2264 1 / ((\u2191m + 1) ^ 2) :=\n    one_div_le_one_div_of_le (by positivity) hCB\n  rw [one_div, one_div] at h4\n  rw [div_eq_mul_inv, div_eq_mul_inv]\n  exact mul_le_mul_of_nonneg_left h4 hx.le\n\n/-- The dominator family is summable (p-series at p = 2, shifted). -/\nlemma summable_div_add_one_sq (c : \u211d) :\n    Summable (fun m : \u2115 => c / ((m : \u211d) + 1) ^ 2) := by\n  have h := Real.summable_one_div_nat_pow.mpr (show 1 < 2 from by norm_num)\n  have h2 : Summable (fun m : \u2115 => (1 : \u211d) / ((m : \u211d) + 1) ^ 2) := by\n    have h3 : Summable (fun m : \u2115 => (1 : \u211d) / ((m + 1 : \u2115) : \u211d) ^ 2) :=\n      (summable_nat_add_iff 1).mpr h\n    apply h3.congr\n    intro m\n    push_cast\n    ring_nf\n  exact (h2.mul_left c).congr (fun m => by ring)\n\n/-- The real digamma series is summable for 0 < x. -/\nlemma dpsiTermR_summable {x : \u211d} (hx : 0 < x) : Summable (dpsiTermR x) :=\n  Summable.of_nonneg_of_le (dpsiTermR_nonneg hx) (dpsiTermR_le hx) (summable_div_add_one_sq x)\n\n/-! ## 2. The deriv-limit interchange: (log \u0393)' = DinfR on (0,\u221e) -/\n\n/-- The derivative of logGammaSeq x n in x: log n \u2212 \u03a3_{m=0}^n 1/(x+m). -/\ndef dpsiSeqR (n : \u2115) (x : \u211d) : \u211d :=\n  Real.log n - \u2211 m \u2208 Finset.range (n + 1), 1 / (x + m)\n\n/-- The derivative sequence decomposes as (log n \u2212 H_n) + (\u22121/x + partial series). -/\nlemma dpsiSeqR_eq (n : \u2115) (x : \u211d) :\n    dpsiSeqR n x = (Real.log n - (harmonic n : \u211d)) +\n      (-1 / x + \u2211 m \u2208 Finset.range n, dpsiTermR x m) := by\n  rw [dpsiSeqR]\n  have hh : (harmonic n : \u211d) = \u2211 i \u2208 Finset.range n, 1 / ((i : \u211d) + 1) := by\n    rw [harmonic]\n    push_cast\n    apply Finset.sum_congr rfl\n    intro i hi\n    rw [one_div]\n  have h2 : \u2211 m \u2208 Finset.range (n + 1), 1 / (x + (m : \u211d)) =\n      1 / x + \u2211 i \u2208 Finset.range n, 1 / (x + i + 1) := by\n    rw [Finset.sum_range_succ']\n    have e : \u2200 i : \u2115, 1 / (x + ((i + 1 : \u2115) : \u211d)) = 1 / (x + i + 1 : \u211d) := fun i => by\n      push_cast\n      ring_nf\n    rw [Finset.sum_congr rfl (fun i _ => e i)]\n    have e0 : 1 / (x + ((0 : \u2115) : \u211d)) = 1 / x := by simp\n    rw [e0]\n    ring\n  have h3 : \u2211 i \u2208 Finset.range n, dpsiTermR x i =\n      \u2211 i \u2208 Finset.range n, 1 / ((i : \u211d) + 1) - \u2211 i \u2208 Finset.range n, 1 / (x + i + 1) := by\n    rw [\u2190 Finset.sum_sub_distrib]\n    apply Finset.sum_congr rfl\n    intro i hi\n    rw [dpsiTermR]\n  rw [hh, h2, h3]\n  ring\n\n/-- The series part converges uniformly on compacts inside (0,\u221e). -/\nlemma dpsiTermR_summableLocallyUniformlyOn :\n    SummableLocallyUniformlyOn (fun m : \u2115 => fun x : \u211d => dpsiTermR x m) (Set.Ioi 0) := by\n  apply SummableLocallyUniformlyOn_of_locally_bounded isOpen_Ioi\n  intro K hK hKc\n  by_cases hKe : K = \u2205\n  \u00b7 subst hKe\n    exact \u27e80, summable_zero, fun m x hx => by simp at hx\u27e9\n  \u00b7 obtain \u27e8x0, hx0\u27e9 := Set.nonempty_iff_ne_empty.mpr hKe\n    obtain \u27e8C, hCK, hCle\u27e9 := hKc.exists_isMaxOn \u27e8x0, hx0\u27e9 (continuous_id.continuousOn)\n    refine \u27e8fun m => C / ((m : \u211d) + 1) ^ 2, summable_div_add_one_sq C, fun m x hx => ?_\u27e9\n    have hx0 : 0 < x := hK hx\n    have hxC : x \u2264 C := hCle hx\n    rw [Real.norm_eq_abs, abs_of_nonneg (dpsiTermR_nonneg hx0 m)]\n    calc dpsiTermR x m \u2264 x / ((m : \u211d) + 1) ^ 2 := dpsiTermR_le hx0 m\n      _ \u2264 C / ((m : \u211d) + 1) ^ 2 :=\n          (div_le_div_iff_of_pos_right (by positivity : (0 : \u211d) < ((m : \u211d) + 1) ^ 2)).mpr hxC\n\n/-- The derivative sequence converges locally uniformly to DinfR on (0,\u221e). -/\nlemma dpsiSeqR_tendstoLocallyUniformlyOn :\n    TendstoLocallyUniformlyOn dpsiSeqR DinfR atTop (Set.Ioi 0) := by\n  have hA : TendstoLocallyUniformlyOn (fun n : \u2115 => fun _ : \u211d => Real.log n - (harmonic n : \u211d))\n      (fun _ => -Real.eulerMascheroniConstant) atTop (Set.Ioi 0) := by\n    have h := Real.tendsto_harmonic_sub_log\n    have h2 : Tendsto (fun n : \u2115 => Real.log n - (harmonic n : \u211d)) atTop\n        (\ud835\udcdd (-Real.eulerMascheroniConstant)) := by\n      have h3 : \u2200 n : \u2115, -((harmonic n : \u211d) - Real.log n) =\n          Real.log n - (harmonic n : \u211d) := fun n => by ring\n      exact Real.tendsto_harmonic_sub_log.neg.congr'\n        (Filter.Eventually.of_forall h3)\n    rw [tendstoLocallyUniformlyOn_iff_forall_isCompact isOpen_Ioi]\n    intro K hK hKc\n    rw [Metric.tendstoUniformlyOn_iff]\n    intro \u03b5 h\u03b5\n    rw [Metric.tendsto_atTop] at h2\n    obtain \u27e8N, hN\u27e9 := h2 \u03b5 h\u03b5\n    rw [Filter.eventually_atTop]\n    exact \u27e8N, fun n hn x hx => by rw [dist_comm]; exact hN n hn\u27e9\n  have hB : TendstoLocallyUniformlyOn (fun _ : \u2115 => fun x : \u211d => -1 / x) (fun x => -1 / x)\n      atTop (Set.Ioi 0) := by\n    rw [tendstoLocallyUniformlyOn_iff_forall_isCompact isOpen_Ioi]\n    intro K hK hKc\n    rw [Metric.tendstoUniformlyOn_iff]\n    intro \u03b5 h\u03b5\n    rw [Filter.eventually_atTop]\n    exact \u27e80, fun n _ x _ => by simpa using h\u03b5\u27e9\n  have hC : TendstoLocallyUniformlyOn (fun n : \u2115 => fun x : \u211d => \u2211 m \u2208 Finset.range n, dpsiTermR x m)\n      (fun x => \u2211' m : \u2115, dpsiTermR x m) atTop (Set.Ioi 0) := by\n    rw [tendstoLocallyUniformlyOn_iff_forall_isCompact isOpen_Ioi]\n    intro K hK hKc\n    by_cases hKe : K = \u2205\n    \u00b7 subst hKe\n      rw [Metric.tendstoUniformlyOn_iff]\n      intro \u03b5 h\u03b5\n      rw [Filter.eventually_atTop]\n      exact \u27e80, fun n _ x hx => by simp at hx\u27e9\n    \u00b7 obtain \u27e8x0, hx0\u27e9 := Set.nonempty_iff_ne_empty.mpr hKe\n      obtain \u27e8C, hCK, hCle\u27e9 := hKc.exists_isMaxOn \u27e8x0, hx0\u27e9 (continuous_id.continuousOn)\n      apply tendstoUniformlyOn_tsum_nat (summable_div_add_one_sq C)\n      intro m x hx\n      have hx0 : 0 < x := hK hx\n      have hxC : x \u2264 C := hCle hx\n      rw [Real.norm_eq_abs, abs_of_nonneg (dpsiTermR_nonneg hx0 m)]\n      calc dpsiTermR x m \u2264 x / ((m : \u211d) + 1) ^ 2 := dpsiTermR_le hx0 m\n        _ \u2264 C / ((m : \u211d) + 1) ^ 2 :=\n            (div_le_div_iff_of_pos_right (by positivity : (0 : \u211d) < ((m : \u211d) + 1) ^ 2)).mpr hxC\n  have hdecomp : \u2200 n : \u2115, (Set.Ioi 0).EqOn (dpsiSeqR n)\n      (fun x => (Real.log n - (harmonic n : \u211d)) +\n        (-1 / x + \u2211 m \u2208 Finset.range n, dpsiTermR x m)) :=\n    fun n x _ => dpsiSeqR_eq n x\n  have hlimit : (Set.Ioi 0).EqOn\n      (fun x => -Real.eulerMascheroniConstant + (-1 / x + \u2211' m : \u2115, dpsiTermR x m)) DinfR :=\n    fun x _ => by rw [DinfR]; ring\n  exact ((hA.add (hB.add hC)).congr (fun n x _ => (dpsiSeqR_eq n x).symm)).congr_right hlimit\n\n/-- (log \u0393)'(x) = DinfR(x) for x > 0 \u2014 the interchange. -/\nlemma deriv_log_Gamma_real {x : \u211d} (hx : 0 < x) :\n    deriv (Real.log \u2218 Real.Gamma) x = DinfR x := by\n  have hfg : \u2200 y \u2208 Set.Ioi 0, Tendsto (fun n => BohrMollerup.logGammaSeq y n) atTop\n      (\ud835\udcdd ((Real.log \u2218 Real.Gamma) y)) := by\n    intro y hy\n    exact BohrMollerup.tendsto_log_gamma hy\n  have hf : \u2200\u1da0 n in atTop, \u2200 y \u2208 Set.Ioi 0,\n      HasDerivAt (fun y => BohrMollerup.logGammaSeq y n) (dpsiSeqR n y) y := by\n    apply Filter.Eventually.of_forall\n    intro n y hy\n    have h1 : HasDerivAt (fun y => y * Real.log n) (Real.log n) y := by\n      simpa using (hasDerivAt_id y).mul_const (Real.log n)\n    have h2 : HasDerivAt (fun _ : \u211d => Real.log (n !)) 0 y := hasDerivAt_const _ _\n    have h3 : HasDerivAt (fun y => \u2211 m \u2208 Finset.range (n + 1), Real.log (y + (m : \u211d)))\n        (\u2211 m \u2208 Finset.range (n + 1), (1 / (y + (m : \u211d)))) y := by\n      rw [show (fun y => \u2211 m \u2208 Finset.range (n + 1), Real.log (y + (m : \u211d))) =\n        \u2211 m \u2208 Finset.range (n + 1), (fun y => Real.log (y + (m : \u211d))) from by\n        funext y; simp [Finset.sum_apply]]\n      apply HasDerivAt.sum\n      intro m hm\n      have hym : (0 : \u211d) < y + m := by\n        have := hy\n        rw [Set.mem_Ioi] at this\n        positivity\n      have h4 : HasDerivAt (fun y : \u211d => y + (m : \u211d)) 1 y := by\n        simpa using (hasDerivAt_id y).add_const (m : \u211d)\n      have h5 := (Real.hasDerivAt_log (ne_of_gt hym)).comp y h4\n      rw [mul_one] at h5\n      have heq : (Real.log \u2218 fun y : \u211d => y + (m : \u211d)) = fun y => Real.log (y + (m : \u211d)) := rfl\n      rw [heq] at h5\n      have hinv : (1 : \u211d) / (y + (m : \u211d)) = (y + (m : \u211d))\u207b\u00b9 := by rw [one_div]\n      rw [hinv]\n      exact h5\n    have hmain : HasDerivAt (fun y => y * Real.log n + Real.log (n !) -\n        \u2211 m \u2208 Finset.range (n + 1), Real.log (y + (m : \u211d)))\n        (Real.log n + 0 - \u2211 m \u2208 Finset.range (n + 1), 1 / (y + (m : \u211d))) y :=\n      (h1.add h2).sub h3\n    have hzero : Real.log n + 0 - \u2211 m \u2208 Finset.range (n + 1), 1 / (y + (m : \u211d)) =\n        dpsiSeqR n y := by\n      rw [dpsiSeqR]\n      ring\n    rw [hzero] at hmain\n    have heq : (fun y => BohrMollerup.logGammaSeq y n) =\n        fun y => y * Real.log n + Real.log (n !) -\n          \u2211 m \u2208 Finset.range (n + 1), Real.log (y + (m : \u211d)) := by\n      funext y\n      rw [BohrMollerup.logGammaSeq]\n    rw [\u2190 heq] at hmain\n    exact hmain\n  have h := hasDerivAt_of_tendstoLocallyUniformlyOn isOpen_Ioi dpsiSeqR_tendstoLocallyUniformlyOn\n    hf hfg (Set.mem_Ioi.mpr hx)\n  exact h.deriv\n\n/-- \u03c8_real(x) := \u0393'(x)/\u0393(x) = DinfR(x) for x > 0. -/\nlemma psiReal_eq_DinfR {x : \u211d} (hx : 0 < x) :\n    deriv Real.Gamma x / Real.Gamma x = DinfR x := by\n  have h := deriv_log_Gamma_real hx\n  have hG : DifferentiableAt \u211d Real.Gamma x := by\n    apply Real.differentiableAt_Gamma\n    intro m hmeq\n    have hxx : (0 : \u211d) < x := hx\n    rw [hmeq] at hxx\n    have hm : (0 : \u211d) \u2264 (m : \u211d) := Nat.cast_nonneg m\n    linarith\n  have hG0 : Real.Gamma x \u2260 0 := (Real.Gamma_pos_of_pos hx).ne'\n  have hchain : deriv (Real.log \u2218 Real.Gamma) x = deriv Real.Gamma x / Real.Gamma x := by\n    have h1 : HasDerivAt Real.Gamma (deriv Real.Gamma x) x := hG.hasDerivAt\n    have h2 : HasDerivAt Real.log (Real.Gamma x)\u207b\u00b9 (Real.Gamma x) :=\n      Real.hasDerivAt_log hG0\n    have h3 := h2.comp x h1\n    have heq : (Real.log \u2218 Real.Gamma) = fun y => Real.log (Real.Gamma y) := rfl\n    rw [heq] at h3\n    rw [heq]\n    rw [h3.deriv]\n    field_simp [hG0]\n  rw [hchain] at h\n  exact h\n\n/-! ## 3. The complex series: summability, analyticity, cast bridge -/\n\n/-- The complex digamma series summand. -/\ndef dpsiTermC (s : \u2102) (m : \u2115) : \u2102 := 1 / ((m : \u2102) + 1) - 1 / (s + m + 1)\n\n/-- The complex digamma series: \u2212\u03b3 \u2212 1/s + \u03a3_{m\u22650} dpsiTermC s m. -/\ndef DinfC (s : \u2102) : \u2102 :=\n  -(Real.eulerMascheroniConstant : \u2102) - 1 / s + \u2211' m : \u2115, dpsiTermC s m\n\n/-- The domain: the ball of radius 1/2 around 1/2 (avoids 0, \u22121, \u22122, \u2026;\nconvex, contains the real segment (0,1)). -/\ndef dpsiDomain : Set \u2102 := Metric.ball ((1 : \u2102) / 2) (1 / 2)\n\nlemma dpsiDomain_convex : Convex \u211d dpsiDomain := convex_ball _ _\nlemma dpsiDomain_isOpen : IsOpen dpsiDomain := Metric.isOpen_ball\nlemma dpsiDomain_half : (1 : \u2102) / 2 \u2208 dpsiDomain :=\n  Metric.mem_ball_self (by norm_num : (0 : \u211d) < 1 / 2)\n\n/-- Points of dpsiDomain have positive real part. -/\nlemma dpsiDomain_re_pos {s : \u2102} (hs : s \u2208 dpsiDomain) : 0 < s.re := by\n  have h1 : \u2016s - (1 : \u2102) / 2\u2016 < 1 / 2 := by\n    have h := hs\n    rw [dpsiDomain, Metric.mem_ball, dist_eq_norm] at h\n    exact h\n  have h2 : |s.re - 1 / 2| \u2264 \u2016s - (1 : \u2102) / 2\u2016 := by\n    have e : s.re - 1 / 2 = (s - (1 : \u2102) / 2).re := by\n      simp [Complex.sub_re]\n    rw [e]\n    exact Complex.abs_re_le_norm _\n  have h3 : |s.re - 1 / 2| < 1 / 2 := lt_of_le_of_lt h2 h1\n  have h4 : -(1 / 2) < s.re - 1 / 2 := (abs_lt.mp h3).1\n  linarith\n\nlemma dpsiTermC_pole_free {s : \u2102} (hs : s \u2208 dpsiDomain) (m : \u2115) : s + m + 1 \u2260 0 := by\n  intro h\n  have hre : 0 < s.re := dpsiDomain_re_pos hs\n  have h2 : (s + (m : \u2102) + 1).re = 0 := by rw [h]; simp\n  simp only [Complex.add_re, Complex.one_re] at h2\n  have h3 : (\u2191m : \u2102).re = (m : \u211d) := by simp\n  rw [h3] at h2\n  have h4 : (0 : \u211d) \u2264 (m : \u211d) := Nat.cast_nonneg m\n  linarith\n\n/-- The summand in factored form: dpsiTermC s m = s/((m+1)(s+m+1)). -/\nlemma dpsiTermC_eq {s : \u2102} (m : \u2115) (hsm : s + m + 1 \u2260 0) :\n    dpsiTermC s m = s / ((\u2191m + 1) * (s + \u2191m + 1)) := by\n  have hm0 : ((m : \u2102) + 1) \u2260 0 := by\n    intro h\n    have hre : ((m : \u2102) + 1).re = 0 := by rw [h]; simp\n    simp [Complex.add_re, Complex.one_re] at hre\n    have : (0 : \u211d) \u2264 (m : \u211d) := Nat.cast_nonneg m\n    linarith\n  rw [dpsiTermC]\n  field_simp [hm0, hsm]\n  ring\n\n/-- \u2016(m : \u2102) + 1\u2016 = m + 1. -/\nlemma norm_natCast_add_one (m : \u2115) : \u2016((m : \u2102) + 1)\u2016 = (m : \u211d) + 1 := by\n  have e : ((m : \u2102) + 1) = \u2191((m : \u211d) + 1) := by push_cast; ring\n  rw [e, Complex.norm_real, Real.norm_eq_abs]\n  exact abs_of_nonneg (by positivity)\n\n/-- The complex series is summable on dpsiDomain. -/\nlemma dpsiTermC_summable {s : \u2102} (hs : s \u2208 dpsiDomain) : Summable (dpsiTermC s) := by\n  have hnorm : \u2200 m : \u2115, \u2016dpsiTermC s m\u2016 \u2264 \u2016s\u2016 / ((m : \u211d) + 1) ^ 2 := by\n    intro m\n    have hsm : s + m + 1 \u2260 0 := dpsiTermC_pole_free hs m\n    rw [dpsiTermC_eq m hsm]\n    rw [norm_div]\n    have hden : ((m : \u211d) + 1) * ((m : \u211d) + 1) \u2264 \u2016((m : \u2102) + 1) * (s + \u2191m + 1)\u2016 := by\n      rw [norm_mul, norm_natCast_add_one]\n      apply mul_le_mul_of_nonneg_left _ (by positivity : (0 : \u211d) \u2264 (m : \u211d) + 1)\n      have hre : 0 < s.re := dpsiDomain_re_pos hs\n      have h5 : s.re + m + 1 \u2264 \u2016s + \u2191m + 1\u2016 := by\n        have h6 : (s + \u2191m + 1).re = s.re + m + 1 := by\n          have h3 : (\u2191m : \u2102).re = (m : \u211d) := by simp\n          simp [Complex.add_re, Complex.one_re, h3]\n        rw [\u2190 h6]\n        exact Complex.re_le_norm _\n      linarith [h5]\n    have hpos : (0 : \u211d) < ((m : \u211d) + 1) * ((m : \u211d) + 1) := by positivity\n    calc \u2016s\u2016 / \u2016((m : \u2102) + 1) * (s + \u2191m + 1)\u2016 \u2264 \u2016s\u2016 / (((m : \u211d) + 1) * ((m : \u211d) + 1)) :=\n          div_le_div_of_nonneg_left (norm_nonneg _) hpos hden\n      _ = \u2016s\u2016 / ((m : \u211d) + 1) ^ 2 := by ring\n  exact Summable.of_norm_bounded (summable_div_add_one_sq \u2016s\u2016) hnorm\n\n/-! ## 4. Analyticity and the identity with Complex.digamma -/\n\n/-- The series converges uniformly on dpsiDomain (M-test, \u03a3 1/(m+1)\u00b2). -/\nlemma dpsiTermC_hasSumUniformlyOn :\n    HasSumUniformlyOn (fun m => fun s : \u2102 => dpsiTermC s m)\n      (fun s => \u2211' m : \u2115, dpsiTermC s m) dpsiDomain := by\n  apply HasSumUniformlyOn.of_norm_le_summable (summable_div_add_one_sq 1)\n  intro m s hs\n  have hsm : s + m + 1 \u2260 0 := dpsiTermC_pole_free hs m\n  have hre : 0 < s.re := dpsiDomain_re_pos hs\n  rw [dpsiTermC_eq m hsm, norm_div]\n  have hden : ((m : \u211d) + 1) * ((m : \u211d) + 1) \u2264 \u2016((m : \u2102) + 1) * (s + \u2191m + 1)\u2016 := by\n    rw [norm_mul, norm_natCast_add_one]\n    apply mul_le_mul_of_nonneg_left _ (by positivity : (0 : \u211d) \u2264 (m : \u211d) + 1)\n    have h5 : s.re + m + 1 \u2264 \u2016s + \u2191m + 1\u2016 := by\n      have h6 : (s + \u2191m + 1).re = s.re + m + 1 := by\n        have h3 : (\u2191m : \u2102).re = (m : \u211d) := by simp\n        simp [Complex.add_re, Complex.one_re, h3]\n      rw [\u2190 h6]\n      exact Complex.re_le_norm _\n    linarith [h5]\n  have hs1 : \u2016s\u2016 \u2264 1 := by\n    have h := hs\n    rw [dpsiDomain, Metric.mem_ball, dist_eq_norm] at h\n    have h12 : \u2016((1 : \u2102) / 2)\u2016 = 1 / 2 := by\n      rw [norm_div, norm_one]\n      norm_num\n    calc \u2016s\u2016 \u2264 \u2016s - (1 : \u2102) / 2\u2016 + \u2016((1 : \u2102) / 2)\u2016 := by\n          have e : s = (s - (1 : \u2102) / 2) + (1 : \u2102) / 2 := by ring\n          nth_rewrite 1 [e]\n          exact norm_add_le _ _\n      _ \u2264 1 / 2 + 1 / 2 := by linarith [h, h12]\n      _ = 1 := by ring\n  have hpos : (0 : \u211d) < ((m : \u211d) + 1) * ((m : \u211d) + 1) := by positivity\n  calc \u2016s\u2016 / \u2016((m : \u2102) + 1) * (s + \u2191m + 1)\u2016 \u2264 \u2016s\u2016 / (((m : \u211d) + 1) * ((m : \u211d) + 1)) :=\n        div_le_div_of_nonneg_left (norm_nonneg _) hpos hden\n    _ = \u2016s\u2016 / ((m : \u211d) + 1) ^ 2 := by ring\n    _ \u2264 1 / ((m : \u211d) + 1) ^ 2 :=\n        (div_le_div_iff_of_pos_right (by positivity : (0 : \u211d) < ((m : \u211d) + 1) ^ 2)).mpr hs1\n\n/-- The series function is differentiable on dpsiDomain (Weierstrass convergence). -/\nlemma dpsiTermC_tsum_differentiableOn :\n    DifferentiableOn \u2102 (fun s => \u2211' m : \u2115, dpsiTermC s m) dpsiDomain := by\n  have htend : TendstoLocallyUniformlyOn\n      (fun t : Finset \u2115 => fun s => \u2211 m \u2208 t, dpsiTermC s m)\n      (fun s => \u2211' m : \u2115, dpsiTermC s m) atTop dpsiDomain :=\n    TendstoUniformlyOn.tendstoLocallyUniformlyOn\n      (hasSumUniformlyOn_iff_tendstoUniformlyOn.mp dpsiTermC_hasSumUniformlyOn)\n  apply htend.differentiableOn _ dpsiDomain_isOpen\n  apply Filter.Eventually.of_forall\n  intro t s hs\n  rw [show (fun s => \u2211 m \u2208 t, dpsiTermC s m) = \u2211 m \u2208 t, (fun s => dpsiTermC s m) from by\n    funext s; simp [Finset.sum_apply]]\n  apply DifferentiableAt.differentiableWithinAt\n  apply DifferentiableAt.sum\n  intro m hm\n  have hsm : s + m + 1 \u2260 0 := dpsiTermC_pole_free hs m\n  have h1 : DifferentiableAt \u2102 (fun s : \u2102 => 1 / ((m : \u2102) + 1)) s := differentiableAt_const _\n  have h2 : DifferentiableAt \u2102 (fun s : \u2102 => 1 / (s + \u2191m + 1)) s := by\n    have h3 : DifferentiableAt \u2102 (fun s : \u2102 => s + \u2191m + 1) s :=\n      (differentiableAt_id.add (differentiableAt_const _)).add (differentiableAt_const _)\n    exact (differentiableAt_const (1 : \u2102)).div h3 hsm\n  exact h1.sub h2\n\n/-- DinfC is analytic on dpsiDomain (Weierstrass convergence theorem). -/\nlemma DinfC_analyticOn : AnalyticOnNhd \u2102 DinfC dpsiDomain := by\n  have hconst : DifferentiableOn \u2102 (fun s : \u2102 => -(Real.eulerMascheroniConstant : \u2102) - 1 / s)\n      dpsiDomain := by\n    intro s hs\n    have hs0 : s \u2260 0 := by\n      have h := dpsiDomain_re_pos hs\n      intro hsz\n      rw [hsz] at h\n      simp at h\n    have h1 : DifferentiableAt \u2102 (fun s : \u2102 => 1 / s) s :=\n      (differentiableAt_const (1 : \u2102)).div differentiableAt_id hs0\n    exact (differentiableAt_const _).sub h1 |>.differentiableWithinAt\n  have hfull : DifferentiableOn \u2102 DinfC dpsiDomain := by\n    have e : DinfC = (fun s : \u2102 => -(Real.eulerMascheroniConstant : \u2102) - 1 / s) +\n        (fun s => \u2211' m : \u2115, dpsiTermC s m) := by\n      funext s\n      rw [DinfC]\n      simp [Pi.add_apply]\n    rw [e]\n    exact hconst.add dpsiTermC_tsum_differentiableOn\n  exact hfull.analyticOnNhd dpsiDomain_isOpen\n\n/-- Complex.digamma is analytic on dpsiDomain (Gamma nonzero + differentiable there). -/\nlemma digamma_analyticOn : AnalyticOnNhd \u2102 Complex.digamma dpsiDomain := by\n  have hpole : \u2200 z \u2208 dpsiDomain, \u2200 m : \u2115, z \u2260 -(m : \u2102) := by\n    intro z hz m hmeq\n    have hre : 0 < z.re := dpsiDomain_re_pos hz\n    rw [hmeq] at hre\n    simp at hre\n    have hm : (0 : \u211d) \u2264 (m : \u211d) := Nat.cast_nonneg m\n    linarith\n  have hGammaAn : AnalyticOnNhd \u2102 Complex.Gamma dpsiDomain := by\n    apply DifferentiableOn.analyticOnNhd _ dpsiDomain_isOpen\n    intro z hz\n    exact (Complex.differentiableAt_Gamma z (hpole z hz)).differentiableWithinAt\n  have hdig : Complex.digamma = fun s => deriv Complex.Gamma s / Complex.Gamma s := by\n    funext s\n    rw [Complex.digamma_def, logDeriv_apply]\n  rw [hdig]\n  intro s hs\n  exact (hGammaAn.deriv s hs).div (hGammaAn s hs)\n    (Complex.Gamma_ne_zero (hpole s hs))\n\n/-- The cast bridge: DinfC(\u2191x) = \u2191(DinfR x) for 0 < x. -/\nlemma DinfC_ofReal {x : \u211d} (_hx : 0 < x) : DinfC (\u2191x) = \u2191(DinfR x) := by\n  rw [DinfC, DinfR]\n  push_cast\n  congr 1\n  apply tsum_congr\n  intro m\n  rw [dpsiTermR, dpsiTermC]\n  push_cast\n  ring\n\n/-- Complex.digamma agrees with DinfC on the real segment inside the domain. -/\nlemma digamma_eq_DinfC_ofReal {x : \u211d} (hx : x \u2208 Set.Ioo 0 1) :\n    Complex.digamma (\u2191x) = DinfC (\u2191x) := by\n  have hx0 : 0 < x := hx.1\n  rw [DinfC_ofReal hx0]\n  -- digamma \u2191x = deriv Gamma \u2191x / Gamma \u2191x = \u2191(\u0393'(x)/\u0393(x)) = \u2191(DinfR x)\n  have hGx : Complex.Gamma (\u2191x : \u2102) = \u2191(Real.Gamma x) := Complex.Gamma_ofReal x\n  have hderiv : deriv Complex.Gamma (\u2191x : \u2102) = \u2191(deriv Real.Gamma x) := by\n    have h2 : HasDerivAt Real.Gamma (deriv Real.Gamma x) x := by\n      have hd : DifferentiableAt \u211d Real.Gamma x := by\n        apply Real.differentiableAt_Gamma\n        intro m hmeq\n        rw [hmeq] at hx0\n        simp at hx0\n        have hm : (0 : \u211d) \u2264 (m : \u211d) := Nat.cast_nonneg m\n        linarith\n      exact hd.hasDerivAt\n    have h1 : HasDerivAt (fun y : \u211d => (\u2191(Real.Gamma y) : \u2102)) (\u2191(deriv Real.Gamma x) : \u2102) x := by\n      have h3 := Complex.ofRealCLM.hasFDerivAt.comp_hasDerivAt x h2\n      rw [Complex.ofRealCLM_apply] at h3\n      have heq : (Complex.ofRealCLM \u2218 Real.Gamma) = fun y : \u211d => \u2191(Real.Gamma y) := by\n        funext y\n        rw [Function.comp_apply, Complex.ofRealCLM_apply]\n      rw [heq] at h3\n      exact h3\n    -- deriv (Gamma \u2218 ofReal) x = deriv Gamma \u2191x \u00b7 1\n    have h6 : deriv (fun y : \u211d => Complex.Gamma (\u2191y)) x = deriv Complex.Gamma (\u2191x : \u2102) := by\n      have h7 : HasDerivAt (fun y : \u211d => (\u2191y : \u2102)) (1 : \u2102) x := by\n        have h8 := Complex.ofRealCLM.hasDerivAt (x := x)\n        rw [Complex.ofRealCLM_apply] at h8\n        exact h8\n      have h9 : HasDerivAt Complex.Gamma (deriv Complex.Gamma (\u2191x : \u2102)) (\u2191x : \u2102) := by\n        apply (Complex.differentiableAt_Gamma _ _).hasDerivAt\n        intro m hmeq\n        have h2 : (x : \u211d) = -(m : \u211d) := by\n          have h3 : (\u2191x : \u2102).re = (-(m : \u2102)).re := by rw [hmeq]\n          simp at h3\n          exact h3\n        have hm : (0 : \u211d) \u2264 (m : \u211d) := Nat.cast_nonneg m\n        linarith\n      have h10 := h9.comp x h7\n      -- comp gives deriv Gamma \u2191x * 1\n      rw [mul_one] at h10\n      have heq : (Complex.Gamma \u2218 fun y : \u211d => (\u2191y : \u2102)) = fun y : \u211d => Complex.Gamma (\u2191y) := rfl\n      rw [heq] at h10\n      exact h10.deriv\n    have h5 : (fun y : \u211d => Complex.Gamma (\u2191y)) = fun y : \u211d => (\u2191(Real.Gamma y) : \u2102) :=\n      funext fun y => Complex.Gamma_ofReal y\n    have h1d : deriv (fun y : \u211d => (\u2191(Real.Gamma y) : \u2102)) x = \u2191(deriv Real.Gamma x) := h1.deriv\n    rw [\u2190 h5] at h1d\n    rw [h6] at h1d\n    exact h1d\n  rw [Complex.digamma_def, logDeriv_apply, hderiv, hGx]\n  rw [\u2190 Complex.ofReal_div]\n  congr 1\n  exact psiReal_eq_DinfR hx0\n\n/-! ## 5. Congruence helpers and the inverse-power iterated derivative -/\n\n/-- If f = g on a nbd of x, then deriv f = deriv g on a (smaller) nbd of x. -/\nlemma eventuallyEq_deriv {f g : \u2102 \u2192 \u2102} {x : \u2102} (h : f =\u1da0[\ud835\udcdd x] g) :\n    deriv f =\u1da0[\ud835\udcdd x] deriv g := by\n  have hS : {y | f y = g y} \u2208 \ud835\udcdd x := h\n  have hxint : x \u2208 interior {y | f y = g y} := by\n    rw [mem_interior_iff_mem_nhds]\n    exact hS\n  filter_upwards [IsOpen.mem_nhds isOpen_interior hxint] with y hy\n  have h3 : f =\u1da0[\ud835\udcdd y] g := by\n    apply Filter.eventually_of_mem (IsOpen.mem_nhds isOpen_interior hy)\n    intro z hz\n    have h4 : z \u2208 {y | f y = g y} := interior_subset hz\n    exact h4\n  exact h3.deriv_eq\n\nlemma eventuallyEq_iteratedDeriv {f g : \u2102 \u2192 \u2102} {x : \u2102} (h : f =\u1da0[\ud835\udcdd x] g) (n : \u2115) :\n    iteratedDeriv n f =\u1da0[\ud835\udcdd x] iteratedDeriv n g := by\n  induction n with\n  | zero => simpa [iteratedDeriv_zero] using h\n  | succ n ih =>\n    rw [iteratedDeriv_succ, iteratedDeriv_succ]\n    exact eventuallyEq_deriv ih\n\n/-- Pointwise congruence of iteratedDeriv under eventual equality. -/\nlemma iteratedDeriv_congr_of_eventuallyEq {f g : \u2102 \u2192 \u2102} {x : \u2102} (h : f =\u1da0[\ud835\udcdd x] g) (n : \u2115) :\n    iteratedDeriv n f x = iteratedDeriv n g x :=\n  (eventuallyEq_iteratedDeriv h n).self_of_nhds\n\n/-- The iterated derivative of s \u21a6 \u2212(s+c)\u207b\u00b9:\n(d/ds)^k [\u2212(s+c)\u207b\u00b9] = \u2212(\u22121)^k\u00b7k!\u00b7(s+c)^{\u2212(k+1)}. -/\nlemma iteratedDeriv_neg_zpow_neg_one_add (k : \u2115) (c : \u2102) {s : \u2102} (hs : s + c \u2260 0) :\n    iteratedDeriv k (fun s : \u2102 => -((s + c) ^ (-1 : \u2124))) s =\n      -((-1 : \u2102)) ^ k * (k ! : \u2102) * (s + c) ^ (-(k : \u2124) - 1) := by\n  induction k generalizing s with\n  | zero =>\n    simp\n  | succ k ih =>\n    rw [iteratedDeriv_succ]\n    -- replace iteratedDeriv k F by its closed form on a nbd of s\n    have hopen : IsOpen {t : \u2102 | t + c \u2260 0} := by\n      have hcont : Continuous (fun t : \u2102 => t + c) := continuous_id.add continuous_const\n      exact isOpen_compl_singleton.preimage hcont\n    have hev : (fun t => iteratedDeriv k (fun u : \u2102 => -((u + c) ^ (-1 : \u2124))) t) =\u1da0[\ud835\udcdd s]\n        (fun t => -((-1 : \u2102)) ^ k * (k ! : \u2102) * (t + c) ^ (-(k : \u2124) - 1)) := by\n      filter_upwards [hopen.mem_nhds hs] with t ht\n      exact ih ht\n    rw [hev.deriv_eq]\n    -- compute deriv of the closed form at s\n    have h1 : HasDerivAt (fun t : \u2102 => (t + c) ^ (-(k : \u2124) - 1))\n        (((-(k : \u2124) - 1 : \u2124) : \u2102) * (s + c) ^ (-(k : \u2124) - 1 - 1)) s := by\n      have h2 : HasDerivAt (fun t : \u2102 => t + c) 1 s := by\n        simpa using (hasDerivAt_id s).add_const c\n      have h3 := (hasDerivAt_zpow (-(k : \u2124) - 1) (s + c) (Or.inl hs)).comp s h2\n      rw [mul_one] at h3\n      have heq : ((fun x : \u2102 => x ^ (-(k : \u2124) - 1)) \u2218 fun t : \u2102 => t + c) =\n          fun t => (t + c) ^ (-(k : \u2124) - 1) := rfl\n      rw [heq] at h3\n      exact h3\n    have h4 : deriv (fun t : \u2102 => -((-1 : \u2102)) ^ k * (k ! : \u2102) * (t + c) ^ (-(k : \u2124) - 1)) s =\n        -((-1 : \u2102)) ^ k * (k ! : \u2102) *\n          (((-(k : \u2124) - 1 : \u2124) : \u2102) * (s + c) ^ (-(k : \u2124) - 1 - 1)) :=\n      (h1.const_mul _).deriv\n    rw [h4]\n    -- normalize the exponents to \u2212(k:\u2124)\u22122, then the constants\n    have hexp1 : (-(k : \u2124) - 1 - 1 : \u2124) = (-(k : \u2124) - 2 : \u2124) := by ring\n    have hexp2 : (-((k + 1 : \u2115) : \u2124) - 1 : \u2124) = (-(k : \u2124) - 2 : \u2124) := by push_cast; ring\n    rw [hexp1, hexp2]\n    have hconst : ((-(k : \u2124) - 1 : \u2124) : \u2102) = -((k : \u2102) + 1) := by push_cast; ring\n    have hfact : (((k + 1) ! : \u2115) : \u2102) = ((k : \u2102) + 1) * (k ! : \u2102) := by\n      rw [Nat.factorial_succ]\n      push_cast\n      ring\n    rw [hconst, hfact, pow_succ]\n    ring\n\n/-! ## 6. The identity digamma = DinfC on the domain (identity principle) -/\n\n/-- digamma and DinfC agree on dpsiDomain. -/\nlemma digamma_eq_DinfC_on : Set.EqOn Complex.digamma DinfC dpsiDomain := by\n  apply AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq digamma_analyticOn DinfC_analyticOn\n    dpsiDomain_convex.isPreconnected dpsiDomain_half\n  rw [frequently_iff]\n  intro U hU\n  rw [mem_nhdsWithin_iff_exists_mem_nhds_inter] at hU\n  obtain \u27e8V, hV, hVU\u27e9 := hU\n  rw [Metric.mem_nhds_iff] at hV\n  obtain \u27e8\u03b4, h\u03b4, h\u03b4V\u27e9 := hV\n  have hpos : (0 : \u211d) < min (\u03b4 / 2) (1 / 4) := lt_min (by positivity) (by norm_num)\n  have hxI : (1 / 2 : \u211d) + min (\u03b4 / 2) (1 / 4) \u2208 Set.Ioo 0 1 := by\n    constructor\n    \u00b7 linarith\n    \u00b7 have h1 : min (\u03b4 / 2) (1 / 4) \u2264 1 / 4 := min_le_right _ _\n      linarith\n  refine \u27e8\u2191((1 / 2 : \u211d) + min (\u03b4 / 2) (1 / 4)), hVU ?_, ?_\u27e9\n  \u00b7 constructor\n    \u00b7 apply h\u03b4V\n      rw [Metric.mem_ball, dist_eq_norm]\n      have e : (\u2191((1 / 2 : \u211d) + min (\u03b4 / 2) (1 / 4)) : \u2102) - (1 : \u2102) / 2 =\n          \u2191(min (\u03b4 / 2) (1 / 4)) := by push_cast; ring\n      rw [e, Complex.norm_real, Real.norm_eq_abs, abs_of_nonneg hpos.le]\n      calc min (\u03b4 / 2) (1 / 4) \u2264 \u03b4 / 2 := min_le_left _ _\n        _ < \u03b4 := by linarith [h\u03b4]\n    \u00b7 intro hcontra\n      have h2 : (1 / 2 : \u211d) + min (\u03b4 / 2) (1 / 4) = 1 / 2 := by\n        have h3 : (\u2191((1 / 2 : \u211d) + min (\u03b4 / 2) (1 / 4)) : \u2102) = (1 : \u2102) / 2 :=\n          Set.mem_singleton_iff.mp hcontra\n        have h4 : ((1 : \u2102) / 2) = \u2191((1 : \u211d) / 2) := by push_cast; ring\n        rw [h4] at h3\n        exact Complex.ofReal_inj.mp h3\n      linarith\n  \u00b7 exact digamma_eq_DinfC_ofReal hxI\n\n/-! ## 7. The iterated derivatives at 1/2 -/\n\n/-- The shifted p-series is summable for any exponent \u2265 2. -/\nlemma summable_div_add_one_pow (c : \u211d) (p : \u2115) (hp : 2 \u2264 p) :\n    Summable (fun m : \u2115 => c / ((m : \u211d) + 1) ^ p) := by\n  have h := Real.summable_one_div_nat_pow.mpr (show 1 < p by omega)\n  have h2 : Summable (fun m : \u2115 => (1 : \u211d) / ((m : \u211d) + 1) ^ p) := by\n    have h3 : Summable (fun m : \u2115 => (1 : \u211d) / ((m + 1 : \u2115) : \u211d) ^ p) :=\n      (summable_nat_add_iff 1).mpr h\n    apply h3.congr\n    intro m\n    push_cast\n    ring_nf\n  exact (h2.mul_left c).congr (fun m => by ring)\n\n/-- The one-div form of the zpow iterated derivative. -/\nlemma iteratedDeriv_neg_one_div_add_const (k : \u2115) (c : \u2102) {s : \u2102} (hs : s + c \u2260 0) :\n    iteratedDeriv k (fun s : \u2102 => -(1 / (s + c))) s =\n      -((-1 : \u2102)) ^ k * (k ! : \u2102) * (s + c) ^ (-(k : \u2124) - 1) := by\n  have e : (fun s : \u2102 => -(1 / (s + c))) = fun s => -((s + c) ^ (-1 : \u2124)) := by\n    funext s\n    rw [zpow_neg_one, one_div]\n  rw [e]\n  exact iteratedDeriv_neg_zpow_neg_one_add k c hs\n\n/-- The k-th iterated derivative (k \u2265 1) of a summand on the domain. -/\nlemma iteratedDerivWithin_dpsiTermC (k : \u2115) (hk : 1 \u2264 k) (m : \u2115) {s : \u2102}\n    (hs : s \u2208 dpsiDomain) :\n    iteratedDerivWithin k (fun s : \u2102 => dpsiTermC s m) dpsiDomain s =\n      -((-1 : \u2102)) ^ k * (k ! : \u2102) * (s + \u2191m + 1) ^ (-(k : \u2124) - 1) := by\n  have hsm : s + m + 1 \u2260 0 := dpsiTermC_pole_free hs m\n  rw [iteratedDerivWithin_of_isOpen dpsiDomain_isOpen hs]\n  have heq : (fun s : \u2102 => dpsiTermC s m) =\n      (fun s : \u2102 => 1 / ((m : \u2102) + 1)) + fun s : \u2102 => -(1 / (s + \u2191m + 1)) := by\n    funext s\n    simp only [Pi.add_apply]\n    rw [dpsiTermC]\n    ring\n  rw [heq]\n  have hcf : ContDiffAt \u2102 k (fun s : \u2102 => 1 / ((m : \u2102) + 1)) s := contDiff_const.contDiffAt\n  have hcg : ContDiffAt \u2102 k (fun s : \u2102 => -(1 / (s + \u2191m + 1))) s := by\n    have h2 : AnalyticAt \u2102 (fun s : \u2102 => s + \u2191m + 1) s :=\n      (analyticAt_id.add analyticAt_const).add analyticAt_const\n    have h3 : AnalyticAt \u2102 (fun s : \u2102 => 1 / (s + \u2191m + 1)) s :=\n      analyticAt_const.div h2 hsm\n    exact h3.neg.contDiffAt\n  rw [iteratedDeriv_add hcf hcg]\n  rw [iteratedDeriv_const, if_neg (by omega : k \u2260 0)]\n  have h4 : iteratedDeriv k (fun s : \u2102 => -(1 / (s + \u2191m + 1))) s =\n      -((-1 : \u2102)) ^ k * (k ! : \u2102) * (s + \u2191m + 1) ^ (-(k : \u2124) - 1) := by\n    have h5 : (fun s : \u2102 => -(1 / (s + \u2191m + 1))) =\n        fun s : \u2102 => -(1 / (s + ((m : \u2102) + 1))) := by\n      funext s\n      rw [add_assoc]\n    rw [h5]\n    rw [iteratedDeriv_neg_one_div_add_const k ((m : \u2102) + 1) (by rw [\u2190 add_assoc]; exact hsm)]\n    rw [\u2190 add_assoc]\n  rw [h4]\n  rw [zero_add]\n\n/-- The k-th derivative family (k \u2265 1) is summable locally uniformly on the domain. -/\nlemma dpsiTermC_deriv_summableLocallyUniformlyOn (k : \u2115) (hk : 1 \u2264 k) :\n    SummableLocallyUniformlyOn\n      (fun m => (iteratedDerivWithin k (fun s : \u2102 => dpsiTermC s m) dpsiDomain)) dpsiDomain := by\n  apply SummableLocallyUniformlyOn_of_locally_bounded dpsiDomain_isOpen\n  intro K hK hKc\n  refine \u27e8fun m => (k ! : \u211d) / ((m : \u211d) + 1) ^ (k + 1),\n    summable_div_add_one_pow _ (k + 1) (by omega), fun m s hs => ?_\u27e9\n  have hsd : s \u2208 dpsiDomain := hK hs\n  rw [iteratedDerivWithin_dpsiTermC k hk m hsd]\n  have hre : 0 < s.re := dpsiDomain_re_pos hsd\n  have hnormS : (m : \u211d) + 1 \u2264 \u2016s + \u2191m + 1\u2016 := by\n    have h6 : (s + \u2191m + 1).re = s.re + m + 1 := by\n      have h3 : (\u2191m : \u2102).re = (m : \u211d) := by simp\n      simp [Complex.add_re, Complex.one_re, h3]\n    have h5 : s.re + m + 1 \u2264 \u2016s + \u2191m + 1\u2016 := by\n      rw [\u2190 h6]\n      exact Complex.re_le_norm _\n    linarith [h5, hre]\n  rw [norm_mul, norm_mul]\n  have hsign : \u2016-((-1 : \u2102)) ^ k\u2016 = 1 := by\n    have h7 : \u2016((-1 : \u2102))\u2016 = 1 := by rw [norm_neg, norm_one]\n    rw [norm_neg, norm_pow, h7, one_pow]\n  rw [hsign, one_mul, RCLike.norm_natCast, norm_zpow]\n  rw [show (-(k : \u2124) - 1 : \u2124) = -(((k + 1 : \u2115) : \u2124)) by push_cast; ring, zpow_neg, zpow_natCast]\n  show (\u2191k ! : \u211d) * (\u2016s + \u2191m + 1\u2016 ^ (k + 1))\u207b\u00b9 \u2264 (k ! : \u211d) / ((m : \u211d) + 1) ^ (k + 1)\n  rw [div_eq_mul_inv]\n  apply mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _)\n  rw [\u2190 one_div, \u2190 one_div]\n  apply one_div_le_one_div_of_le (by positivity)\n  exact pow_le_pow_left\u2080 (by positivity : (0 : \u211d) \u2264 (m : \u211d) + 1) hnormS (k + 1)\n\n/-- The iterated derivative of the series function at 1/2 (termwise). -/\nlemma iteratedDerivWithin_tsum_dpsiTermC (k : \u2115) (hk : 1 \u2264 k) :\n    iteratedDerivWithin k (fun s : \u2102 => \u2211' m : \u2115, dpsiTermC s m) dpsiDomain ((1 : \u2102) / 2) =\n      \u2211' m : \u2115, -((-1 : \u2102)) ^ k * (k ! : \u2102) * ((1 / 2 : \u2102) + \u2191m + 1) ^ (-(k : \u2124) - 1) := by\n  rw [iteratedDerivWithin_tsum k dpsiDomain_isOpen dpsiDomain_half\n    (fun s hs => dpsiTermC_summable hs)\n    (fun j hj1 _ => dpsiTermC_deriv_summableLocallyUniformlyOn j hj1)\n    ?_]\n  \u00b7 apply tsum_congr\n    intro m\n    exact iteratedDerivWithin_dpsiTermC k hk m dpsiDomain_half\n  \u00b7 intro n j r hjm hr\n    rcases Nat.eq_zero_or_pos j with hj0 | hj0\n    \u00b7 subst hj0\n      rw [iteratedDerivWithin_zero]\n      have hsm : r + n + 1 \u2260 0 := dpsiTermC_pole_free hr n\n      have heq : (fun s : \u2102 => dpsiTermC s n) = fun s => 1 / ((n : \u2102) + 1) - 1 / (s + \u2191n + 1) := by\n        funext s; rw [dpsiTermC]\n      rw [heq]\n      apply DifferentiableAt.sub (differentiableAt_const _)\n      have h3 : DifferentiableAt \u2102 (fun s : \u2102 => s + \u2191n + 1) r :=\n        (differentiableAt_id.add (differentiableAt_const _)).add (differentiableAt_const _)\n      exact (differentiableAt_const (1 : \u2102)).div h3 hsm\n    \u00b7 have h5 : (fun r => iteratedDerivWithin j (fun z : \u2102 => dpsiTermC z n) dpsiDomain r) =\u1da0[\ud835\udcdd r]\n          fun r => -((-1 : \u2102)) ^ j * (j ! : \u2102) * (r + \u2191n + 1) ^ (-(j : \u2124) - 1) := by\n        filter_upwards [dpsiDomain_isOpen.mem_nhds hr] with t ht\n        exact iteratedDerivWithin_dpsiTermC j (by omega) n ht\n      apply h5.differentiableAt_iff.mpr\n      have hsm : r + n + 1 \u2260 0 := dpsiTermC_pole_free hr n\n      have h4 : DifferentiableAt \u2102 (fun s : \u2102 => s + \u2191n + 1) r :=\n        (differentiableAt_id.add (differentiableAt_const _)).add (differentiableAt_const _)\n      have h6 : DifferentiableAt \u2102 (fun s : \u2102 => (s + \u2191n + 1) ^ (-(j : \u2124) - 1)) r := by\n        have h7 := ((hasDerivAt_zpow (-(j : \u2124) - 1) (r + \u2191n + 1) (Or.inl hsm)).differentiableAt).comp r h4\n        have heq : ((fun x : \u2102 => x ^ (-(j : \u2124) - 1)) \u2218 fun s : \u2102 => s + \u2191n + 1) =\n            fun s : \u2102 => (s + \u2191n + 1) ^ (-(j : \u2124) - 1) := rfl\n        rw [heq] at h7\n        exact h7\n      exact (differentiableAt_const _).mul h6\n\n\n/-! ## 9. The values at 1/2 and the transfer to digamma -/\n\n/-- The (1/2 + m)-power series is summable (norm \u2264 2^{k+1}/(m+1)^{k+1}). -/\nlemma summable_zpow_half_add_nat (k : \u2115) (hk : 1 \u2264 k) :\n    Summable (fun m : \u2115 => ((1 / 2 : \u2102) + \u2191m) ^ (-(k : \u2124) - 1)) := by\n  apply Summable.of_norm_bounded (summable_div_add_one_pow (2 ^ (k + 1)) (k + 1) (by omega))\n  intro m\n  have hpos : (0 : \u211d) < (m : \u211d) + 1 / 2 := by positivity\n  have h1 : \u2016((1 / 2 : \u2102) + \u2191m)\u2016 = (m : \u211d) + 1 / 2 := by\n    have e : ((1 / 2 : \u2102) + \u2191m) = \u2191((m : \u211d) + 1 / 2) := by push_cast; ring\n    rw [e, Complex.norm_real, Real.norm_eq_abs, abs_of_nonneg hpos.le]\n  rw [norm_zpow, h1]\n  rw [show (-(k : \u2124) - 1 : \u2124) = -(((k + 1 : \u2115) : \u2124)) by push_cast; ring, zpow_neg, zpow_natCast]\n  rw [\u2190 one_div]\n  show (1 : \u211d) / ((m : \u211d) + 1 / 2) ^ (k + 1) \u2264 2 ^ (k + 1) / ((m : \u211d) + 1) ^ (k + 1)\n  rw [div_le_div_iff\u2080 (by positivity : (0 : \u211d) < ((m : \u211d) + 1 / 2) ^ (k + 1))\n    (by positivity : (0 : \u211d) < ((m : \u211d) + 1) ^ (k + 1))]\n  rw [one_mul]\n  rw [show (2 : \u211d) ^ (k + 1) * ((m : \u211d) + 1 / 2) ^ (k + 1) =\n    (2 * ((m : \u211d) + 1 / 2)) ^ (k + 1) by rw [mul_pow]]\n  apply pow_le_pow_left\u2080 (by positivity : (0 : \u211d) \u2264 (m : \u211d) + 1)\n  ring_nf\n  linarith [Nat.cast_nonneg (\u03b1 := \u211d) m]\n\n/-- The polygamma values of DinfC at 1/2 (j \u2265 1). -/\nlemma iteratedDeriv_DinfC_half (k : \u2115) (hk : 1 \u2264 k) :\n    iteratedDeriv k DinfC ((1 : \u2102) / 2) =\n      ((-1 : \u2102)) ^ (k + 1) * (k ! : \u2102) * \u2211' m : \u2115, ((1 / 2 : \u2102) + \u2191m) ^ (-(k : \u2124) - 1) := by\n  have hsign : \u2200 k : \u2115, -((-1 : \u2102)) ^ k = (-1 : \u2102) ^ (k + 1) := fun k => by\n    rw [pow_succ]; ring\n  have hsplit : DinfC = (fun s : \u2102 => -(Real.eulerMascheroniConstant : \u2102) - 1 / s) +\n      (fun s => \u2211' m : \u2115, dpsiTermC s m) := by\n    funext s\n    rw [DinfC]\n    simp [Pi.add_apply]\n  rw [hsplit]\n  have hcfA : ContDiffAt \u2102 k (fun s : \u2102 => -(Real.eulerMascheroniConstant : \u2102) - 1 / s)\n      ((1 : \u2102) / 2) := by\n    have h1 : AnalyticAt \u2102 (fun s : \u2102 => 1 / s) ((1 : \u2102) / 2) :=\n      analyticAt_const.div analyticAt_id (by norm_num)\n    exact (analyticAt_const.sub h1).contDiffAt\n  have hcfB : ContDiffAt \u2102 k (fun s => \u2211' m : \u2115, dpsiTermC s m) ((1 : \u2102) / 2) := by\n    have h2 : AnalyticOnNhd \u2102 (fun s => \u2211' m : \u2115, dpsiTermC s m) dpsiDomain :=\n      dpsiTermC_tsum_differentiableOn.analyticOnNhd dpsiDomain_isOpen\n    exact (h2 _ dpsiDomain_half).contDiffAt\n  rw [iteratedDeriv_add hcfA hcfB]\n  have hA : iteratedDeriv k (fun s : \u2102 => -(Real.eulerMascheroniConstant : \u2102) - 1 / s)\n      ((1 : \u2102) / 2) = ((-1 : \u2102)) ^ (k + 1) * (k ! : \u2102) * ((1 : \u2102) / 2) ^ (-(k : \u2124) - 1) := by\n    have heq : (fun s : \u2102 => -(Real.eulerMascheroniConstant : \u2102) - 1 / s) =\n        (fun _ : \u2102 => -(Real.eulerMascheroniConstant : \u2102)) + fun s => -(1 / (s + 0)) := by\n      funext s\n      simp [Pi.add_apply]\n      ring\n    rw [heq]\n    have hcf1 : ContDiffAt \u2102 k (fun _ : \u2102 => -(Real.eulerMascheroniConstant : \u2102)) ((1 : \u2102) / 2) :=\n      contDiff_const.contDiffAt\n    have hcf2 : ContDiffAt \u2102 k (fun s : \u2102 => -(1 / (s + 0))) ((1 : \u2102) / 2) := by\n      have h2 : AnalyticAt \u2102 (fun s : \u2102 => s + 0) ((1 : \u2102) / 2) :=\n        analyticAt_id.add analyticAt_const\n      have h3 : AnalyticAt \u2102 (fun s : \u2102 => 1 / (s + 0)) ((1 : \u2102) / 2) :=\n        analyticAt_const.div h2 (by simp)\n      exact h3.neg.contDiffAt\n    rw [iteratedDeriv_add hcf1 hcf2]\n    rw [iteratedDeriv_const, if_neg (by omega : k \u2260 0)]\n    rw [iteratedDeriv_neg_one_div_add_const k 0 (by simp)]\n    rw [add_zero, zero_add, hsign]\n  have hB : iteratedDeriv k (fun s => \u2211' m : \u2115, dpsiTermC s m) ((1 : \u2102) / 2) =\n      ((-1 : \u2102)) ^ (k + 1) * (k ! : \u2102) * \u2211' m : \u2115, ((1 / 2 : \u2102) + \u2191m + 1) ^ (-(k : \u2124) - 1) := by\n    rw [\u2190 iteratedDerivWithin_of_isOpen dpsiDomain_isOpen dpsiDomain_half]\n    rw [iteratedDerivWithin_tsum_dpsiTermC k hk]\n    rw [tsum_mul_left]\n    rw [hsign]\n  rw [hA, hB]\n  rw [\u2190 mul_add]\n  congr 2\n  have hsum := summable_zpow_half_add_nat k hk\n  conv_rhs => rw [hsum.tsum_eq_zero_add]\n  have e0 : ((1 / 2 : \u2102) + ((0 : \u2115) : \u2102)) ^ (-(k : \u2124) - 1) = ((1 : \u2102) / 2) ^ (-(k : \u2124) - 1) := by\n    simp\n  rw [e0]\n  apply add_left_cancel_iff.mpr\n  apply tsum_congr\n  intro m\n  push_cast\n  ring\n\n/-- The polygamma values of Complex.digamma at 1/2 (j \u2265 1). -/\nlemma iteratedDeriv_digamma_half (j : \u2115) (hj : 1 \u2264 j) :\n    iteratedDeriv j Complex.digamma ((1 : \u2102) / 2) =\n      ((-1 : \u2102)) ^ (j + 1) * (j ! : \u2102) * \u2211' m : \u2115, ((1 / 2 : \u2102) + \u2191m) ^ (-(j : \u2124) - 1) := by\n  have hev : Complex.digamma =\u1da0[\ud835\udcdd ((1 : \u2102) / 2)] DinfC := by\n    apply Filter.eventually_of_mem (dpsiDomain_isOpen.mem_nhds dpsiDomain_half)\n    intro z hz\n    exact digamma_eq_DinfC_on hz\n  rw [iteratedDeriv_congr_of_eventuallyEq hev]\n  exact iteratedDeriv_DinfC_half j hj\n\n/-- The odd-shift equivalence: m \u21a6 2m+3 from \u2115 to {m odd, m \u2265 3}. -/\ndef oddGeThreeEquiv : \u2115 \u2243 {m : \u2115 // Odd m \u2227 3 \u2264 m} where\n  toFun m := \u27e82 * m + 3, by\n    constructor\n    \u00b7 exact Nat.odd_iff.mpr (by omega)\n    \u00b7 omega\u27e9\n  invFun := fun \u27e8m, _\u27e9 => (m - 3) / 2\n  left_inv m := by simp\n  right_inv := fun \u27e8m, hm\u27e9 => by\n    obtain \u27e8hodd, h3\u27e9 := hm\n    rw [Nat.odd_iff] at hodd\n    apply Subtype.ext\n    simp only []\n    omega\n\n/-- The series over odd m \u2265 3 of m^{-(j+1)} is summable (real, the\nlagariasA tail's summand family). -/\nlemma summable_odd_tail_inv_pow (j : \u2115) (hj : 1 \u2264 j) :\n    Summable (fun m : {m : \u2115 // Odd m \u2227 3 \u2264 m} => (1 / ((m : \u211d) : \u211d)) ^ (j + 1)) := by\n  have h := oddSlice_summable (j + 1) (by omega)\n  apply h.congr\n  intro m\n  rw [div_pow, one_pow]\n\n/-- The reindexing: \u03a3_{m\u22650} (2m+1)^{-(j+1)} = lagariasA (j+1) (as \u2102). -/\nlemma tsum_two_mul_add_one_inv_pow (j : \u2115) (hj : 1 \u2264 j) :\n    (\u2211' m : \u2115, ((2 : \u2102) * \u2191m + 1) ^ (-(j : \u2124) - 1)) = (lagariasA (j + 1) : \u211d) := by\n  -- peel m = 0 (value 1), shift, then the odd\u22653 equiv\n  have hsumm : Summable (fun m : \u2115 => ((2 : \u2102) * \u2191m + 1) ^ (-(j : \u2124) - 1)) := by\n    apply Summable.of_norm_bounded (summable_div_add_one_pow (4 ^ (j + 1)) (j + 1) (by omega))\n    intro m\n    have hpos : (0 : \u211d) < 2 * (m : \u211d) + 1 := by positivity\n    have h1 : \u2016((2 : \u2102) * \u2191m + 1)\u2016 = 2 * (m : \u211d) + 1 := by\n      have e : ((2 : \u2102) * \u2191m + 1) = \u2191(2 * (m : \u211d) + 1) := by push_cast; ring\n      rw [e, Complex.norm_real, Real.norm_eq_abs, abs_of_nonneg hpos.le]\n    rw [norm_zpow, h1]\n    rw [show (-(j : \u2124) - 1 : \u2124) = -(((j + 1 : \u2115) : \u2124)) by push_cast; ring, zpow_neg, zpow_natCast]\n    rw [\u2190 one_div]\n    rw [div_le_div_iff\u2080 (by positivity : (0 : \u211d) < (2 * (m : \u211d) + 1) ^ (j + 1))\n      (by positivity : (0 : \u211d) < ((m : \u211d) + 1) ^ (j + 1))]\n    rw [one_mul]\n    rw [show (4 : \u211d) ^ (j + 1) * (2 * (m : \u211d) + 1) ^ (j + 1) =\n      (4 * (2 * (m : \u211d) + 1)) ^ (j + 1) by rw [mul_pow]]\n    apply pow_le_pow_left\u2080 (by positivity : (0 : \u211d) \u2264 (m : \u211d) + 1)\n    linarith [Nat.cast_nonneg (\u03b1 := \u211d) m]\n  rw [hsumm.tsum_eq_zero_add]\n  have hf0 : ((2 : \u2102) * ((0 : \u2115) : \u2102) + 1) ^ (-(j : \u2124) - 1) = 1 := by simp\n  rw [hf0]\n  -- the tail: \u03a3_{m\u22650} (2\u2191m+3)^{-(j+1)} = \u03a3_{m' odd \u2265 3} (\u2191m')^{-(j+1)}\n  have heq2 : \u2200 m : \u2115, ((2 : \u2102) * \u2191(m + 1) + 1) ^ (-(j : \u2124) - 1) =\n      ((2 : \u2102) * \u2191m + 3) ^ (-(j : \u2124) - 1) := fun m => by push_cast; ring_nf\n  rw [tsum_congr heq2]\n  have heq3 : (fun m : \u2115 => ((2 : \u2102) * \u2191m + 3) ^ (-(j : \u2124) - 1)) =\n      (fun m' : {m : \u2115 // Odd m \u2227 3 \u2264 m} => (((m' : \u2115) : \u2102)) ^ (-(j : \u2124) - 1)) \u2218 oddGeThreeEquiv := by\n    funext m\n    rw [Function.comp_apply]\n    show ((2 : \u2102) * \u2191m + 3) ^ (-(j : \u2124) - 1) = (((oddGeThreeEquiv m : \u2115) : \u2102)) ^ (-(j : \u2124) - 1)\n    congr 1\n    show (2 : \u2102) * \u2191m + 3 = ((2 * m + 3 : \u2115) : \u2102)\n    push_cast\n    ring\n  rw [heq3]\n  rw [show (\u2211' m : \u2115, (((fun m' : {m : \u2115 // Odd m \u2227 3 \u2264 m} => (((m' : \u2115) : \u2102)) ^ (-(j : \u2124) - 1)) \u2218\n      oddGeThreeEquiv) m)) =\n    \u2211' m : \u2115, (fun m' : {m : \u2115 // Odd m \u2227 3 \u2264 m} => (((m' : \u2115) : \u2102)) ^ (-(j : \u2124) - 1))\n      (oddGeThreeEquiv m) from rfl]\n  rw [Equiv.tsum_eq oddGeThreeEquiv\n    (fun m' : {m : \u2115 // Odd m \u2227 3 \u2264 m} => (((m' : \u2115) : \u2102)) ^ (-(j : \u2124) - 1))]\n  -- now: 1 + \u03a3_{m' odd \u2265 3} (\u2191m')^{-(j+1)} = \u2191(lagariasA (j+1))\n  have hj1 : j + 1 \u2260 1 := by omega\n  rw [lagariasA, if_neg hj1]\n  push_cast\n  congr 1\n  have hcast : (\u2191(\u2211' m : {m : \u2115 // Odd m \u2227 3 \u2264 m}, (1 / (m : \u211d)) ^ (j + 1)) : \u2102) =\n      \u2211' m : {m : \u2115 // Odd m \u2227 3 \u2264 m}, (((m : \u2115) : \u2102)) ^ (-(j : \u2124) - 1) := by\n    have h2 := Complex.ofRealCLM.map_tsum (oddSlice_summable (j + 1) (by omega))\n    rw [Complex.ofRealCLM_apply] at h2\n    rw [h2]\n    apply tsum_congr\n    intro m\n    rw [Complex.ofRealCLM_apply]\n    push_cast\n    have hexp : (-(j : \u2124) - 1 : \u2124) = -(((j + 1 : \u2115) : \u2124)) := by push_cast; ring\n    rw [hexp]\n    rw [show (((m : \u2115) : \u2102)) ^ (-(((j + 1 : \u2115) : \u2124))) = ((((m : \u2115) : \u2102) ^ (j + 1))\u207b\u00b9) from by\n      rw [zpow_neg, zpow_natCast]]\n    rw [one_div_pow, inv_eq_one_div]\n  rw [hcast]\n",
  "structuredPatch": [
    {
      "oldStart": 955,
      "oldLines": 19,
      "newStart": 955,
      "newLines": 12,
      "lines": [
        "   rw [lagariasA, if_neg hj1]",
        "   push_cast",
        "   congr 1",
        "-  have hcast : (\u2191(\u2211' m : {m : \u2115 // Odd m \u2227 3 \u2264 m}, (1 / (m : \u211d)) ^ (j + 1)) : \u2102) =",
        "-      \u2211' m : {m : \u2115 // Odd m \u2227 3 \u2264 m}, (((m : \u2115) : \u2102)) ^ (-(j : \u2124) - 1) := by",
        "-    have h2 := Complex.ofRealCLM.map_tsum (oddSlice_summable (j + 1) (by omega))",
        "-    rw [Complex.ofRealCLM_apply] at h2",
        "-    rw [h2]",
        "-    apply tsum_congr",
        "-    intro m",
        "-    rw [Complex.ofRealCLM_apply]",
        "-    push_cast",
        "-    have hexp : (-(j : \u2124) - 1 : \u2124) = -(((j + 1 : \u2115) : \u2124)) := by push_cast; ring",
        "-    rw [hexp]",
        "-    rw [show (((m : \u2115) : \u2102)) ^ (-(((j + 1 : \u2115) : \u2124))) = ((((m : \u2115) : \u2102) ^ (j + 1))\u207b\u00b9) from by",
        "-      rw [zpow_neg, zpow_natCast]]",
        "-    rw [one_div_pow, inv_eq_one_div]",
        "-  rw [hcast]",
        "+  apply tsum_congr",
        "+  intro m",
        "+  push_cast",
        "+  have hexp : (-(j : \u2124) - 1 : \u2124) = -(((j + 1 : \u2115) : \u2124)) := by push_cast; ring",
        "+  rw [hexp]",
        "+  rw [show (((m : \u2115) : \u2102)) ^ (-(((j + 1 : \u2115) : \u2124))) = ((((m : \u2115) : \u2102) ^ (j + 1))\u207b\u00b9) from by",
        "+    rw [zpow_neg, zpow_natCast]]",
        "+  rw [one_div_pow, inv_eq_one_div]",
        " "
      ]
    }
  ],
  "userModified": false,
  "replaceAll": false
}