{
  "file_path": "D:\\Python\\Quantum\\research\\derivations\\D-061-lean-build-and-skeletons.md",
  "old_string": "## 5. What remains for 5.1 (future sessions)\nOrdered per draft Appendix B: (i) sInfty_lower_bound +\nmarginTilde_convex (elementary; positivity/interval tactics + the\n11-block table); (ii) the traced contour bound inside\nlambda_pos_finite_height (needs explicit N(T)/S(T)/\u03b6\u2032/\u03b6 bounds);\n(iii) valley proofs (need model-space/RKHS infrastructure);\n(iv) Suzuki factorization proof + the (1.12) statement itself.\nThe finite-height theorem's computational hypotheses (RHUpTo,\nLiVerifiedUpTo) stay as trusted inputs by design.",
  "new_string": "## 5. What remains for 5.1 (future sessions)\nOrdered per draft Appendix B: (i) sInfty_lower_bound +\nmarginTilde_convex (elementary; positivity/interval tactics + the\n11-block table); (ii) the traced contour bound inside\nlambda_pos_finite_height (needs explicit N(T)/S(T)/\u03b6\u2032/\u03b6 bounds);\n(iii) valley proofs (need model-space/RKHS infrastructure);\n(iv) Suzuki factorization proof + the (1.12) statement itself.\nThe finite-height theorem's computational hypotheses (RHUpTo,\nLiVerifiedUpTo) stay as trusted inputs by design.\n\n**UPDATE 2026-08-19 (session 011): tier (i) COMPLETE.**\nchain_rule_sqrt_shift, sInfty_lower_bound, marginTilde_convex all PROVED\nwith PrintAxioms = [propext, Classical.choice, Quot.sound] only (no\nsorryAx). ~1100 new lines across 10 commits: full support library \u2014\nbern_term_*, sInf_series_summable, harmonic_lower/upper, oddHarm_eq,\nsInf_partial_lower (for sInfty); chain-rule package\n(chain_rule_sqrt_shift_on/sqrt, deriv2_of_hasDerivAt_nhds), psiOf block\ntable (8 blocks with formulas+signs, block_range_bounds), IIMaj as\npsiTilde with iim_u2_antitone/iimaj_bracket_bound/IIMaj_deriv2_lt,\nmarginTilde_eq_expanded identity, marginExpanded ContDiffOn/ContinuousOn\nregularity, deriv2 combinators (for marginTilde). Details:\nresearch/journal/session-011.md. Remaining: tiers (ii), (iii), (iv)."
}

{
  "filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigamma.lean",
  "oldString": "  rw [dpsiTermC]\n  field_simp [hm0, hs, hsm]\n  ring\n\n/-- The complex series is summable on dpsiDomain. -/\nlemma dpsiTermC_summable {s : \u2102} (hs : s \u2208 dpsiDomain) : Summable (dpsiTermC s) := by\n  have hs1 : s + 1 \u2260 0 := by\n    have h := dpsiTermC_pole_free hs 0\n    simpa using h\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 hs1 m hsm]\n    rw [norm_div]\n    have hden : \u2016((m : \u2102) + 1) * (s + \u2191m + 1)\u2016 \u2265 ((m : \u211d) + 1) * ((m : \u211d) + 1) := by\n      rw [norm_mul]\n      apply mul_le_mul_of_nonneg_left _ (by positivity : (0 : \u211d) \u2264 \u2016(m : \u2102) + 1\u2016)\n      \u00b7 -- \u2016s + m + 1\u2016 \u2265 m + 1 via the real part\n        have hre : 0 < s.re := by\n          have h1 : |s.re - 1 / 2| < 1 / 2 := by\n            have h2 : |s.re - (1 / 2 : \u211d)| \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 : dist s ((1 : \u2102) / 2) = \u2016s - (1 : \u2102) / 2\u2016 := dist_eq_norm _ _\n            have h4 := hs\n            rw [dpsiDomain, Metric.mem_ball, h3] at h4\n            exact lt_of_le_of_lt h2 h4\n          linarith [abs_lt.mp h1]\n        have h5 : \u2016s + \u2191m + 1\u2016 \u2265 s.re + m + 1 := by\n          have h6 : (s + \u2191m + 1).re = s.re + m + 1 := by\n            simp [Complex.add_re, Complex.one_re, Complex.ofReal_re]\n          rw [\u2190 h6]\n          exact Complex.re_le_norm _\n        have h7 : s.re + m + 1 \u2265 (m : \u211d) + 1 := by linarith\n        exact h5.trans h7\n    -- \u2016\u2191m + 1\u2016 = m + 1\n    have hnorm1 : \u2016((m : \u2102) + 1)\u2016 = (m : \u211d) + 1 := by\n      rw [show ((m : \u2102) + 1) = ((m + 1 : \u211d) : \u2102) by push_cast; ring]\n      rw [RCLike.norm_ofReal]\n      exact abs_of_nonneg (by positivity)\n    rw [hnorm1] at hden\n    -- \u2016s\u2016/(\u2016m+1\u2016\u00b7\u2016s+m+1\u2016) \u2264 \u2016s\u2016/(m+1)\u00b2\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)) := by\n          apply 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",
  "newString": "  rw [dpsiTermC]\n  field_simp [hm0, hs, 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 hs1 : s + 1 \u2260 0 := by\n    have h := dpsiTermC_pole_free hs 0\n    simpa using h\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 hs1 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        all_goals linarith\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",
  "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} (hs : s + 1 \u2260 0) (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.ofReal_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, hs, hsm]\n  ring\n\n/-- The complex series is summable on dpsiDomain. -/\nlemma dpsiTermC_summable {s : \u2102} (hs : s \u2208 dpsiDomain) : Summable (dpsiTermC s) := by\n  have hs1 : s + 1 \u2260 0 := by\n    have h := dpsiTermC_pole_free hs 0\n    simpa using h\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 hs1 m hsm]\n    rw [norm_div]\n    have hden : \u2016((m : \u2102) + 1) * (s + \u2191m + 1)\u2016 \u2265 ((m : \u211d) + 1) * ((m : \u211d) + 1) := by\n      rw [norm_mul]\n      apply mul_le_mul_of_nonneg_left _ (by positivity : (0 : \u211d) \u2264 \u2016(m : \u2102) + 1\u2016)\n      \u00b7 -- \u2016s + m + 1\u2016 \u2265 m + 1 via the real part\n        have hre : 0 < s.re := by\n          have h1 : |s.re - 1 / 2| < 1 / 2 := by\n            have h2 : |s.re - (1 / 2 : \u211d)| \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 : dist s ((1 : \u2102) / 2) = \u2016s - (1 : \u2102) / 2\u2016 := dist_eq_norm _ _\n            have h4 := hs\n            rw [dpsiDomain, Metric.mem_ball, h3] at h4\n            exact lt_of_le_of_lt h2 h4\n          linarith [abs_lt.mp h1]\n        have h5 : \u2016s + \u2191m + 1\u2016 \u2265 s.re + m + 1 := by\n          have h6 : (s + \u2191m + 1).re = s.re + m + 1 := by\n            simp [Complex.add_re, Complex.one_re, Complex.ofReal_re]\n          rw [\u2190 h6]\n          exact Complex.re_le_norm _\n        have h7 : s.re + m + 1 \u2265 (m : \u211d) + 1 := by linarith\n        exact h5.trans h7\n    -- \u2016\u2191m + 1\u2016 = m + 1\n    have hnorm1 : \u2016((m : \u2102) + 1)\u2016 = (m : \u211d) + 1 := by\n      rw [show ((m : \u2102) + 1) = ((m + 1 : \u211d) : \u2102) by push_cast; ring]\n      rw [RCLike.norm_ofReal]\n      exact abs_of_nonneg (by positivity)\n    rw [hnorm1] at hden\n    -- \u2016s\u2016/(\u2016m+1\u2016\u00b7\u2016s+m+1\u2016) \u2264 \u2016s\u2016/(m+1)\u00b2\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)) := by\n          apply 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\nend NguyenRH1\n",
  "structuredPatch": [
    {
      "oldStart": 333,
      "oldLines": 6,
      "newStart": 333,
      "newLines": 12,
      "lines": [
        "   field_simp [hm0, hs, hsm]",
        "   ring",
        " ",
        "+/-- \u2016(m : \u2102) + 1\u2016 = m + 1. -/",
        "+lemma norm_natCast_add_one (m : \u2115) : \u2016((m : \u2102) + 1)\u2016 = (m : \u211d) + 1 := by",
        "+  have e : ((m : \u2102) + 1) = \u2191((m : \u211d) + 1) := by push_cast; ring",
        "+  rw [e, Complex.norm_real, Real.norm_eq_abs]",
        "+  exact abs_of_nonneg (by positivity)",
        "+",
        " /-- The complex series is summable on dpsiDomain. -/",
        " lemma dpsiTermC_summable {s : \u2102} (hs : s \u2208 dpsiDomain) : Summable (dpsiTermC s) := by",
        "   have hs1 : s + 1 \u2260 0 := by"
      ]
    },
    {
      "oldStart": 343,
      "oldLines": 39,
      "newStart": 349,
      "newLines": 21,
      "lines": [
        "     have hsm : s + m + 1 \u2260 0 := dpsiTermC_pole_free hs m",
        "     rw [dpsiTermC_eq hs1 m hsm]",
        "     rw [norm_div]",
        "-    have hden : \u2016((m : \u2102) + 1) * (s + \u2191m + 1)\u2016 \u2265 ((m : \u211d) + 1) * ((m : \u211d) + 1) := by",
        "-      rw [norm_mul]",
        "-      apply mul_le_mul_of_nonneg_left _ (by positivity : (0 : \u211d) \u2264 \u2016(m : \u2102) + 1\u2016)",
        "-      \u00b7 -- \u2016s + m + 1\u2016 \u2265 m + 1 via the real part",
        "-        have hre : 0 < s.re := by",
        "-          have h1 : |s.re - 1 / 2| < 1 / 2 := by",
        "-            have h2 : |s.re - (1 / 2 : \u211d)| \u2264 \u2016s - (1 : \u2102) / 2\u2016 := by",
        "-              have e : s.re - 1 / 2 = (s - (1 : \u2102) / 2).re := by",
        "-                simp [Complex.sub_re]",
        "-              rw [e]",
        "-              exact Complex.abs_re_le_norm _",
        "-            have h3 : dist s ((1 : \u2102) / 2) = \u2016s - (1 : \u2102) / 2\u2016 := dist_eq_norm _ _",
        "-            have h4 := hs",
        "-            rw [dpsiDomain, Metric.mem_ball, h3] at h4",
        "-            exact lt_of_le_of_lt h2 h4",
        "-          linarith [abs_lt.mp h1]",
        "-        have h5 : \u2016s + \u2191m + 1\u2016 \u2265 s.re + m + 1 := by",
        "-          have h6 : (s + \u2191m + 1).re = s.re + m + 1 := by",
        "-            simp [Complex.add_re, Complex.one_re, Complex.ofReal_re]",
        "-          rw [\u2190 h6]",
        "-          exact Complex.re_le_norm _",
        "-        have h7 : s.re + m + 1 \u2265 (m : \u211d) + 1 := by linarith",
        "-        exact h5.trans h7",
        "-    -- \u2016\u2191m + 1\u2016 = m + 1",
        "-    have hnorm1 : \u2016((m : \u2102) + 1)\u2016 = (m : \u211d) + 1 := by",
        "-      rw [show ((m : \u2102) + 1) = ((m + 1 : \u211d) : \u2102) by push_cast; ring]",
        "-      rw [RCLike.norm_ofReal]",
        "-      exact abs_of_nonneg (by positivity)",
        "-    rw [hnorm1] at hden",
        "-    -- \u2016s\u2016/(\u2016m+1\u2016\u00b7\u2016s+m+1\u2016) \u2264 \u2016s\u2016/(m+1)\u00b2",
        "+    have hden : ((m : \u211d) + 1) * ((m : \u211d) + 1) \u2264 \u2016((m : \u2102) + 1) * (s + \u2191m + 1)\u2016 := by",
        "+      rw [norm_mul, norm_natCast_add_one]",
        "+      apply mul_le_mul_of_nonneg_left _ (by positivity : (0 : \u211d) \u2264 (m : \u211d) + 1)",
        "+      have hre : 0 < s.re := dpsiDomain_re_pos hs",
        "+      have h5 : s.re + m + 1 \u2264 \u2016s + \u2191m + 1\u2016 := by",
        "+        have h6 : (s + \u2191m + 1).re = s.re + m + 1 := by",
        "+          have h3 : (\u2191m : \u2102).re = (m : \u211d) := by simp",
        "+          simp [Complex.add_re, Complex.one_re, h3]",
        "+        rw [\u2190 h6]",
        "+        exact Complex.re_le_norm _",
        "+        all_goals linarith",
        "+      linarith [h5]",
        "     have hpos : (0 : \u211d) < ((m : \u211d) + 1) * ((m : \u211d) + 1) := by positivity",
        "-    calc \u2016s\u2016 / \u2016((m : \u2102) + 1) * (s + \u2191m + 1)\u2016 \u2264 \u2016s\u2016 / (((m : \u211d) + 1) * ((m : \u211d) + 1)) := by",
        "-          apply div_le_div_of_nonneg_left (norm_nonneg _) hpos hden",
        "+    calc \u2016s\u2016 / \u2016((m : \u2102) + 1) * (s + \u2191m + 1)\u2016 \u2264 \u2016s\u2016 / (((m : \u211d) + 1) * ((m : \u211d) + 1)) :=",
        "+          div_le_div_of_nonneg_left (norm_nonneg _) hpos hden",
        "       _ = \u2016s\u2016 / ((m : \u211d) + 1) ^ 2 := by ring",
        "   exact Summable.of_norm_bounded (summable_div_add_one_sq \u2016s\u2016) hnorm",
        " "
      ]
    }
  ],
  "userModified": false,
  "replaceAll": false
}