[{"type":"thinking","thinking":"`AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq (hf : AnalyticOnNhd 𝕜 f U) (hg) (hU : IsPreconnected U) (h₀ : z₀ ∈ U) (hfg : ∃ᶠ z in 𝓝[≠] z₀, f z = g z) : EqOn f g U` ✓ EXISTS.\n\nAll infrastructure verified. Now let me write the digamma series file. Given the late hour and the size, let me structure it in compilable increments. I'll write the first chunk now: the real series + summability + the uniform convergence + the ψ_real identity (A2+A3). Then compile. Then the complex side (A4, A5) + reindexing (A6) + assembly (A7) next.\n\nLet me define the shared summand. To keep the real and complex series aligned, define for m : ℕ and x : ℝ / s : ℂ:\n\nReal version: dpsiTermR (x : ℝ) (m : ℕ) : ℝ := if m = 0 then −1/x else (1/(m:ℝ) − 1/(x + m))\nComplex version: dpsiTermC (s : ℂ) (m : ℕ) : ℂ := if m = 0 then −1/s else (1/(m:ℂ) − 1/(s + m))\n\nHmm — the if-then-else summand will make every tsum manipulation annoying. Alternative: use the (−1/(x+m)) form for the derivative-related parts and keep the base series as 1/(m+1) − 1/(x+m+1) over ℕ (no if). The m = 0 derivative term −1/x doesn't fit Σ_{m≥1}... — hold on: the base series Σ_{m≥1}(1/m − 1/(x+m)) only converges due to the cancellation; its derivative series Σ_{m≥1} 1/(x+m)² converges absolutely and the −1/x's derivative 1/x² is separate. For the ITERATED derivatives I need them combined: iteratedDeriv j D = (−1)^{j+1}j!Σ_{m≥0}(x+m)^{−(j+1)} — combining the 1/x^{j+1} term as m = 0. The combination step: Σ_{m≥1}(x+m)^{−(j+1)} + x^{−(j+1)} = Σ_{m≥0}(x+m)^{−(j+1)} — via tsum_eq_zero_add shift ✓ simple.\n\nSo encode the base series with m+1 indexing (no if):\ndpsiTermR (x : ℝ) (m : ℕ) : ℝ := 1/(m+1 : ℝ) − 1/(x + m + 1)\nDinfR (x : ℝ) : ℝ := −γ − 1/x + ∑' m, dpsiTermR x m\ndpsiTermC (s : ℂ) (m : ℕ) : ℂ := 1/((m:ℂ)+1) − 1/(s + m + 1)\nDinfC (s : ℂ) : ℂ := −γ − 1/s + ∑' m, dpsiTermC s m\n\nCast bridge: ↑(dpsiTermR x m) = dpsiTermC ↑x m ✓ (push_cast).\n\nSummability (real): |dpsiTermR x m| = x/((m+1)(x+m+1)) ≤ x/(m+1)² for x > 0. Hmm — need the norm form for Summable.of_norm_bounded: ‖dpsiTermR x m‖ ≤ x/(m+1)² — for x > 0: dpsiTermR x m = x/((m+1)(x+m+1)) — positivity: 1/(m+1) − 1/(x+m+1) = (x+m+1 − (m+1))/((m+1)(x+m+1)) = x/((m+1)(x+m+1)) ≥ 0 for x > 0 ✓ so |term| = term = x/((m+1)(x+m+1)) ≤ x/(m+1)² since x+m+1 ≥ m+1 ⟹ 1/(x+m+1) ≤ 1/(m+1) ✓.\n\nThe dominator fun m => x/(m+1)² : summable — from Real.summable_one_div_nat_pow (p=2): Summable (fun n => 1/(n:ℝ)^2) — shift by 1: summable_nat_add_iff 1: Summable (fun n => 1/((n+1):ℝ)^2) ↔ Summable (fun n => 1/(n:ℝ)^2) — wait summable_nat_add_iff (k : ℕ) : Summable (fun n => f (n + k)) ↔ Summable f — with f n := 1/(n:ℝ)^2: f (n+1) = 1/((n+1):ℝ)^2 — hmm ((n+1:ℕ):ℝ) vs (n:ℝ)+1 — cast — careful: f (n + 1) with f n := 1/(n:ℝ)^2: = 1/((↑(n+1)):ℝ)^2 = 1/((↑n + 1):ℝ)^2 ✓ push_cast bridge. Then mul by x: .mul_left x? Summable.mul_left? — `Summable.mul_left (a) (hf : Summable f) : Summable (fun b => a * f b)` ✓ (used in liSummable ✓).\n\nFor x ≤ 0... the real domain is (0,∞) — state for 0 < x.\n\nThe uniform convergence for the interchange: I need TendstoLocallyUniformlyOn (fun n x => log n − Σ_{m ∈ range(n+1)} 1/(x+m)) DinfR ... hmm — actually the interchange lemma `hasDerivAt_of_tendstoLocallyUniformlyOn` wants: (hf' : TendstoLocallyUniformlyOn f' g' l s) — the DERIVATIVE sequence converging locally uniformly. The derivative sequence: d/dx[logGammaSeq x n] = log n − Σ_{m=0}^n 1/(x+m). Decompose:\n  log n − Σ_{m=0}^n 1/(x+m) = (log n − harmonic n) + (−1/x + Σ_{m=1}^n (1/m − 1/(x+m)))\n  — where Σ_{m=1}^n (1/m − 1/(x+m)) = Σ_{m ∈ Icc 1 n} ... = Σ_{m ∈ range n} dpsiTermR x m (m ↦ m+1: dpsiTermR x m = 1/(m+1) − 1/(x+m+1) — so Σ_{m=1}^n (1/m − 1/(x+m)) = Σ_{m' ∈ range n} dpsiTermR x m' with m' = m−1 ✓ (range n, m'+1 = 1..n ✓)).\n  So the deriv sequence = (log n − harmonic n) + (−1/x) + Σ_{m ∈ range n} dpsiTermR x m — wait sign check: −1/x + Σ — and DinfR x = −γ − 1/x + ∑' — ✓ consistent.\n  \n  The locally-uniform convergence of the sum of three pieces:\n  (i) log n − harmonic n → −γ: constant in x — pointwise (tendsto_harmonic_sub_log — wait direction: harmonic n − log n → γ — so log n − harmonic n → −γ ✓ via .neg). Locally uniform in x: the sequence doesn't depend on x — `TendstoLocallyUniformlyOn` of an x-constant sequence from its pointwise tendsto: there should be `TendstoLocallyUniformlyOn.of_forall_tendsto`? hmm — or: TendstoLocallyUniformlyOn iff locally-uniform... — a constant-in-x sequence converging pointwise converges UNIFORMLY on any set (the rate doesn't involve x) — `TendstoUniformlyOn` of a constant sequence: the uniform-cauchy / direct: ∀ ε, ∃ N, ∀ n ≥ N, ∀ x ∈ s, |a_n − a| < ε — from the pointwise rate ✓ — there might be `TendstoUniformlyOn.of_...`? I can prove via `Metric.tendstoUniformlyOn_iff`... — fine, small.\n  (ii) −1/x: constant in n — `tendstoLocallyUniformlyOn_const`? ✓.\n  (iii) Σ_{m ∈ range n} dpsiTermR x m → ∑' — locally uniform via the M-test: HasSumUniformlyOn.of_norm_le_summable? — hmm — that gives HasSumUniformlyOn (the sum-function relation uniformly) — from which TendstoLocallyUniformlyOn of partial sums — there's `hasSumUniformlyOn_iff_tendstoLocallyUniformlyOn` (used in derivWithin_tsum's proof ✓). So: HasSumUniformlyOn (dpsiTermR) (Dinf-series) on each compact via of_norm_le_summable with u m := K/(m+1)² for x ∈ compact ⊆ Ioi 0... — the of_norm_le_summable signature (line 35): (hu : Summable u) {s} (h : ∀ n x, x ∈ s → ‖f n x‖ ≤ u n)? : HasSumUniformlyOn f (fun x => ∑' n, f n x) s? — roughly. Then assemble locally-uniform from compact covers: SummableLocallyUniformlyOn_of_locally_bounded (line 56) is for SummableLocallyUniformlyOn — the derivative-series summable-locally-uniformly: that's what's needed for the (real) interchange's hf' (TendstoLocallyUniformlyOn of the deriv sequence) — via hasSumUniformlyOn_iff_tendstoLocallyUniformlyOn — hmm wait: hf' wants TendstoLocallyUniformlyOn (fun n => deriv-seq-partial-sums) Dinf — the partial sums of a HasSumUniformlyOn family converge locally uniformly (hasSumUniformlyOn_iff_tendstoLocallyUniformlyOn.mp ✓).\n\nOK — all pieces mapped. Let me now also plan the ITERATED derivative on the complex side via iteratedDerivWithin_tsum:\n- f m := fun s : ℂ => dpsiTermC s m (on U := Metric.ball (1/2:ℂ) (1/2)? — need U open, containing 1/2, avoiding s = −(m+1) for all m: the poles of the terms are at −(m+1): −1, −2, ... — ball (1/2) (3/4)? — take U := {s : ℂ | 0 < s.re} — the right half-plane! open ✓ (isOpen_re... — `{s | 0 < s.re}` = re ⁻¹' Ioi 0 — open by continuity ✓), contains 1/2 ✓ and the real segment (0,1) ✓, avoids all −(m+1) ✓ (those have re ≤ 0... −(m+1) has re = −(m+1) ≤ −1 < 0 ✓). On the right half-plane: |s + m + 1| ≥ re(s) + m + 1 — hmm for the M-test on compacts K ⊆ {re > 0}: |s+m+1| ≥ re(s)+m+1 ≥ c_K + m + 1 with c_K := min re on K > 0 ✓ and |1/(m+1) − 1/(s+m+1)| = |s|/((m+1)|s+m+1|) ≤ C_K/((m+1)(c_K+m+1)) ≤ C'_K/(m+1)² ✓ summable ✓.\n- The iterated derivative of the summand: iteratedDerivWithin k (fun s => 1/(↑m+1) − 1/(s + ↑m + 1)) U s = −(−1)^k k! (s+m+1)^{−(k+1)}·... for k ≥ 1 — via the const (1/(m+1))'s derivative 0 + the −1/(s+m+1) part. The helper: iteratedDerivWithin k (fun s => (s + c)⁻¹) U x = (−1)^k · k! · (x+c)^{−(k+1)}? — hmm zpow form: (x+c)^(-(k+1) : ℤ) — induction on k with derivWithin_zpow/hasDerivAt_zpow ✓ (LiPrincipal used hasDerivAt_zpow ✓).\n  Actually — cleaner: write the summand as −(s + ↑m + 1)⁻¹ + const — and use iteratedDerivWithin_add/const — the iteratedDerivWithin of a sum = sum of iteratedDerivWithins (needs ContDiffOn ✓). And of the constant: 0 for k ≥ 1 ✓.\n  The inv part: fun s => (s + c)⁻¹ = fun s => (s + c)^(−1 : ℤ) — iteratedDerivWithin k of zpow(−1): there might be `iteratedDerivWithin_zpow`? or prove by induction: base: iteratedDerivWithin 0 = (s+c)^(−1) ✓ = (−1)^0·0!·(s+c)^{−1} ✓; step: derivWithin of (−1)^k k! (s+c)^{−(k+1)} = (−1)^k k! · (−(k+1))·(s+c)^{−(k+2)}·1 (chain with s+c deriv 1) = (−1)^{k+1}(k+1)!(s+c)^{−(k+2)} ✓. via derivWithin_const_mul + derivWithin zpow comp... — `derivWithin_zpow`? hmm — there's `derivWithin... zpow`? — hasDerivAt_zpow exists ✓; for derivWithin on an open set: derivWithin = deriv (isOpen) ✓ then deriv_zpow? — `deriv_zpow`? — hasDerivAt_zpow.deriv + deriv_const_mul + deriv comp (s+c): deriv (fun s => (s+c)^(-n:ℤ)) x = (−n)·(x+c)^(−n−1)·1 — via hasDerivAt_zpow.comp with (hasDerivAt_id.add_const)... — the deriv zpow: `deriv_zpow`? or do via hasDerivAt... .deriv. Fine — small induction lemma.\n- Then SummableLocallyUniformlyOn of the k-th derivative family (k ≥ 1): |−(−1)^k k!(s+m+1)^{−(k+1)}| = k!/|s+m+1|^{k+1} ≤ k!/(c_K + m + 1)^{k+1} on compact K — summable (k+1 ≥ 2) ✓ via SummableLocallyUniformlyOn_of_locally_bounded (line 56) or of_locally_bounded_eventually.\n- iteratedDerivWithin_tsum gives: iteratedDerivWithin k (fun s => ∑' m, dpsiTermC s m) U x = ∑' m, −(−1)^k k!(x+m+1)^{−(k+1)} for x ∈ U, k ≥ 1.\n- The −γ − 1/s part: iteratedDerivWithin k (−γ − 1/s) at x for k ≥ 1: = −(−1)^k k! x^{−(k+1)} (the −γ dies) ✓ same inv-induction.\n- Sum them: iteratedDerivWithin k DinfC U x = −(−1)^k k![x^{−(k+1)} + Σ_{m≥0}(x+m+1)^{−(k+1)}] = −(−1)^k k! Σ_{m≥0}(x+m)^{−(k+1)} (tsum_eq_zero_add or the shift) ✓.\n- iteratedDerivWithin_of_isOpen: = iteratedDeriv k DinfC x ✓.\n- digamma = DinfC on U via identity principle ✓ ⟹ iteratedDeriv k digamma = iteratedDeriv k DinfC at points of U — via... the EqOn on an open set gives eventualEq on nhds of interior points ⟹ iteratedDeriv equality — the helper: `AnalyticOnNhd`-EqOn ⟹ iteratedDeriv eq: for x ∈ U, U open: f =ᶠ[𝓝 x] g (from EqOn + U ∈ 𝓝 x) ⟹ iteratedDeriv k f x = iteratedDeriv k g x — need `Filter.EventuallyEq.iteratedDeriv_eq`? — might not exist — but deriv_eq exists and iterating: `Filter.EventuallyEq.iteratedDeriv`? — check. If missing, small induction: f =ᶠ[𝓝 x] g ⟹ ∀ᶠ y in 𝓝 x, deriv f y = deriv g y? — hmm — deriv_eq gives pointwise at x only. For the iteration I need the eventual equality of the derived functions — there's `Filter.EventuallyEq.deriv` (I keep guessing) — let me check: `EventuallyEq.deriv`? — hmm — there IS `Filter.EventuallyEq.deriv (h : f =ᶠ[𝓝 x] g) : deriv f =ᶠ[𝓝 x] deriv g`? — I believe that exists (it's a standard one — if two functions agree on a neighborhood, their derivatives agree on a neighborhood — via derivWithin... or it's `EventuallyEq.deriv` in Deriv.lean). If not, prove: on ball(x, r) f = g; for y in ball: f =ᶠ[𝓝 y] g (ball ⊆ nhd) ⟹ deriv f y = deriv g y (EventuallyEq.deriv_eq at y) — so ∀ y ∈ ball: deriv f y = deriv g y ⟹ deriv f =ᶠ[𝓝 x] deriv g (ball ∈ 𝓝 x) ✓. Then induction on k. Fine — write a bespoke `iteratedDeriv_congr_of_eventuallyEq` helper.\n\n- The affine comp for the final assembly: iteratedDeriv j (fun s => digamma ((1+s)/2)) 0 = (1/2)^j · iteratedDeriv j digamma (1/2) — the map φ(s) = (1+s)/2 = 1/2 + s/2: φ = (1/2 + ·) ∘ (·/2)? or (·/2) ∘ (1+·)... (1+s)/2 — affine with slope 1/2. iteratedDeriv comp with an affine map: (d/ds)^j f((1+s)/2) = (1/2)^j f^{(j)}((1+s)/2). Via iteratedDeriv_comp_add_const (have it? — used in LiResidue for sub-const ✓ `iteratedDeriv_comp_sub_const`) + the const-mul comp `iteratedDeriv_comp_const_mul`? — need: iteratedDeriv j (fun s => f (s/2)) x = (1/2)^j iteratedDeriv j f (x/2) — is there such a lemma? Let me search: `iteratedDeriv_comp_const_mul`? or via zpow... Actually there might be `iteratedDeriv_comp_mul_left`? Hmm — let me handle via a bespoke induction on j using `deriv_const_mul`-style comp: deriv (fun s => f (s/c)) x = (1/c)·deriv f (x/c) — via HasDerivAt.comp with HasDerivAt.div_const — then iterate. I'll write the induction inline. OR — alternative: avoid the affine comp by rephrasing piece (A)'s series at the right CENTER: define the complex series centered at 1/2 directly: the series for digamma((1+s)/2): its summand 1/((1+s)/2 + m + 1) = 2/(1 + s + 2m + 2) = 2/(s + (2m+3))·... and 1/((1+s)/2) = 2/(1+s) — hmm — the digamma series at w = (1+s)/2: digamma(w) = −γ − 1/w + Σ_{m≥1}(1/m − 1/(w+m)) — at w = (1+s)/2: −γ − 2/(1+s) + Σ_{m≥1}(1/m − 2/(1+s+2m)) — the iteratedDeriv j at s = 0 of −2/(1+s): −2·(−1)^j j! (1+s)^{−(j+1)}|₀ = −2(−1)^j j!; of −2/(1+s+2m): −2(−1)^j j!(1+2m)^{−(j+1)}. Sum: −2(−1)^j j![1 + Σ_{m≥1}(2m+1)^{−(j+1)}]·... — hmm let me compute the target: iteratedDeriv j [digamma((1+s)/2)] at 0 = (1/2)^j digamma^{(j)}(1/2) = (1/2)^j·(−1)^{j+1}j!Σ_{m≥0}(1/2+m)^{−(j+1)}. And Σ_{m≥0}(1/2+m)^{−(j+1)} = Σ_{m≥0} 2^{j+1}/(1+2m)^{j+1} = 2^{j+1}lagariasA(j+1) — so the value = (1/2)^j(−1)^{j+1}j!2^{j+1}lagariasA(j+1) = 2·(−1)^{j+1}j!·lagariasA(j+1). Via the direct series at s: Σ_{m≥0}-form: digamma((1+s)/2) = −γ + Σ_{m≥0}[?] — with the m≥0 unified form: −γ − 1/w + Σ_{m≥1}(1/m − 1/(w+m)) at w = (1+s)/2: = −γ − 2/(1+s) + Σ_{m≥1}(1/m − 2/(1+s+2m)). Hmm — this has the SAME three-part structure — and its iteratedDeriv j at 0 (j ≥ 1): −2(−1)^j j!·1 + Σ_{m≥1} (−2)(−1)^j j!(1+2m)^{−(j+1)} = −2(−1)^j j! Σ_{m≥0}(2m+1)^{−(j+1)} = −2(−1)^j j!·lagariasA(j+1)·... wait Σ_{m≥0}(2m+1)^{−(j+1)} = Σ_{odd ≥ 1} m^{−(j+1)} = lagariasA(j+1) ✓ (my lagariasA(j+1) for j+1 ≥ 2 ✓ j ≥ 1). = 2(−1)^{j+1}j! lagariasA(j+1) ✓✓ SAME. So whether I go via the affine comp or via the directly-shifted series, same answer. The DIRECT series at s avoids the affine comp lemma! But then I need the digamma-series identity at w = (1+s)/2 — i.e. the identity DinfC = digamma on the shifted domain... — the identity principle gives digamma = DinfC on U (right half-plane) — then digamma((1+s)/2) = DinfC((1+s)/2) for (1+s)/2 ∈ U — and DinfC((1+s)/2)'s series terms: 1/(↑m+1) − 1/((1+s)/2 + ↑m + 1) = 1/(↑m+1) − 2/(1+s+2↑m+2) — hmm — the iteratedDerivWithin_tsum then applies to the series-in-s — the summands as functions of s: (s ↦ 1/(↑m+1) − 1/((1+s)/2 + ↑m + 1)) — their iteratedDerivs at 0 via the chain — the (1+s)/2 inside — SAME affine comp issue, just moved. Meh. The affine comp is one small induction — let me just do the affine comp induction. OR — simplest of all: get the iterated deriv of the series at the CENTER 1/2 in the w-variable (via iteratedDerivWithin_tsum on U ∋ 1/2), giving digamma^{(j)}(1/2) = (−1)^{j+1}j!Σ_{m≥0}(1/2+m)^{−(j+1)} — and then ONE affine-comp lemma for the final assembly. The affine comp: iteratedDeriv j (fun s => F ((1+s)/2)) 0 = (1/2)^j · iteratedDeriv j F (1/2) for any F analytic near 1/2 — a clean standalone induction on j:\n  j = 0: F(1/2) ✓.\n  step: deriv (fun s => G((1+s)/2)) 0 = (1/2)·deriv G (1/2) — hasDerivAt comp: HasDerivAt (fun s => (1+s)/2) (1/2) 0 + HasDerivAt G (deriv G (1/2)) (1/2) — comp → deriv = deriv G (1/2)·(1/2)·... — hmm the iteratedDeriv_succ step: iteratedDeriv (j+1) F∘φ 0 = deriv (iteratedDeriv j (F∘φ)) 0 = deriv (fun s => (1/2)^j · iteratedDeriv j F (φ s)) 0 [by the IH function equality] = (1/2)^j · deriv (iteratedDeriv j F ∘ φ) 0 = (1/2)^j · (1/2) · iteratedDeriv (j+1) F (1/2) ✓ — needs the deriv-comp at each step. OK — standard. Let me write the affine comp as: `iteratedDeriv_comp_div_two`... — actually generic: `iteratedDeriv_comp_add_div_two`? Let me make it specific to φ(s) = (1+s)/2:\n\n```lean\nlemma iteratedDeriv_comp_one_add_div_two (F : ℂ → ℂ) (j : ℕ) (hF : ∀ s ∈ Metric.ball (1/2) (1/2), AnalyticAt ℂ F s) -- or ContDiffAt assumptions\n    : iteratedDeriv j (fun s => F ((1 + s) / 2)) 0 = (1/2)^j * iteratedDeriv j F (1/2)\n```\nHmm — the differentiability side conditions: for the induction I need iteratedDeriv j F to exist and be differentiable near the points — F analytic on a ball around 1/2 ✓. Let me state with AnalyticAt ℂ F (1/2) + ... — actually the induction needs F's iterated derivs analytic near 1/2 — AnalyticAt F (1/2) gives all iteratedDerivs analytic at 1/2 (AnalyticAt.deriv + eventually_analyticAt ✓) ✓ so hypothesis AnalyticAt ℂ F (1/2) suffices... — plus the domain where the intermediate functions are evaluated: deriv (iteratedDeriv j F ∘ φ) 0 needs iteratedDeriv j F differentiable at φ(0) = 1/2 ✓ and φ differentiable ✓.\n\nOK — I have the full plan. It's ~23:15. This is a LOT for one more push. Let me build it in the file incrementally, compiling as I go. I'll write LiDigamma.lean section by section. Section 1: real series summability + cast bridge. Section 2: the real interchange (ψ_real = Dinf on (0,∞)). Section 3: complex DinfC + identity principle. Section 4: iterated derivatives at 1/2. Section 5: reindexing to lagariasA + final τ_j assembly in LiArchimedean.lean.\n\nLet me write Section 1 + 2 first.","signature":""},{"type":"text","text":"All infrastructure verified (identity principle, CLM.map_tsum, iteratedDerivWithin_of_isOpen, the tsum-deriv lemmas). Writing the digamma-series file — Section 1: the real series + summability."},{"type":"tool_use","id":"Write_301","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigamma.lean","content":"/-\nNguyenRH1/LiDigamma.lean — tier ii′ sub-stage ii′-3a, piece (A) core\n(D-066 §4): 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·log n + log n! − Σ_{m=0}^n log(x+m)` with\n`tendsto_log_gamma`. The derivative sequence\n  d/dx[logGammaSeq x n] = log n − Σ_{m=0}^n 1/(x+m)\n  = (log n − H_n) + [−1/x + Σ_{m=1}^n (1/m − 1/(x+m))]\nconverges locally uniformly on (0,∞) (the harmonic piece to −γ by\n`Real.tendsto_harmonic_sub_log`; the series piece by the Weierstrass\nM-test with Σ 1/m²), so the deriv-limit interchange\n(`hasDerivAt_of_tendstoLocallyUniformlyOn`) yields the real identity\n  (log Γ)'(x) = −γ − 1/x + Σ_{m≥1} (1/m − 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) = (−1)^{j+1}·j!·Σ_{m≥0} (m + 1/2)^{−(j+1)}   (j ≥ 1),\nand the odd-m reindexing identifies the sum as 2^{j+1}·lagariasA (j+1).\n\nArchive references: D-066 (route β4, 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) − 1/(x+m+1) (m : ℕ, x : ℝ). -/\ndef dpsiTermR (x : ℝ) (m : ℕ) : ℝ := 1 / (m + 1 : ℝ) - 1 / (x + m + 1)\n\n/-- The real digamma series: −γ − 1/x + Σ_{m≥0} dpsiTermR x m. -/\ndef DinfR (x : ℝ) : ℝ :=\n  -Real.eulerMascheroniConstant - 1 / x + ∑' m : ℕ, dpsiTermR x m\n\n/-- For 0 < x the summand is x/((m+1)(x+m+1)) ≥ 0, ≤ x/(m+1)². -/\nlemma dpsiTermR_eq {x : ℝ} (hx : 0 < x) (m : ℕ) :\n    dpsiTermR x m = x / ((m + 1 : ℝ) * (x + m + 1)) := by\n  have hm0 : (0 : ℝ) < (m : ℝ) + 1 := by positivity\n  have hxm : (0 : ℝ) < x + m + 1 := by positivity\n  rw [dpsiTermR]\n  field_simp\n  ring\n\nlemma dpsiTermR_nonneg {x : ℝ} (hx : 0 < x) (m : ℕ) : 0 ≤ dpsiTermR x m := by\n  rw [dpsiTermR_eq hx]\n  positivity\n\nlemma dpsiTermR_le {x : ℝ} (hx : 0 < x) (m : ℕ) :\n    dpsiTermR x m ≤ x / ((m : ℝ) + 1) ^ 2 := by\n  have hm0 : (0 : ℝ) < (m : ℝ) + 1 := by positivity\n  have hxm : (0 : ℝ) < x + m + 1 := by positivity\n  rw [dpsiTermR_eq hx]\n  rw [div_le_div_iff_of_pos_right (by positivity : (0 : ℝ) < (m + 1 : ℝ) * (x + m + 1))]\n  -- x * (m+1)² ≤ (x/(m+1)²)·((m+1)(x+m+1))·((m+1)²)... — do directly:\n  rw [div_mul_eq_mul_div, le_div_iff₀ (by positivity : (0 : ℝ) < ((m : ℝ) + 1) ^ 2)]\n  have hle : ((m : ℝ) + 1) * ((m : ℝ) + 1) ≤ (x + m + 1) * ((m : ℝ) + 1) := by\n    apply mul_le_mul_of_nonneg_right _ hm0.le\n    linarith\n  calc x * ((m : ℝ) + 1) ^ 2 = x * (((m : ℝ) + 1) * ((m : ℝ) + 1)) := by ring\n    _ ≤ x * ((x + m + 1) * ((m : ℝ) + 1)) :=\n        mul_le_mul_of_nonneg_left hle hx.le\n    _ = (x + m + 1) * ((m : ℝ) + 1) * x := by ring\n    _ ≤ (x + m + 1) * ((m : ℝ) + 1) * ((m : ℝ) + 1) ^ 2 := by\n        apply mul_le_mul_of_nonneg_left _ (by positivity : (0 : ℝ) ≤ (x + m + 1) * ((m : ℝ) + 1))\n        calc x ≤ x + m := by linarith [Nat.cast_nonneg (α := ℝ) m]\n          _ ≤ (m + 1 : ℝ) ^ 2 := by\n            rw [pow_two]\n            have hm0' : (0 : ℝ) ≤ (m : ℝ) := Nat.cast_nonneg m\n            nlinarith\n\n/-- The dominator family is summable (p-series at p = 2, shifted). -/\nlemma summable_div_add_one_sq (c : ℝ) :\n    Summable (fun m : ℕ => c / ((m : ℝ) + 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 : ℕ => (1 : ℝ) / ((m : ℝ) + 1) ^ 2) := by\n    have h3 : Summable (fun m : ℕ => (1 : ℝ) / ((m + 1 : ℕ) : ℝ) ^ 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\n\n/-- The real digamma series is summable for 0 < x. -/\nlemma dpsiTermR_summable {x : ℝ} (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\nend NguyenRH1\n"},"extra_content":null}]