[{"type":"thinking","thinking":"`Complex.digamma_one : digamma 1 = -Real.eulerMascheroniConstant` ✓ exists. So the integer case: ψ(m) = −γ + H_{m−1} via digamma_one + digamma_apply_add_one induction:\nψ(↑n) for n ≥ 1: ψ(n+1) = ψ(n) + 1/n = ψ(n) + n⁻¹... induction: ψ(↑n) = −γ + Σ_{j=1}^{n−1} 1/j = −γ + harmonic(n−1)... harmonic(n−1) = Σ_{i<n−1} (i+1)⁻¹ = Σ_{j=1}^{n−1} 1/j ✓.\n\nThe induction lemma:\n```\ntheorem digamma_natCast_eq (n : ℕ) (hn : 1 ≤ n) :\n    Complex.digamma (n : ℂ) = -(Real.eulerMascheroniConstant : ℂ) + (harmonic (n - 1) : ℝ) := by\n  induction n with\n  | zero => omega\n  | succ k ih =>\n    rcases eq_or_ne k 0 with hk | hk\n    · subst hk  -- n = 1: harmonic 0 = 0: ψ(1) = −γ ✓\n      simp [Complex.digamma_one, harmonic]  -- harmonic 0 = ∑ range 0 = 0: cast 0: −γ + 0: simp [digamma_one, harmonic, Finset.sum_range_zero...] — harmonic 0 = 0: `harmonic_zero : harmonic 0 = 0`? probably simp via def\n    · have hk1 : 1 ≤ k := Nat.one_le_iff_ne_zero.mpr hk\n      have h1 := ih hk1  -- ψ(↑k) = −γ + H_{k−1}\n      have h2 := Complex.digamma_apply_add_one (k : ℂ) ?_  -- ψ(↑k+1) = ψ(↑k) + (↑k)⁻¹; side: ∀ m, ↑k ≠ −↑m: k ≥ 1: −↑m ≤ 0 < ... re: (↑k ≠ −↑m): both real: k = −m impossible (k ≥ 1, −m ≤ 0): intro m h; have : (k:ℝ) = -(m:ℝ) := by exact_mod_cast h; have : (0:ℝ) ≤ (m:ℝ) := by positivity; linarith [this, ...]  hmm (↑k : ℂ) = −(↑m : ℂ) ⟺ k = −m: exact_mod_cast h : k = −(m:ℤ)?? the casts: (↑k : ℂ) = −(↑m : ℂ) with k m : ℕ: exact_mod_cast h gives (k : ℤ) = -(m : ℤ)? or k = m hmm: −(↑m : ℂ) with m : ℕ: the cast of −↑m: exact_mod_cast h : k = m?? no: −(m:ℂ) is not a nat cast... Let me: have hre := congrArg Complex.re h: (↑k).re = (−↑m).re: ↑k = −↑m as reals: k ≥ 1, m ≥ 0 ⟹ −↑m ≤ 0 < 1 ≤ k: linarith ✓:\n      have hside : ∀ m : ℕ, (k : ℂ) ≠ -(m : ℂ) := by\n        intro m h\n        have hre := congrArg Complex.re h\n        simp [Complex.neg_re, Complex.natCast_re] at hre\n        have hmk : (1 : ℝ) ≤ (k : ℝ) := by exact_mod_cast hk1\n        have hm0 : (0 : ℝ) ≤ (m : ℝ) := by positivity\n        linarith\n      have h2 := Complex.digamma_apply_add_one (k : ℂ) hside  -- digamma (↑k + 1) = digamma ↑k + (↑k)⁻¹\n      rw [show ((k + 1 : ℕ) : ℂ) = (k : ℂ) + 1 by push_cast; ring, h2, h1]\n      -- harmonic (k+1−1) = harmonic k = harmonic (k−1) + (k)⁻¹-ish: harmonic (k) = harmonic (k−1) + (k)⁻¹: harmonic_succ? `harmonic_succ : harmonic (n+1) = harmonic n + (↑(n+1))⁻¹`? probably from the def via sum_range_succ\n      rw [show (k + 1 : ℕ) - 1 = k by omega, show k = (k - 1) + 1 by omega, harmonic_succ??]\n      ...\n```\nThe harmonic step: harmonic (k) = harmonic (k−1) + (↑k)⁻¹: harmonic k = ∑_{i<k} (i+1)⁻¹ = ∑_{i<k−1} (i+1)⁻¹ + (↑k)⁻¹ (sum_range_succ) ✓:\n```\n      have hharm : (harmonic (k + 1 - 1) : ℝ) = (harmonic (k - 1) : ℝ) + ((k : ℝ))⁻¹ := by\n        have h1 : k + 1 - 1 = k := by omega\n        rw [h1]\n        have h2 : harmonic k = harmonic (k - 1) + ((k : ℚ))⁻¹ := by\n          conv_lhs => rw [show k = (k - 1) + 1 by omega]\n          rw [harmonic]  -- unfold: ∑ i ∈ range ((k−1)+1), (↑(i+1))⁻¹\n          rw [Finset.sum_range_succ]\n          -- goal: ∑_{i<k−1} (↑(i+1))⁻¹ + (↑((k−1)+1))⁻¹ = harmonic (k−1) + (↑k)⁻¹\n          rw [show (k - 1 : ℕ) + 1 = k by omega]  -- hmm inside: ↑((k−1)+1) = ↑k\n          rfl  -- harmonic (k−1) unfolds definitionally? harmonic is a def: harmonic (k−1) ≡ ∑ ... — rfl might work or need unfold on RHS too\n        rw [h2]  -- now in ℝ: ↑(harmonic (k−1) + (↑k)⁻¹) = ↑(harmonic (k−1)) + ↑(↑k)⁻¹: push_cast\n        push_cast\n        ring\n      rw [hharm]  -- goal: −γ + ↑(harmonic (k−1)) + (↑k:ℂ)⁻¹ = −γ + (↑(harmonic (k−1)) + (↑k:ℝ)⁻¹ : ℂ)-ish — casts ℝ→ℂ: push_cast; ring\n      push_cast\n      ring\n```\nFiddly but fine. THEN the (B) integer case:\n‖ψ(↑n)‖ = ‖−γ + H_{n−1}‖ ≤ γ + H_{n−1} (norm of the ℂ-cast of a real: ‖(x:ℝ):ℂ‖ = |x|: Complex.norm_real; −γ + H: real; |−γ + H_{n−1}| = −γ + H_{n−1} (H ≥ 0, H_{n−1} ≥ 0 and... −γ + H_{n−1} could be negative for n = 1 (H_0 = 0: −γ) — |−γ| = γ ✓; for n ≥ 2: H_1 = 1 > γ ✓ nonneg... just bound |−γ + H| ≤ γ + H (abs via triangle) ≤ 2/3 + (1 + log(n−1)) (harmonic_le_one_add_log) ≤ 5/3 + log n... then ≤ 20 log(2+‖w‖) with ‖w‖ = n ≥ 2: log(2+n) ≥ log 4: 5/3 + log n ≤ 20 log(2+n)?? log n ≤ log(2+n) ✓; 5/3 ≤ 19 log 4 ≈ 26 ✓.)\n\nThe integer-case detection: by_cases ∃ m : ℤ, (m:ℂ) = w — then m ≥ 2, w = ↑n with n := m.toNat ≥ 2, ‖w‖ = n (norm: ‖(↑n:ℂ)‖ = n: RCLike.norm_natCast ✓).\n\nOK. Now let me write the whole §1+§2. Actually — the file will also have §3 (C) + §4 (A) + §5 (G). Let me write §1+§2 first and compile, to keep iterations manageable.\n\nImports for LiDigammaLeft.lean: Mathlib + Zeta23.GammaFacts.Series (digamma_series) + Zeta23.GammaFacts.StirlingVert (digamma_stirling — for (A) later) + NguyenRH1.LiReflect (digamma_add_natCast) + NguyenRH1.LiTrivialZeros (gamma_mul_prod — for (G) later). Hmm — LiReflect is heavy (LiDisc chain) but built. OK.\n\nLet me write §1 + §2 now.","signature":""},{"type":"text","text":"`digamma_one` exists. Writing LiDigammaLeft.lean §1 (telescope) + §2 (right-half bound B)."},{"type":"tool_use","id":"Write_258","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigammaLeft.lean","content":"/-\nNguyenRH1/LiDigammaLeft.lean — tier ii′ sub-stage 5e-ii (D-068 §1 C2):\nthe two digamma bounds feeding the circle estimate of ii′-5e-v.\n\n* §1 `tsum_one_div_sub_telescope`: ∑'ₙ (1/(n+N) − 1/(n+N+1)) = 1/N\n  (partial-sum telescope + squeeze).\n* §2 `norm_digamma_le_of_two_le_re`: ‖ψ(w)‖ ≤ 20·log(2+‖w‖) for\n  re w ≥ 2, |im w| ≤ 5 — the Weierstrass-series route (Zeta23\n  `DigammaSeries.digamma_series`): Σ'_n w/((n+1)(w+n+1)) with the split\n  at N = ⌈re w⌉₊ (head via the harmonic bound, tail via §1's telescope);\n  the positive-integer case via `digamma_one` + the recurrence\n  (`digamma_natCast_eq`).\n* §3 (C): `digamma_recip_sum_le` — the separated reciprocal sum bound\n  Σ_{j<m} ‖w+j‖⁻¹ ≤ 2/c + 2 + 2·log m for dist(w, −ℕ) ≥ c (V-split).\n* §4 (A): `norm_digamma_le_of_dist_nat` — the near-axis left-plane bound\n  ‖ψ(w)‖ ≤ (46 + 2/c) + 23·log(2+‖w‖) for re w ≤ 2, dist(w,−ℕ) ≥ c\n  (recurrence `digamma_add_natCast` + §3 + the landing-zone bound via\n  §2 or StirlingVert).\n* §5 (G): `logDeriv_Gammaℝ_eq` — logDeriv ΓR s = −(log π)/2 + ½ψ(s/2)\n  for im s ≠ 0 (the m-fold shift: `gamma_mul_prod` + the EventuallyEq\n  machinery of 5d).\n\nArchive references: D-068 §1 (C2) + §7, journal-025/026.\n-/\nimport Mathlib\nimport Zeta23.GammaFacts.Series\nimport Zeta23.GammaFacts.StirlingVert\nimport NguyenRH1.LiReflect\nimport NguyenRH1.LiTrivialZeros\n\nopen Zeta23 Complex Filter Topology MeasureTheory\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. The telescoping tail -/\n\n/-- The partial sums of the telescoping series. -/\ntheorem sum_range_one_div_sub (N M : ℕ) :\n    ∑ n ∈ Finset.range M, ((1 : ℝ) / ((n : ℝ) + N) - 1 / ((n : ℝ) + N + 1))\n      = 1 / (N : ℝ) - 1 / ((M : ℝ) + N) := by\n  have h := Finset.sum_range_sub' (fun n : ℕ => (1 : ℝ) / ((n : ℝ) + N)) M\n  simp only at h\n  rw [Nat.cast_zero, zero_add] at h\n  rw [← h]\n  apply Finset.sum_congr rfl\n  intro n _\n  push_cast\n  ring_nf\n\n/-- **The telescoping tail**: ∑'ₙ (1/(n+N) − 1/(n+N+1)) = 1/N for N ≥ 1. -/\ntheorem tsum_one_div_sub_telescope (N : ℕ) (hN : 1 ≤ N) :\n    ∑' n : ℕ, ((1 : ℝ) / ((n : ℝ) + N) - 1 / ((n : ℝ) + N + 1)) = 1 / (N : ℝ) := by\n  have hNR : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hN\n  have hnonneg : ∀ n : ℕ, (0 : ℝ) ≤ 1 / ((n : ℝ) + N) - 1 / ((n : ℝ) + N + 1) := by\n    intro n\n    have h1 : (0 : ℝ) < (n : ℝ) + N := by\n      have h2 := Nat.cast_nonneg (n : ℕ)\n      linarith [hNR, h2]\n    have h3 : 1 / ((n : ℝ) + N + 1) ≤ 1 / ((n : ℝ) + N) :=\n      one_div_le_one_div_of_le h1 (by linarith)\n    linarith [h3]\n  have hlim0 : Tendsto (fun M : ℕ => (1 : ℝ) / ((M : ℝ) + N)) atTop (𝓝 0) := by\n    have h1 : Tendsto (fun M : ℕ => (1 : ℝ) / (M + 1)) atTop (𝓝 0) :=\n      tendsto_one_div_add_atTop_nhds_zero_nat\n    apply squeeze_zero (fun M => by positivity)\n    · intro M\n      apply one_div_le_one_div_of_le (by positivity)\n      linarith [hNR]\n    · exact h1\n  have hlim : Tendsto (fun M : ℕ => (1 : ℝ) / (N : ℝ) - 1 / ((M : ℝ) + N)) atTop\n      (𝓝 (1 / (N : ℝ))) := by\n    have h := hlim0.const_sub (1 / (N : ℝ))\n    rwa [sub_zero] at h\n  have hHasSum : HasSum (fun n : ℕ => (1 : ℝ) / ((n : ℝ) + N) - 1 / ((n : ℝ) + N + 1))\n      (1 / (N : ℝ)) := by\n    rw [hasSum_iff_tendsto_nat_of_nonneg hnonneg]\n    convert hlim using 1\n    ext M\n    exact sum_range_one_div_sub N M\n  exact hHasSum.tsum_eq\n\n/-! ## 2. The right-half-plane bound (B) -/\n\n/-- ψ at positive integers: ψ(n) = −γ + H_{n−1} for n ≥ 1. -/\ntheorem digamma_natCast_eq (n : ℕ) (hn : 1 ≤ n) :\n    Complex.digamma (n : ℂ)\n      = -(Real.eulerMascheroniConstant : ℂ) + ((harmonic (n - 1) : ℚ) : ℂ) := by\n  induction n with\n  | zero => omega\n  | succ k ih =>\n    rcases eq_or_ne k 0 with hk | hk\n    · subst hk\n      simp [Complex.digamma_one, harmonic]\n    · have hk1 : 1 ≤ k := Nat.one_le_iff_ne_zero.mpr hk\n      have h1 := ih hk1\n      have hside : ∀ m : ℕ, (k : ℂ) ≠ -(m : ℂ) := by\n        intro m h\n        have hre := congrArg Complex.re h\n        simp [Complex.neg_re, Complex.natCast_re] at hre\n        have hmk : (1 : ℝ) ≤ (k : ℝ) := by exact_mod_cast hk1\n        have hm0 : (0 : ℝ) ≤ (m : ℝ) := by positivity\n        linarith\n      have h2 := Complex.digamma_apply_add_one (k : ℂ) hside\n      rw [show ((k + 1 : ℕ) : ℂ) = (k : ℂ) + 1 by push_cast; ring, h2, h1]\n      have hharm : ((harmonic (k + 1 - 1) : ℚ) : ℂ)\n          = ((harmonic (k - 1) : ℚ) : ℂ) + ((k : ℝ) : ℂ)⁻¹ := by\n        have h3 : k + 1 - 1 = k := by omega\n        rw [h3]\n        have h4 : harmonic k = harmonic (k - 1) + ((k : ℚ))⁻¹ := by\n          conv_lhs => rw [show k = (k - 1) + 1 by omega]\n          rw [harmonic, Finset.sum_range_succ]\n          have h5 : k - 1 + 1 = k := by omega\n          rw [h5]\n          rfl\n        rw [h4]\n        push_cast\n        ring\n      rw [hharm]\n      push_cast\n      ring\n\n/-- The summability of the pointwise majorant g n = ‖w‖/((n+1)(A+n+1))\nfor A = re w ≥ 2, and the shifted harmonic-split bound on its sum. -/\ntheorem summable_digamma_majorant {w : ℂ} (hwre : 2 ≤ w.re) :\n    Summable (fun n : ℕ => ‖w‖ / (((n : ℝ) + 1) * (w.re + (n : ℝ) + 1))) := by\n  have h1 : Summable (fun n : ℕ => (((n : ℝ) + 1) ^ 2)⁻¹) := by\n    have h2 : Summable (fun n : ℕ => (((n : ℝ)) ^ 2)⁻¹) := by\n      have h3 := Real.summable_nat_rpow_inv.mpr (by norm_num : (1 : ℝ) < 2)\n      have heq : (fun n : ℕ => ((n : ℝ) ^ (2 : ℝ))⁻¹) = fun n : ℕ => (((n : ℝ)) ^ 2)⁻¹ := by\n        funext n\n        rw [show ((2 : ℝ)) = ((2 : ℕ) : ℝ) by norm_num, Real.rpow_natCast]\n      rwa [heq] at h3\n    have h4 := (summable_nat_add_iff 1).mpr h2\n    simpa [add_comm] using h4\n  refine Summable.of_nonneg_of_le (fun n => by positivity) ?_ (h1.mul_left ‖w‖)\n  intro n\n  have hpos1 : (0 : ℝ) < ((n : ℝ) + 1) * (w.re + (n : ℝ) + 1) := by\n    apply mul_pos (by positivity)\n    have := Nat.cast_nonneg (n : ℕ)\n    linarith [hwre, this]\n  rw [div_le_div_iff?]...\n```\nHmm — wait, the comparison: ‖w‖/((n+1)(A+n+1)) ≤ ‖w‖·((n+1)²)⁻¹ ⟺ 1/((n+1)(A+n+1)) ≤ 1/(n+1)² ⟺ (n+1)² ≤ (n+1)(A+n+1) ⟺ n+1 ≤ A+n+1 ⟺ 0 ≤ A. Via div_le_div_of_nonneg_left (ha : 0 ≤ ‖w‖) (hb : 0 < (n+1)²) (hbc : (n+1)² ≤ (n+1)(A+n+1)): gives ‖w‖/((n+1)(A+n+1)) ≤ ‖w‖/(n+1)² ✓. And ‖w‖/(n+1)² = ‖w‖ * ((n+1)²)⁻¹ by (div_eq_mul_inv). Let me write it cleanly with div_le_div_of_nonneg_left:\n```\n  intro n\n  have hA : (0 : ℝ) < w.re := by linarith [hwre]\n  have hstep : ((n : ℝ) + 1) ^ 2 ≤ ((n : ℝ) + 1) * (w.re + (n : ℝ) + 1) := by\n    rw [sq]\n    apply mul_le_mul_of_nonneg_left _ (by positivity : (0 : ℝ) ≤ (n : ℝ) + 1)\n    have := Nat.cast_nonneg (n : ℕ)\n    linarith [hwre, this]\n  calc ‖w‖ / (((n : ℝ) + 1) * (w.re + (n : ℝ) + 1))\n      ≤ ‖w‖ / (((n : ℝ) + 1) ^ 2) :=\n        div_le_div_of_nonneg_left (norm_nonneg _) (by positivity) hstep\n    _ = ‖w‖ * ((((n : ℝ) + 1) ^ 2)⁻¹) := by rw [div_eq_mul_inv]\n```\nGood. Now the main (B) theorem. Let me also pin the per-term identity and bound:\na_n := 1/((n:ℂ)+1) − 1/(w+n+1): \n- identity: a_n = w/(((n:ℂ)+1)*(w+n+1)): field_simp [Nat.cast_add_one_ne_zero n, (w+n+1 ≠ 0)] — w+n+1 ≠ 0: re(w+n+1) = re w + n + 1 ≥ 3 > 0: fun h => by have := congrArg Complex.re h; simp [add_re, natCast_re, one_re] at this; linarith [hwre, Nat.cast_nonneg n]... let me write a have:\n```\n  have hwn1 : ∀ n : ℕ, w + (n : ℂ) + 1 ≠ 0 := by\n    intro n h\n    have h2 := congrArg Complex.re h\n    simp [Complex.add_re, Complex.natCast_re, Complex.one_re] at h2\n    have h3 := Nat.cast_nonneg n\n    linarith [hwre, h3, h2]\n```\n- ‖a_n‖ ≤ g n: \n```\n  have hterm : ∀ n : ℕ, ‖1 / ((n : ℂ) + 1) - 1 / (w + n + 1)‖\n      ≤ ‖w‖ / (((n : ℝ) + 1) * (w.re + (n : ℝ) + 1)) := by\n    intro n\n    have hident : 1 / ((n : ℂ) + 1) - 1 / (w + n + 1)\n        = w / (((n : ℂ) + 1) * (w + n + 1)) := by\n      field_simp [Nat.cast_add_one_ne_zero n, hwn1 n]\n      ring\n    rw [hident, norm_div, norm_mul, DigammaSeries.norm_natCast_add_one]\n    -- wait — norm_natCast_add_one is in Zeta23's DigammaSeries namespace? It was in Series.lean: `lemma norm_natCast_add_one (n : ℕ) : ‖((n : ℂ) + 1)‖ = (n : ℝ) + 1` — namespace? the file had `namespace Zeta23`... `end DigammaSeries / end Zeta23` — so it's Zeta23.DigammaSeries.norm_natCast_add_one — with open Zeta23: DigammaSeries.norm_natCast_add_one ✓.\n    -- now: ‖w‖/((n+1)·‖w+n+1‖) ≤ ‖w‖/((n+1)(re w+n+1)): need ‖w+n+1‖ ≥ re w+n+1 ≥ 0 and (n+1) > 0\n    have hrew : (w + (n : ℂ) + 1).re = w.re + (n : ℝ) + 1 := by\n      simp [Complex.add_re, Complex.natCast_re, Complex.one_re]\n    have hle : w.re + (n : ℝ) + 1 ≤ ‖w + (n : ℂ) + 1‖ := by\n      rw [← hrew]\n      exact (Complex.abs_re_le_norm _).trans_eq (abs_of_nonneg (by\n        have := Nat.cast_nonneg n\n        linarith [hwre, this]) |>.symm)?? hmm: |re| ≤ ‖·‖ and re ≥ 0 ⟹ re ≤ ‖·‖: (Complex.abs_re_le_norm _) : |z.re| ≤ ‖z‖; z.re ≥ 0 ⟹ |z.re| = z.re: so z.re ≤ ‖z‖: (abs_of_nonneg h).symm ▸: \n      rw [← hrew]\n      have hpos : (0:ℝ) ≤ (w + (n:ℂ) + 1).re := by rw [hrew]; have := Nat.cast_nonneg n; linarith [hwre, this]\n      rwa [abs_of_nonneg hpos] at *?? — (abs_re_le_norm _) : |z.re| ≤ ‖z‖: rw [abs_of_nonneg hpos] at this?? getting confused. Clean:\n      have h2 := Complex.abs_re_le_norm (w + (n : ℂ) + 1)\n      rw [abs_of_nonneg hpos] at h2\n      rw [hrew] at h2  -- hmm hrew : (w+↑n+1).re = w.re + ↑n + 1: rw at h2: h2 : w.re + ↑n + 1 ≤ ‖w+↑n+1‖ ✓\n      exact h2\n    apply div_le_div_of_nonneg_left (norm_nonneg _)\n    · positivity... (0 < (n+1)*(re w + n + 1): mul_pos (Nat.cast_add_one_pos?...) — (0:ℝ) < (n:ℝ)+1: by positivity (Nat.cast_nonneg + 1 — positivity handles? `Nat.cast_add_one_pos`? there's positivity extension for Nat.cast: (n:ℝ)+1 > 0: by have := Nat.cast_nonneg n; linarith. Let me inline haves.)\n    · -- (n+1)*(re w+n+1) ≤ (n+1)*‖w+n+1‖\n      apply mul_le_mul_of_nonneg_left hle (by positivity?)...\n```\nOK — I'll write these carefully in the file with explicit haves for the positivities. Let me now write §1+§2 fully and compile. To keep it manageable I'll write the whole file skeleton with §1+§2 complete and §3–§5 as... no — write §1+§2 only first (the file grows by appends). Actually the Write tool replaces the whole file; I'll write §1+§2 now, compile, then append §3+§4+§5 via Edit."},"extra_content":null}]