← Session 22 — ii′-1: liCoeff pairing fix + residue machinery
thinking (3252 chars)
The probe with `(fun z => dpsiTermC z n) = (fun s => 1/(↑n+1) − 1/(s+↑n+1))` by rfl works. So the function forms are fine.
The remaining possibility: in the FILE, the hf2 goal's function is NOT the reduced form — and my `show` produced the reduced form — but the error persists — meaning the show's term is NOT defeq to the goal's?! The hf2 goal: `DifferentiableAt ℂ (iteratedDerivWithin j (fun z ↦ f n z) dpsiDomain) r` with f := the family — the `fun z ↦ f n z` — with f = `fun (m:ℕ) => fun (s:ℂ) => dpsiTermC s m`?? — wait NO — the tsum in my iteratedDerivWithin_tsum_dpsiTermC's statement: `fun s : ℂ => ∑' m : ℕ, dpsiTermC s m` — the iteratedDerivWithin_tsum lemma is about `fun z ↦ ∑' n, f n z` with f : ι → 𝕜 → F — matching `∑' n, f n z` with `∑' m, dpsiTermC s m`: f n z := dpsiTermC z n — so f := fun m => fun z => dpsiTermC z m?? — hmm — the elaboration: `∑' m : ℕ, dpsiTermC s m` = tsum (fun m => dpsiTermC s m) — so the family is `fun m => dpsiTermC s m` — with s the OUTER lambda's bound var. When the lemma is instantiated, f := fun m => dpsiTermC ?s m — NO — the lemma's f is a fixed function ι → 𝕜 → F — the unification: (fun z => ∑' n, f n z) =?= (fun s => ∑' m, dpsiTermC s m) — so f n z := dpsiTermC z n — f := fun m => fun z => dpsiTermC z m — then hf2's `fun z ↦ f n z` = `fun z => (fun m => fun z => dpsiTermC z m) n z` — a beta-redex — and my show's target `fun z : ℂ => dpsiTermC z n` — defeq via beta ✓ — show should bridge...
Hmm — unless the error is happening at a DIFFERENT point than I think. Let me look at the current line 772's actual content after my edit — the `show` is at line ~767 now. The error at 772:10 — that's the `rw [h5]`?? or the show? Let me count: 765-777 area — the `show` is at 767-ish, `have h5` at 768-770, `rw [h5]` at 771-772. The error at 772:10 = rw [h5]. And the goal shown: `DifferentiableAt ℂ (iteratedDerivWithin j (fun z => dpsiTermC z n) dpsiDomain) r` — the show ALREADY changed the goal to the reduced form (the display matches h5's LHS exactly) — and rw [h5] STILL fails!?!? — that means h5's LHS term ≠ the goal's term as ELABORATED — both display identically — so there's a hidden instance/def difference. The candidates: the `iteratedDerivWithin` — the field instance — ℂ's DenselyNormedField etc. — could differ by instance PATH: my lemma iteratedDerivWithin_dpsiTermC was proved in the file with `open ... Real` etc. — the instances are the same...
WAIT — I just realized — maybe it's the `dpsiTermC` — in hf2's goal, the family is the one from MY iteratedDerivWithin_tsum_dpsiTermC's statement — `fun s : ℂ => ∑' m : ℕ, dpsiTermC s m` — so the family inside hf2 is `fun m => dpsiTermC ?s m` with ?s := z (the hf2 lambda binder) — i.e. `fun z ↦ (fun m => dpsiTermC ?s m) ...` hmm.
Let me take yet another approach to see the real terms: in the FILE, at the hf2 branch, add `show` with the FULLY-EXPLICIT expected — or better, use `conv` to unfold. Actually — cleanest: use `set_option tactic.hygienic false`? no. Let me use `change` with the exact term from h5's type, and if change fails, the error message will show the mismatch:
Actually — let me use a different strategy entirely: `first | rw [h5] | rw [h5']`? no. Let me use `Strachey`... no. Let me try `simp only [h5]`:
Let me try `simp only [h5]` (which uses a different matching discipline than rw).
tool: Edit ok
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigamma.lean",
"old_string": " \u00b7 show DifferentiableAt \u2102 (iteratedDerivWithin j (fun z : \u2102 => dpsiTermC z n) dpsiDomain) r\n have h5 : iteratedDerivWithin j (fun z : \u2102 => dpsiTermC z n) dpsiDomain r =\n -((-1 : \u2102)) ^ j * (j ! : \u2102) * (r + \u2191n + 1) ^ (-(j : \u2124) - 1) :=\n iteratedDerivWithin_dpsiTermC j (by omega) n hr\n rw [h5]",
"new_string": " \u00b7 have h5 : _ = _ := iteratedDerivWithin_dpsiTermC j (by omega) n hr\n simp only [h5]"
}
result 2026-08-22 09:01:08Z → 2026-08-23 11:33:31Z
{
"filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigammaLeft.lean",
"oldString": " have hm_ge : (2 : \u211d) - w.re \u2264 (m : \u211d) := by\n have h := Nat.le_ceil (2 - w.re)\n rw [hm_def]\n push_cast\n linarith [h]",
"newString": " have hm_ge : (2 : \u211d) - w.re + 1 \u2264 (m : \u211d) := by\n have h := Nat.le_ceil (2 - w.re)\n rw [hm_def]\n push_cast\n linarith [h]",
"originalFile": "/-\nNguyenRH1/LiDigammaLeft.lean \u2014 tier ii\u2032 sub-stage 5e-ii (D-068 \u00a71 C2):\nthe two digamma bounds feeding the circle estimate of ii\u2032-5e-v.\n\n* \u00a71 `tsum_one_div_sub_telescope`: \u2211'\u2099 (1/(n+N) \u2212 1/(n+N+1)) = 1/N\n (partial-sum telescope + squeeze).\n* \u00a72 `norm_digamma_le_of_two_le_re`: \u2016\u03c8(w)\u2016 \u2264 20\u00b7log(2+\u2016w\u2016) for\n re w \u2265 2, |im w| \u2264 5 \u2014 the Weierstrass-series route (Zeta23\n `DigammaSeries.digamma_series`): \u03a3'_n w/((n+1)(w+n+1)) split at\n N = \u2308re w\u2309\u208a (head via the harmonic bound `harmonic_le_one_add_log`,\n tail via \u00a71's telescope); the positive-integer case via `digamma_one`\n + the recurrence (`digamma_natCast_eq`).\n* \u00a73 (C): `digamma_recip_sum_le` \u2014 the separated reciprocal sum bound\n \u03a3_{j<m} \u2016w+j\u2016\u207b\u00b9 \u2264 2/c + 2 + 2\u00b7log m for dist(w, \u2212\u2115) \u2265 c (V-split).\n* \u00a74 (A): `norm_digamma_le_of_dist_nat` \u2014 the near-axis left-plane bound\n for re w \u2264 2, dist(w,\u2212\u2115) \u2265 c (recurrence `digamma_add_natCast` + \u00a73 +\n the landing-zone bound via \u00a72 or StirlingVert).\n* \u00a75 (G): `logDeriv_Gamma\u211d_eq` \u2014 logDeriv \u0393R s = \u2212(log \u03c0)/2 + \u00bd\u03c8(s/2)\n for im s \u2260 0 (the m-fold shift: `gamma_mul_prod` + the EventuallyEq\n machinery of 5d).\n\nArchive references: D-068 \u00a71 (C2) + \u00a77, 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 : \u2115) :\n \u2211 n \u2208 Finset.range M, ((1 : \u211d) / ((n : \u211d) + N) - 1 / ((n : \u211d) + N + 1))\n = 1 / (N : \u211d) - 1 / ((M : \u211d) + N) := by\n have h := Finset.sum_range_sub' (fun n : \u2115 => (1 : \u211d) / ((n : \u211d) + N)) M\n rw [Nat.cast_zero, zero_add] at h\n rw [\u2190 h]\n apply Finset.sum_congr rfl\n intro n _\n push_cast\n ring_nf\n\n/-- **The telescoping tail, HasSum form**. -/\ntheorem hasSum_one_div_sub_telescope (N : \u2115) (hN : 1 \u2264 N) :\n HasSum (fun n : \u2115 => (1 : \u211d) / ((n : \u211d) + N) - 1 / ((n : \u211d) + N + 1))\n (1 / (N : \u211d)) := by\n have hNR : (0 : \u211d) < (N : \u211d) := by exact_mod_cast hN\n have hnonneg : \u2200 n : \u2115, (0 : \u211d) \u2264 1 / ((n : \u211d) + N) - 1 / ((n : \u211d) + N + 1) := by\n intro n\n have h1 : (0 : \u211d) < (n : \u211d) + N := by\n have h2 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n linarith [hNR, h2]\n have h3 : 1 / ((n : \u211d) + N + 1) \u2264 1 / ((n : \u211d) + N) :=\n one_div_le_one_div_of_le h1 (by linarith)\n linarith [h3]\n have hlim0 : Tendsto (fun M : \u2115 => (1 : \u211d) / ((M : \u211d) + N)) atTop (\ud835\udcdd 0) := by\n have h1 : Tendsto (fun M : \u2115 => (1 : \u211d) / ((M : \u211d) + 1)) atTop (\ud835\udcdd 0) :=\n tendsto_one_div_add_atTop_nhds_zero_nat\n refine squeeze_zero (f := fun M : \u2115 => (1 : \u211d) / ((M : \u211d) + N))\n (g := fun M : \u2115 => (1 : \u211d) / ((M : \u211d) + 1)) ?_ ?_ h1\n \u00b7 intro M\n positivity\n \u00b7 intro M\n apply one_div_le_one_div_of_le (by positivity)\n have hN1R : (1 : \u211d) \u2264 (N : \u211d) := by exact_mod_cast hN\n linarith [hN1R]\n have hlim : Tendsto (fun M : \u2115 => (1 : \u211d) / (N : \u211d) - 1 / ((M : \u211d) + N)) atTop\n (\ud835\udcdd (1 / (N : \u211d))) := by\n have h := hlim0.const_sub (1 / (N : \u211d))\n rwa [sub_zero] at h\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\n/-- **The telescoping tail**: \u2211'\u2099 (1/(n+N) \u2212 1/(n+N+1)) = 1/N for N \u2265 1. -/\ntheorem tsum_one_div_sub_telescope (N : \u2115) (hN : 1 \u2264 N) :\n \u2211' n : \u2115, ((1 : \u211d) / ((n : \u211d) + N) - 1 / ((n : \u211d) + N + 1)) = 1 / (N : \u211d) :=\n (hasSum_one_div_sub_telescope N hN).tsum_eq\n\n/-! ## 2. The right-half-plane bound (B) -/\n\n/-- \u03c8 at positive integers: \u03c8(n) = \u2212\u03b3 + H_{n\u22121} for n \u2265 1. -/\ntheorem digamma_natCast_eq (n : \u2115) (hn : 1 \u2264 n) :\n Complex.digamma (n : \u2102)\n = -(Real.eulerMascheroniConstant : \u2102) + ((harmonic (n - 1) : \u211a) : \u2102) := by\n induction n with\n | zero => omega\n | succ k ih =>\n rcases eq_or_ne k 0 with hk | hk\n \u00b7 subst hk\n simp [Complex.digamma_one, harmonic]\n \u00b7 have hk1 : 1 \u2264 k := Nat.one_le_iff_ne_zero.mpr hk\n have h1 := ih hk1\n have hside : \u2200 m : \u2115, (k : \u2102) \u2260 -(m : \u2102) := 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 : \u211d) \u2264 (k : \u211d) := by exact_mod_cast hk1\n have hm0 : (0 : \u211d) \u2264 (m : \u211d) := by positivity\n linarith\n have h2 := Complex.digamma_apply_add_one (k : \u2102) hside\n rw [show ((k + 1 : \u2115) : \u2102) = (k : \u2102) + 1 by push_cast; ring, h2, h1]\n have hharm : ((harmonic (k + 1 - 1) : \u211a) : \u2102)\n = ((harmonic (k - 1) : \u211a) : \u2102) + ((k : \u211d) : \u2102)\u207b\u00b9 := by\n have h3 : k + 1 - 1 = k := by omega\n rw [h3]\n have h4 : harmonic k = harmonic (k - 1) + ((k : \u211a))\u207b\u00b9 := 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 rw [harmonic]\n rw [h4]\n push_cast\n ring\n rw [hharm]\n push_cast\n ring\n\n/-- The digamma-series majorant g n = \u2016w\u2016/((n+1)(re w+n+1)) is summable\n(dominated by \u2016w\u2016/(n+1)\u00b2) for re w \u2265 2. -/\ntheorem summable_digamma_majorant {w : \u2102} (hwre : 2 \u2264 w.re) :\n Summable (fun n : \u2115 => \u2016w\u2016 / (((n : \u211d) + 1) * (w.re + (n : \u211d) + 1))) := by\n have h1 : Summable (fun n : \u2115 => (((n : \u211d) + 1) ^ 2)\u207b\u00b9) := by\n have h2 : Summable (fun n : \u2115 => (((n : \u211d)) ^ 2)\u207b\u00b9) := by\n have h3 := Real.summable_nat_rpow_inv.mpr (by norm_num : (1 : \u211d) < 2)\n have heq : (fun n : \u2115 => ((n : \u211d) ^ (2 : \u211d))\u207b\u00b9) = fun n : \u2115 => (((n : \u211d)) ^ 2)\u207b\u00b9 := by\n funext n\n rw [show ((2 : \u211d)) = ((2 : \u2115) : \u211d) 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 \u2016w\u2016)\n intro n\n have hstep : ((n : \u211d) + 1) ^ 2 \u2264 ((n : \u211d) + 1) * (w.re + (n : \u211d) + 1) := by\n rw [sq]\n apply mul_le_mul_of_nonneg_left _ (by positivity)\n have h2 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n linarith [hwre, h2]\n calc \u2016w\u2016 / (((n : \u211d) + 1) * (w.re + (n : \u211d) + 1))\n \u2264 \u2016w\u2016 / (((n : \u211d) + 1) ^ 2) := by\n apply div_le_div_of_nonneg_left (norm_nonneg _)\n (show (0 : \u211d) < ((n : \u211d) + 1) ^ 2 by positivity) hstep\n _ = \u2016w\u2016 * ((((n : \u211d) + 1) ^ 2)\u207b\u00b9) := by rw [div_eq_mul_inv]\n\n/-- The per-term bound: \u20161/(n+1) \u2212 1/(w+n+1)\u2016 \u2264 \u2016w\u2016/((n+1)(re w+n+1)). -/\ntheorem norm_digamma_term_le {w : \u2102} (hwre : 2 \u2264 w.re) (n : \u2115) :\n \u20161 / ((n : \u2102) + 1) - 1 / (w + n + 1)\u2016\n \u2264 \u2016w\u2016 / (((n : \u211d) + 1) * (w.re + (n : \u211d) + 1)) := by\n have hwn1 : w + (n : \u2102) + 1 \u2260 0 := by\n intro h\n have h2 := congrArg Complex.re h\n simp [Complex.add_re, Complex.natCast_re, Complex.one_re] at h2\n have h3 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n linarith [hwre, h3, h2]\n have hident : 1 / ((n : \u2102) + 1) - 1 / (w + n + 1)\n = w / (((n : \u2102) + 1) * (w + n + 1)) := by\n field_simp [Nat.cast_add_one_ne_zero n, hwn1]\n ring\n have hrew : (w + (n : \u2102) + 1).re = w.re + (n : \u211d) + 1 := by\n simp [Complex.add_re, Complex.natCast_re, Complex.one_re]\n have hle : w.re + (n : \u211d) + 1 \u2264 \u2016w + (n : \u2102) + 1\u2016 := by\n have hpos : (0 : \u211d) \u2264 (w + (n : \u2102) + 1).re := by\n rw [hrew]\n have h3 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n linarith [hwre, h3]\n have h2 := Complex.abs_re_le_norm (w + (n : \u2102) + 1)\n rwa [abs_of_nonneg hpos, hrew] at h2\n rw [hident, norm_div, norm_mul, DigammaSeries.norm_natCast_add_one]\n apply div_le_div_of_nonneg_left (norm_nonneg _)\n \u00b7 apply mul_pos (by positivity)\n have h3 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n linarith [hwre, h3]\n \u00b7 apply mul_le_mul_of_nonneg_left hle (by positivity)\n\n/-- The harmonic-sum form used in the head split. -/\ntheorem sum_one_div_le_one_add_log (N : \u2115) :\n \u2211 n \u2208 Finset.range N, (1 : \u211d) / ((n : \u211d) + 1) \u2264 1 + Real.log N := by\n have h1 : (\u2211 n \u2208 Finset.range N, (1 : \u211d) / ((n : \u211d) + 1)) = (harmonic N : \u211d) := by\n rw [harmonic, Rat.cast_sum]\n apply Finset.sum_congr rfl\n intro i _\n rw [Rat.cast_inv, Rat.cast_natCast, Nat.cast_add_one, one_div]\n rw [h1]\n exact harmonic_le_one_add_log N\n/-- **The right-half-plane digamma bound (B)**: for re w \u2265 2, |im w| \u2264 5,\n\u2016\u03c8(w)\u2016 \u2264 20\u00b7log(2+\u2016w\u2016). Weierstrass series + split at N = \u2308re w\u2309\u208a;\npositive integers via the harmonic identity. -/\ntheorem norm_digamma_le_of_two_le_re {w : \u2102} (hwre : 2 \u2264 w.re) (hwim : |w.im| \u2264 5) :\n \u2016Complex.digamma w\u2016 \u2264 20 * Real.log (2 + \u2016w\u2016) := by\n have hw_norm_ge : 2 \u2264 \u2016w\u2016 := by\n have h1 := Complex.abs_re_le_norm w\n rw [abs_of_nonneg (by linarith [hwre])] at h1\n linarith [hwre, h1]\n have h1log4 : Real.log 4 \u2264 Real.log (2 + \u2016w\u2016) :=\n Real.log_le_log (by norm_num) (by linarith [hw_norm_ge])\n have hlog4gt : (1 : \u211d) < Real.log 4 := by\n have h4 := Real.log_two_gt_d9.le\n have h5 : Real.log 4 = 2 * Real.log 2 := by\n rw [show (4 : \u211d) = 2 ^ 2 by norm_num, Real.log_pow]\n push_cast\n ring\n linarith [h4, h5]\n have hlog4 : (5 : \u211d) / 3 \u2264 19 * Real.log (2 + \u2016w\u2016) := by nlinarith [h1log4, hlog4gt]\n by_cases hwint : \u2203 m : \u2124, (m : \u2102) = w\n \u00b7 -- the positive-integer case: w = \u2191n, n \u2265 2\n obtain \u27e8m, hm\u27e9 := hwint\n have hmre : w.re = (m : \u211d) := by rw [\u2190 hm]; simp\n have hm2 : 2 \u2264 m := by\n by_contra h\n push Not at h\n have h1 : (m : \u211d) \u2264 1 := by exact_mod_cast (show m \u2264 1 by omega)\n linarith [hwre, hmre, h1]\n have hn2 : 2 \u2264 m.toNat := by\n have h1 : (m : \u2124) = ((m.toNat : \u2115) : \u2124) := (Int.toNat_of_nonneg (by omega)).symm\n rw [h1] at hm2\n exact_mod_cast hm2\n set n := m.toNat with hn_def\n have hwn : w = (n : \u2102) := by\n rw [\u2190 hm, hn_def]\n exact_mod_cast (Int.toNat_of_nonneg (by omega : (0 : \u2124) \u2264 m)).symm\n rw [hwn, digamma_natCast_eq n (by omega)]\n have h\u03b30 : (0 : \u211d) \u2264 Real.eulerMascheroniConstant :=\n (by norm_num : (0 : \u211d) \u2264 1 / 2).trans Real.one_half_lt_eulerMascheroniConstant.le\n have hreal : |(-Real.eulerMascheroniConstant + (harmonic (n - 1) : \u211a) : \u211d)|\n \u2264 Real.eulerMascheroniConstant + (1 + Real.log ((n : \u211d) - 1)) := by\n have hH0\u211a : (0 : \u211a) \u2264 harmonic (n - 1) :=\n Finset.sum_nonneg (fun i _ => by positivity)\n have hH0 : (0 : \u211d) \u2264 ((harmonic (n - 1) : \u211a) : \u211d) := by exact_mod_cast hH0\u211a\n have hcast2 : ((n - 1 : \u2115) : \u211d) = (n : \u211d) - 1 := by\n rw [Nat.cast_sub (by omega : 1 \u2264 n)]\n push_cast\n ring\n have hHbound : ((harmonic (n - 1) : \u211a) : \u211d) \u2264 1 + Real.log ((n : \u211d) - 1) := by\n have h := harmonic_le_one_add_log (n - 1)\n rw [hcast2] at h\n exact h\n have hlog0 : (0 : \u211d) \u2264 Real.log ((n : \u211d) - 1) := by\n apply Real.log_nonneg\n have h1 : (1 : \u211d) \u2264 ((n - 1 : \u2115) : \u211d) := by exact_mod_cast (by omega : 1 \u2264 n - 1)\n linarith [h1, hcast2]\n apply abs_le.mpr\n constructor <;> linarith [h\u03b30, hH0, hHbound, hlog0]\n have hnrm : \u2016-(Real.eulerMascheroniConstant : \u2102) + ((harmonic (n - 1) : \u211a) : \u2102)\u2016\n = |(-Real.eulerMascheroniConstant + (harmonic (n - 1) : \u211a) : \u211d)| := by\n rw [\u2190 Complex.ofReal_ratCast, \u2190 Complex.ofReal_neg, \u2190 Complex.ofReal_add,\n Complex.norm_real, Real.norm_eq_abs]\n rw [hnrm]\n have hlogn1 : Real.log ((n : \u211d) - 1) \u2264 Real.log (2 + \u2016w\u2016) := by\n have h2 : ((n - 1 : \u2115) : \u211d) = (n : \u211d) - 1 := by\n rw [Nat.cast_sub (by omega : 1 \u2264 n)]\n push_cast\n ring\n have hpos : (0 : \u211d) < (n : \u211d) - 1 := by\n have h1 : (1 : \u211d) \u2264 ((n - 1 : \u2115) : \u211d) := by exact_mod_cast (by omega : 1 \u2264 n - 1)\n linarith [h1, h2]\n apply Real.log_le_log hpos\n have hwnorm : \u2016w\u2016 = (n : \u211d) := by rw [hwn, RCLike.norm_natCast]\n rw [hwnorm]\n linarith [h2]\n have h\u03b31 : Real.eulerMascheroniConstant \u2264 1 :=\n Real.eulerMascheroniConstant_lt_two_thirds.le.trans (by norm_num)\n rw [hwn] at hlogn1 h1log4\n have hlogbig : (2 : \u211d) \u2264 19 * Real.log (2 + \u2016(n : \u2102)\u2016) := by nlinarith [h1log4, hlog4gt]\n linarith [hreal, h\u03b31, hlogn1, hlogbig]\n \u00b7 -- the series case: w off the integers\n have hcomp : w \u2208 Complex.integerComplement := hwint\n rw [DigammaSeries.digamma_series hcomp]\n set A := w.re with hA_def\n set N := \u2308w.re\u2309\u208a with hN_def\n have hA0 : (0 : \u211d) < A := by linarith [hwre]\n have hNA : A \u2264 (N : \u211d) := by rw [hN_def]; exact Nat.le_ceil _\n have hNA1 : (N : \u211d) \u2264 A + 1 := by\n have h := Nat.ceil_lt_add_one (show (0 : \u211d) \u2264 w.re by linarith [hwre])\n have h2 : ((\u2308w.re\u2309\u208a : \u2115) : \u211d) < w.re + 1 := by exact_mod_cast h\n rw [hN_def]\n linarith [h2]\n have hN1 : 1 \u2264 N := by\n have h1 : (2 : \u2115) \u2264 N := by\n rw [hN_def]\n have h2 := Nat.ceil_mono hwre\n rwa [Nat.ceil_ofNat] at h2\n omega\n have hterm_summ : Summable (fun n : \u2115 => \u20161 / ((n : \u2102) + 1) - 1 / (w + n + 1)\u2016) :=\n Summable.of_nonneg_of_le (fun n => norm_nonneg _) (fun n => norm_digamma_term_le hwre n)\n (summable_digamma_majorant hwre)\n -- the kernel: summable + the split bound\n have hker_summ : Summable (fun n : \u2115 => (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9) := by\n have h1 : Summable (fun n : \u2115 => (((n : \u211d) + 1) ^ 2)\u207b\u00b9) := by\n have h2 : Summable (fun n : \u2115 => (((n : \u211d)) ^ 2)\u207b\u00b9) := by\n have h3 := Real.summable_nat_rpow_inv.mpr (by norm_num : (1 : \u211d) < 2)\n have heq : (fun n : \u2115 => ((n : \u211d) ^ (2 : \u211d))\u207b\u00b9)\n = fun n : \u2115 => (((n : \u211d)) ^ 2)\u207b\u00b9 := by\n funext n\n rw [show ((2 : \u211d)) = ((2 : \u2115) : \u211d) 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\n intro n\n apply (inv_le_inv\u2080 (by positivity) (by positivity)).mpr\n rw [sq]\n apply mul_le_mul_of_nonneg_left _ (by positivity)\n have h2 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n linarith [hA0, h2]\n have hsplit : (\u2211' n : \u2115, (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9)\n = \u2211 n \u2208 Finset.range N, (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9\n + \u2211' n : \u2115, (fun m : \u2115 => (((m : \u211d) + 1) * (A + (m : \u211d) + 1))\u207b\u00b9) (n + N) := by\n exact (hker_summ.sum_add_tsum_nat_add N).symm\n -- the head bound\n have hhead : \u2211 n \u2208 Finset.range N, (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9\n \u2264 (1 + Real.log (N : \u211d)) / A := by\n have hper : \u2200 n : \u2115, (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9\n \u2264 ((n : \u211d) + 1)\u207b\u00b9 * A\u207b\u00b9 := by\n intro n\n have h1 : (0 : \u211d) < ((n : \u211d) + 1) * A := mul_pos (by positivity) hA0\n have h2 : (0 : \u211d) < ((n : \u211d) + 1) * (A + (n : \u211d) + 1) := by\n apply mul_pos (by positivity)\n have h3 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n linarith [hA0, h3]\n rw [\u2190 mul_inv]\n apply (inv_le_inv\u2080 h2 h1).mpr\n apply mul_le_mul_of_nonneg_left _ (by positivity)\n have h3 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n linarith [hA0, h3]\n have hS' : (\u2211 n \u2208 Finset.range N, ((n : \u211d) + 1)\u207b\u00b9) \u2264 1 + Real.log (N : \u211d) := by\n have h := sum_one_div_le_one_add_log N\n simpa [one_div] using h\n calc \u2211 n \u2208 Finset.range N, (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9\n \u2264 \u2211 n \u2208 Finset.range N, ((n : \u211d) + 1)\u207b\u00b9 * A\u207b\u00b9 :=\n Finset.sum_le_sum fun n _ => hper n\n _ = (\u2211 n \u2208 Finset.range N, ((n : \u211d) + 1)\u207b\u00b9) * A\u207b\u00b9 := by rw [\u2190 Finset.sum_mul]\n _ \u2264 (1 + Real.log (N : \u211d)) * A\u207b\u00b9 :=\n mul_le_mul_of_nonneg_right hS' (inv_nonneg.mpr hA0.le)\n _ = (1 + Real.log (N : \u211d)) / A := by rw [div_eq_mul_inv]\n -- the tail bound\n have htail : (\u2211' n : \u2115, (fun m : \u2115 => (((m : \u211d) + 1) * (A + (m : \u211d) + 1))\u207b\u00b9) (n + N))\n \u2264 1 / (N : \u211d) := by\n have h1 : Summable (fun n : \u2115 => (fun m : \u2115 => (((m : \u211d) + 1) * (A + (m : \u211d) + 1))\u207b\u00b9)\n (n + N)) :=\n (summable_nat_add_iff N).mpr hker_summ\n have hterm : \u2200 n : \u2115, (fun m : \u2115 => (((m : \u211d) + 1) * (A + (m : \u211d) + 1))\u207b\u00b9) (n + N)\n \u2264 1 / ((n : \u211d) + N) - 1 / ((n : \u211d) + N + 1) := by\n intro n\n show ((((n + N : \u2115) : \u211d) + 1) * (A + ((n + N : \u2115) : \u211d) + 1))\u207b\u00b9\n \u2264 1 / ((n : \u211d) + N) - 1 / ((n : \u211d) + N + 1)\n have hN0 : (0 : \u211d) < (n : \u211d) + N := by\n have h2 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n have h3 : (0 : \u211d) < (N : \u211d) := by exact_mod_cast hN1\n linarith [h2, h3]\n have htele : (1 : \u211d) / ((n : \u211d) + N) - 1 / ((n : \u211d) + N + 1)\n = (((n : \u211d) + N) * ((n : \u211d) + N + 1))\u207b\u00b9 := by\n rw [div_sub_div _ _ hN0.ne' (by positivity)]\n rw [div_eq_iff (by positivity : ((n : \u211d) + N) * ((n : \u211d) + N + 1) \u2260 0)]\n rw [inv_mul_cancel\u2080 (by positivity : ((n : \u211d) + N) * ((n : \u211d) + N + 1) \u2260 0)]\n ring\n rw [htele]\n have h2 : (0 : \u211d) < ((n : \u211d) + N) * ((n : \u211d) + N + 1) := by positivity\n have h3 : (0 : \u211d) < (((n + N : \u2115) : \u211d) + 1) * (A + ((n + N : \u2115) : \u211d) + 1) := by\n apply mul_pos\n \u00b7 push_cast\n have h4 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n have h5 : (0 : \u211d) < (N : \u211d) := by exact_mod_cast hN1\n positivity\n \u00b7 push_cast\n have h4 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n have h5 : (0 : \u211d) < (N : \u211d) := by exact_mod_cast hN1\n linarith [hA0, h4, h5]\n apply (inv_le_inv\u2080 h3 h2).mpr\n push_cast\n have h4 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n nlinarith [hA0, h4, hN0]\n calc (\u2211' n : \u2115, (fun m : \u2115 => (((m : \u211d) + 1) * (A + (m : \u211d) + 1))\u207b\u00b9) (n + N))\n \u2264 \u2211' n : \u2115, (1 / ((n : \u211d) + N) - 1 / ((n : \u211d) + N + 1)) :=\n Summable.tsum_le_tsum hterm h1 (hasSum_one_div_sub_telescope N hN1).summable\n _ = 1 / (N : \u211d) := (hasSum_one_div_sub_telescope N hN1).tsum_eq\n -- the kernel bound\n have hN0R : (0 : \u211d) < (N : \u211d) := by exact_mod_cast hN1\n have hkernel_bound : (\u2211' n : \u2115, (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9)\n \u2264 (2 + Real.log (A + 1)) / A := by\n rw [hsplit]\n have h1 : (1 + Real.log (N : \u211d)) / A \u2264 (1 + Real.log (A + 1)) / A := by\n have h2 : Real.log (N : \u211d) \u2264 Real.log (A + 1) := Real.log_le_log hN0R hNA1\n rw [div_eq_mul_inv, div_eq_mul_inv]\n apply mul_le_mul_of_nonneg_right _ (inv_nonneg.mpr hA0.le)\n linarith [h2]\n have h2 : (1 : \u211d) / (N : \u211d) \u2264 1 / A := one_div_le_one_div_of_le hA0 hNA\n have h3 : (2 + Real.log (A + 1)) / A = (1 + Real.log (A + 1)) / A + 1 / A := by\n rw [\u2190 add_div]\n congr 1\n ring\n rw [h3]\n linarith [h1, h2, hhead, htail]\n -- the norm of the series\n have hser : \u2016\u2211' n : \u2115, (1 / ((n : \u2102) + 1) - 1 / (w + n + 1))\u2016\n \u2264 (\u2016w\u2016 / A) * (2 + Real.log (A + 1)) := by\n calc \u2016\u2211' n : \u2115, (1 / ((n : \u2102) + 1) - 1 / (w + n + 1))\u2016\n \u2264 \u2211' n : \u2115, \u20161 / ((n : \u2102) + 1) - 1 / (w + n + 1)\u2016 :=\n norm_tsum_le_tsum_norm hterm_summ\n _ \u2264 \u2211' n : \u2115, \u2016w\u2016 / (((n : \u211d) + 1) * (A + (n : \u211d) + 1)) :=\n Summable.tsum_le_tsum (fun n => norm_digamma_term_le hwre n) hterm_summ\n (summable_digamma_majorant hwre)\n _ = \u2016w\u2016 * \u2211' n : \u2115, (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9 := by\n rw [show (\u2211' n : \u2115, \u2016w\u2016 / (((n : \u211d) + 1) * (A + (n : \u211d) + 1)))\n = \u2211' n : \u2115, \u2016w\u2016 * (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9 from\n tsum_congr fun n => by rw [div_eq_mul_inv]]\n exact tsum_mul_left\n _ \u2264 \u2016w\u2016 * ((2 + Real.log (A + 1)) / A) :=\n mul_le_mul_of_nonneg_left hkernel_bound (norm_nonneg _)\n _ = (\u2016w\u2016 / A) * (2 + Real.log (A + 1)) := by ring\n -- the ratio \u2016w\u2016/A \u2264 3\n have hratio : \u2016w\u2016 / A \u2264 3 := by\n have h1 : \u2016w\u2016 \u2264 3 * A := by\n have hnormsq : \u2016w\u2016 ^ 2 = w.re ^ 2 + w.im ^ 2 := by\n rw [\u2190 Complex.normSq_eq_norm_sq, Complex.normSq_apply]\n ring\n have him5 : w.im ^ 2 \u2264 25 := by\n calc w.im ^ 2 = |w.im| ^ 2 := by rw [sq_abs]\n _ \u2264 5 ^ 2 := pow_le_pow_left\u2080 (abs_nonneg _) hwim _\n _ = 25 := by norm_num\n have h2 : \u2016w\u2016 ^ 2 \u2264 (3 * A) ^ 2 := by\n rw [hnormsq]\n have hA2 : 2 \u2264 A := hwre\n nlinarith [him5, hA2]\n exact le_of_pow_le_pow_left\u2080 (two_ne_zero) (by positivity) h2\n rw [div_le_iff\u2080 hA0]\n linarith [h1]\n have hlogA : Real.log (A + 1) \u2264 Real.log (\u2016w\u2016 + 1) := by\n apply Real.log_le_log (by linarith [hA0])\n have h1 : w.re \u2264 \u2016w\u2016 := by\n have h2 := Complex.abs_re_le_norm w\n rwa [abs_of_nonneg (by linarith [hwre])] at h2\n linarith [h1]\n -- the final assembly\n have h\u03b31 : Real.eulerMascheroniConstant \u2264 1 :=\n Real.eulerMascheroniConstant_lt_two_thirds.le.trans (by norm_num)\n have h1w : \u2016(1 : \u2102) / w\u2016 \u2264 1 := by\n rw [norm_div, norm_one]\n rw [div_le_one (by linarith [hw_norm_ge] : (0 : \u211d) < \u2016w\u2016)]\n linarith [hw_norm_ge]\n calc \u2016-(Real.eulerMascheroniConstant : \u2102) - 1 / w\n + \u2211' n : \u2115, (1 / ((n : \u2102) + 1) - 1 / (w + n + 1))\u2016\n \u2264 Real.eulerMascheroniConstant + \u2016(1 : \u2102) / w\u2016\n + \u2016\u2211' n : \u2115, (1 / ((n : \u2102) + 1) - 1 / (w + n + 1))\u2016 := by\n refine (norm_add_le _ _).trans ?_\n refine add_le_add_left ?_ _\n refine (norm_sub_le _ _).trans ?_\n refine add_le_add_left ?_ _\n rw [norm_neg,\n show (Real.eulerMascheroniConstant : \u2102)\n = ((Real.eulerMascheroniConstant : \u211d) : \u2102) from rfl,\n Complex.norm_real, Real.norm_eq_abs,\n abs_of_nonneg ((by norm_num : (0 : \u211d) \u2264 1 / 2).trans\n Real.one_half_lt_eulerMascheroniConstant.le)]\n _ \u2264 1 + 1 + (\u2016w\u2016 / A) * (2 + Real.log (A + 1)) := by\n linarith [h\u03b31, h1w, hser]\n _ \u2264 20 * Real.log (2 + \u2016w\u2016) := by\n have h2 : (\u2016w\u2016 / A) * (2 + Real.log (A + 1)) \u2264 3 * (2 + Real.log (\u2016w\u2016 + 1)) := by\n have h5 : (0 : \u211d) \u2264 Real.log (A + 1) :=\n Real.log_nonneg (by linarith [hwre] : (1 : \u211d) \u2264 A + 1)\n have h3 : (0 : \u211d) \u2264 2 + Real.log (A + 1) := by linarith [h5]\n exact mul_le_mul hratio (by linarith [hlogA]) h3 (by norm_num)\n have h3 : Real.log (\u2016w\u2016 + 1) \u2264 Real.log (2 + \u2016w\u2016) :=\n Real.log_le_log (by positivity) (by linarith)\n have hlognonneg : (0 : \u211d) \u2264 Real.log (2 + \u2016w\u2016) :=\n Real.log_nonneg (by linarith [hw_norm_ge])\n nlinarith [h2, h3, hlog4, hlognonneg]\n\n/-! ## 3. The separated reciprocal sum (C) -/\n\n/-- The right half of the V-split: for j\u2080 = \u2308\u2212re w\u2309\u208a and j > j\u2080,\n\u2016(w+j)\u207b\u00b9\u2016 \u2264 1/(j\u2212j\u2080) (real parts are 1-separated and j\u2080 catches up to\n\u2212re w). -/\ntheorem recip_norm_le_right {w : \u2102} {c : \u211d} (_hdist : \u2200 m : \u2115, c \u2264 \u2016w + (m : \u2102)\u2016)\n {j\u2080 : \u2115} (hj\u2080 : j\u2080 = \u2308-w.re\u2309\u208a) {j : \u2115} (hj : j\u2080 + 1 \u2264 j) :\n \u2016(w + (j : \u2102))\u207b\u00b9\u2016 \u2264 ((j - j\u2080 : \u2115) : \u211d)\u207b\u00b9 := by\n have hj\u2080ge : -(w.re) \u2264 (j\u2080 : \u211d) := by rw [hj\u2080]; exact Nat.le_ceil _\n have hrewj : (w + (j : \u2102)).re = w.re + (j : \u211d) := by\n simp [Complex.add_re, Complex.natCast_re]\n rw [norm_inv]\n have hge : ((j - j\u2080 : \u2115) : \u211d) \u2264 \u2016w + (j : \u2102)\u2016 := by\n have h1 : (w + (j : \u2102)).re \u2264 \u2016w + (j : \u2102)\u2016 := by\n have h2 := Complex.abs_re_le_norm (w + (j : \u2102))\n rwa [abs_of_nonneg (by\n rw [hrewj]\n have h3 : (0 : \u211d) \u2264 w.re + (j\u2080 : \u211d) := by linarith [hj\u2080ge]\n have h4 : ((j\u2080 : \u211d) + 1) \u2264 (j : \u211d) := by exact_mod_cast hj\n linarith [h3, h4])] at h2\n refine le_trans ?_ h1\n rw [hrewj]\n have h3 : (0 : \u211d) \u2264 w.re + (j\u2080 : \u211d) := by linarith [hj\u2080ge]\n have h4 : ((j - j\u2080 : \u2115) : \u211d) = (j : \u211d) - (j\u2080 : \u211d) := by\n rw [Nat.cast_sub (by omega : j\u2080 \u2264 j)]\n rw [h4]\n linarith [h3]\n have hpos : (0 : \u211d) < ((j - j\u2080 : \u2115) : \u211d) := by\n have h1 : (1 : \u2115) \u2264 j - j\u2080 := by omega\n have h2 : (0 : \u211d) < ((j - j\u2080 : \u2115) : \u211d) := by exact_mod_cast h1\n exact h2\n exact (inv_le_inv\u2080 (by linarith [hge, hpos]) hpos).mpr hge\n\n/-- The left half: for j < j\u2080 \u2212 1 (so j\u2080 \u2265 2 and the real part is still\nnegative), \u2016(w+j)\u207b\u00b9\u2016 \u2264 1/(j\u2080\u22121\u2212j). -/\ntheorem recip_norm_le_left {w : \u2102} {c : \u211d} (_hdist : \u2200 m : \u2115, c \u2264 \u2016w + (m : \u2102)\u2016)\n {j\u2080 : \u2115} (hj\u2080 : j\u2080 = \u2308-w.re\u2309\u208a) {j : \u2115} (hj : j + 1 \u2264 j\u2080 - 1) :\n \u2016(w + (j : \u2102))\u207b\u00b9\u2016 \u2264 ((j\u2080 - 1 - j : \u2115) : \u211d)\u207b\u00b9 := by\n have hj\u2080lt : (j\u2080 : \u211d) < -w.re + 1 := by\n rw [hj\u2080]\n by_cases hre : 0 \u2264 -w.re\n \u00b7 have h := Nat.ceil_lt_add_one hre\n have h2 : ((\u2308-w.re\u2309\u208a : \u2115) : \u211d) < -w.re + 1 := by exact_mod_cast h\n exact h2\n \u00b7 push Not at hre\n have h1 : \u2308-w.re\u2309\u208a = 0 := by\n apply Nat.ceil_eq_zero.mpr\n linarith [hre]\n rw [h1] at hj\u2080\n -- j\u2080 = 0 but j + 1 \u2264 j\u2080 \u2212 1 = 0 \u2212 1 = 0 in \u2115: impossible\n omega\n have hrewj : (w + (j : \u2102)).re = w.re + (j : \u211d) := by\n simp [Complex.add_re, Complex.natCast_re]\n have hneg : (w + (j : \u2102)).re < 0 := by\n rw [hrewj]\n have hj\u20802 : 2 \u2264 j\u2080 := by omega\n have h5 : ((j\u2080 - 1 : \u2115) : \u211d) = (j\u2080 : \u211d) - 1 := by\n rw [Nat.cast_sub (by omega : 1 \u2264 j\u2080)]\n push_cast\n ring\n have h6 : ((j + 1 : \u2115) : \u211d) \u2264 ((j\u2080 - 1 : \u2115) : \u211d) := by exact_mod_cast hj\n rw [Nat.cast_add_one] at h6\n linarith [hj\u2080lt, h5, h6]\n rw [norm_inv]\n have hge : ((j\u2080 - 1 - j : \u2115) : \u211d) \u2264 \u2016w + (j : \u2102)\u2016 := by\n have h1 : |(w + (j : \u2102)).re| \u2264 \u2016w + (j : \u2102)\u2016 := Complex.abs_re_le_norm _\n rw [hrewj] at h1\n have h2 : |(w.re + (j : \u211d))| = -(w.re + (j : \u211d)) := abs_of_neg (by rwa [\u2190 hrewj])\n rw [h2] at h1\n refine le_trans ?_ h1\n have h4 : ((j\u2080 - 1 - j : \u2115) : \u211d) = (j\u2080 : \u211d) - 1 - (j : \u211d) := by\n rw [Nat.cast_sub (by omega : j \u2264 j\u2080 - 1), Nat.cast_sub (by omega : 1 \u2264 j\u2080)]\n push_cast\n ring\n rw [h4]\n linarith [hj\u2080lt]\n have hpos : (0 : \u211d) < ((j\u2080 - 1 - j : \u2115) : \u211d) := by\n have h1 : (1 : \u2115) \u2264 j\u2080 - 1 - j := by omega\n exact_mod_cast h1\n exact (inv_le_inv\u2080 (by linarith [hge, hpos]) hpos).mpr hge\n\n/-- **The separated reciprocal sum bound (C)**: for dist(w, \u2212\u2115) \u2265 c > 0,\n\u03a3_{j<m} \u2016w+j\u2016\u207b\u00b9 \u2264 2/c + 2 + 2\u00b7log m (the V-split: at most one term per\nside needs the dist condition; the rest telescope into the harmonic bound). -/\ntheorem digamma_recip_sum_le {c : \u211d} (hc : 0 < c) {w : \u2102}\n (hdist : \u2200 m : \u2115, c \u2264 \u2016w + (m : \u2102)\u2016) {m : \u2115} (hm : \u2308-w.re\u2309\u208a + 1 \u2264 m) :\n \u2211 j \u2208 Finset.range m, \u2016(w + (j : \u2102))\u207b\u00b9\u2016 \u2264 2 / c + 2 + 2 * Real.log m := by\n set j\u2080 := \u2308-w.re\u2309\u208a with hj\u2080\n have hj\u2080m : j\u2080 \u2264 m := by omega\n have hm1 : 1 \u2264 m := by omega\n have hHarm : \u2200 K : \u2115, \u2211 i \u2208 Finset.range K, ((i : \u211d) + 1)\u207b\u00b9 \u2264 1 + Real.log K := by\n intro K\n have h := sum_one_div_le_one_add_log K\n simpa [one_div] using h\n have hlogmono : \u2200 {a b : \u2115}, 1 \u2264 a \u2192 a \u2264 b \u2192\n 1 + Real.log (a : \u211d) \u2264 1 + Real.log (b : \u211d) := by\n intro a b ha hab\n have h1 : (0 : \u211d) < (a : \u211d) := by exact_mod_cast ha\n have h2 : (a : \u211d) \u2264 (b : \u211d) := by exact_mod_cast hab\n have h3 := Real.log_le_log h1 h2\n linarith [h3]\n have hlogmono0 : \u2200 {a b : \u2115}, a \u2264 b \u2192 1 \u2264 b \u2192\n 1 + Real.log (a : \u211d) \u2264 1 + Real.log (b : \u211d) := by\n intro a b hab hb\n rcases eq_or_ne a 0 with ha | ha\n \u00b7 rw [ha, Nat.cast_zero, Real.log_zero]\n have h2 : (0 : \u211d) \u2264 Real.log (b : \u211d) := Real.log_nonneg (by exact_mod_cast hb)\n linarith [h2]\n \u00b7 exact hlogmono (Nat.one_le_iff_ne_zero.mpr ha) hab\n have hsplit : \u2211 j \u2208 Finset.range m, \u2016(w + (j : \u2102))\u207b\u00b9\u2016\n = \u2211 j \u2208 Finset.range j\u2080, \u2016(w + (j : \u2102))\u207b\u00b9\u2016\n + \u2211 j \u2208 Finset.Ico j\u2080 m, \u2016(w + (j : \u2102))\u207b\u00b9\u2016 := by\n rw [Finset.range_eq_Ico, Finset.range_eq_Ico,\n \u2190 Finset.sum_Ico_consecutive _ (Nat.zero_le j\u2080) hj\u2080m]\n rw [hsplit]\n -- RIGHT side\n have hfirst_r : \u2016(w + (j\u2080 : \u2102))\u207b\u00b9\u2016 \u2264 1 / c := by\n rw [norm_inv, show (1 : \u211d) / c = c\u207b\u00b9 by rw [one_div]]\n have hpos : (0 : \u211d) < \u2016w + (j\u2080 : \u2102)\u2016 := lt_of_lt_of_le hc (hdist j\u2080)\n exact (inv_le_inv\u2080 hpos hc).mpr (hdist j\u2080)\n have hrest_r : \u2211 j \u2208 Finset.Ico (j\u2080 + 1) m, \u2016(w + (j : \u2102))\u207b\u00b9\u2016 \u2264 1 + Real.log m := by\n calc \u2211 j \u2208 Finset.Ico (j\u2080 + 1) m, \u2016(w + (j : \u2102))\u207b\u00b9\u2016\n \u2264 \u2211 j \u2208 Finset.Ico (j\u2080 + 1) m, ((j - j\u2080 : \u2115) : \u211d)\u207b\u00b9 :=\n Finset.sum_le_sum fun j hj => recip_norm_le_right hdist hj\u2080 (by\n rw [Finset.mem_Ico] at hj; exact hj.1)\n _ = \u2211 i \u2208 Finset.range (m - (j\u2080 + 1)), ((i : \u211d) + 1)\u207b\u00b9 := by\n rw [Finset.sum_Ico_eq_sum_range]\n apply Finset.sum_congr rfl\n intro i _\n have h1 : (j\u2080 + 1 + i) - j\u2080 = i + 1 := by omega\n rw [h1, Nat.cast_add_one]\n _ \u2264 1 + Real.log (\u2191(m - (j\u2080 + 1)) : \u211d) := hHarm _\n _ \u2264 1 + Real.log m := hlogmono0 (show m - (j\u2080 + 1) \u2264 m by omega) hm1\n have hright : \u2211 j \u2208 Finset.Ico j\u2080 m, \u2016(w + (j : \u2102))\u207b\u00b9\u2016 \u2264 1 / c + (1 + Real.log m) := by\n have hsplit0 : \u2211 j \u2208 Finset.Ico j\u2080 m, \u2016(w + (j : \u2102))\u207b\u00b9\u2016\n = (\u2211 i \u2208 Finset.range (m - j\u2080 - 1), \u2016(w + ((j\u2080 + (i + 1) : \u2115)) : \u2102)\u207b\u00b9\u2016)\n + \u2016(w + (j\u2080 : \u2102))\u207b\u00b9\u2016 := by\n rw [Finset.sum_Ico_eq_sum_range]\n conv_lhs => rw [show m - j\u2080 = (m - j\u2080 - 1) + 1 by omega]\n rw [Finset.sum_range_succ']\n rw [add_zero]\n have hrest' : \u2211 i \u2208 Finset.range (m - j\u2080 - 1), \u2016(w + ((j\u2080 + (i + 1) : \u2115)) : \u2102)\u207b\u00b9\u2016\n \u2264 1 + Real.log m := by\n calc \u2211 i \u2208 Finset.range (m - j\u2080 - 1), \u2016(w + ((j\u2080 + (i + 1) : \u2115)) : \u2102)\u207b\u00b9\u2016\n \u2264 \u2211 i \u2208 Finset.range (m - j\u2080 - 1), ((i : \u211d) + 1)\u207b\u00b9 := by\n apply Finset.sum_le_sum\n intro i _\n have h1 := recip_norm_le_right hdist hj\u2080 (j := j\u2080 + (i + 1)) (by omega)\n have h2 : (j\u2080 + (i + 1)) - j\u2080 = i + 1 := by omega\n rw [h2] at h1\n have h3 : (((i + 1 : \u2115)) : \u211d)\u207b\u00b9 = ((i : \u211d) + 1)\u207b\u00b9 := by rw [Nat.cast_add_one]\n rwa [h3] at h1\n _ \u2264 1 + Real.log (\u2191(m - j\u2080 - 1) : \u211d) := hHarm _\n _ \u2264 1 + Real.log m := hlogmono0 (show m - j\u2080 - 1 \u2264 m by omega) hm1\n rw [hsplit0]\n calc (\u2211 i \u2208 Finset.range (m - j\u2080 - 1), \u2016(w + ((j\u2080 + (i + 1) : \u2115)) : \u2102)\u207b\u00b9\u2016)\n + \u2016(w + (j\u2080 : \u2102))\u207b\u00b9\u2016\n \u2264 (1 + Real.log m) + 1 / c := add_le_add hrest' hfirst_r\n _ = 1 / c + (1 + Real.log m) := by ring\n -- LEFT side\n have hleft : \u2211 j \u2208 Finset.range j\u2080, \u2016(w + (j : \u2102))\u207b\u00b9\u2016 \u2264 1 / c + (1 + Real.log m) := by\n by_cases hj\u20800 : j\u2080 = 0\n \u00b7 rw [hj\u20800]\n simp only [Finset.range_zero, Finset.sum_empty]\n have h1 : (0 : \u211d) \u2264 1 / c := by positivity\n have h2 : (0 : \u211d) \u2264 Real.log m := Real.log_nonneg (by exact_mod_cast hm1)\n linarith [h1, h2]\n \u00b7 have hj\u20801 : 1 \u2264 j\u2080 := Nat.one_le_iff_ne_zero.mpr hj\u20800\n have hdecomp : \u2211 j \u2208 Finset.range j\u2080, \u2016(w + (j : \u2102))\u207b\u00b9\u2016\n = \u2211 j \u2208 Finset.range (j\u2080 - 1), \u2016(w + (j : \u2102))\u207b\u00b9\u2016\n + \u2016(w + ((j\u2080 - 1 : \u2115) : \u2102))\u207b\u00b9\u2016 := by\n conv_lhs => rw [show j\u2080 = (j\u2080 - 1) + 1 by omega]\n rw [Finset.sum_range_succ]\n have hlast : \u2016(w + ((j\u2080 - 1 : \u2115) : \u2102))\u207b\u00b9\u2016 \u2264 1 / c := by\n have hpos : (0 : \u211d) < \u2016w + ((j\u2080 - 1 : \u2115) : \u2102)\u2016 := lt_of_lt_of_le hc (hdist (j\u2080 - 1))\n rw [norm_inv, show (1 : \u211d) / c = c\u207b\u00b9 by rw [one_div]]\n exact (inv_le_inv\u2080 hpos hc).mpr (hdist (j\u2080 - 1))\n have hrest_l : \u2211 j \u2208 Finset.range (j\u2080 - 1), \u2016(w + (j : \u2102))\u207b\u00b9\u2016 \u2264 1 + Real.log m := by\n calc \u2211 j \u2208 Finset.range (j\u2080 - 1), \u2016(w + (j : \u2102))\u207b\u00b9\u2016\n \u2264 \u2211 j \u2208 Finset.range (j\u2080 - 1), ((j\u2080 - 1 - j : \u2115) : \u211d)\u207b\u00b9 :=\n Finset.sum_le_sum fun j hj => recip_norm_le_left hdist hj\u2080 (by\n rw [Finset.mem_range] at hj; omega)\n _ = \u2211 i \u2208 Finset.range (j\u2080 - 1), ((i : \u211d) + 1)\u207b\u00b9 := by\n apply Finset.sum_bij (fun j _ => j\u2080 - 2 - j)\n \u00b7 intro j hj\n rw [Finset.mem_range] at hj\n exact Finset.mem_range.mpr (by omega)\n \u00b7 intro j\u2081 hj\u2081 j\u2082 hj\u2082 h\n rw [Finset.mem_range] at hj\u2081 hj\u2082\n omega\n \u00b7 intro i hi\n rw [Finset.mem_range] at hi\n exact \u27e8j\u2080 - 2 - i, Finset.mem_range.mpr (by omega), by omega\u27e9\n \u00b7 intro j hj\n rw [Finset.mem_range] at hj\n have h1 : ((j\u2080 - 1 - j : \u2115) : \u211d) = ((j\u2080 - 2 - j : \u2115) : \u211d) + 1 := by\n rw [Nat.cast_sub (by omega : j \u2264 j\u2080 - 1),\n Nat.cast_sub (by omega : j \u2264 j\u2080 - 2),\n Nat.cast_sub hj\u20801,\n Nat.cast_sub (by omega : (2 : \u2115) \u2264 j\u2080)]\n push_cast\n ring\n rw [h1]\n _ \u2264 1 + Real.log (\u2191(j\u2080 - 1) : \u211d) := hHarm _\n _ \u2264 1 + Real.log m := hlogmono0 (show j\u2080 - 1 \u2264 m by omega) hm1\n calc \u2211 j \u2208 Finset.range j\u2080, \u2016(w + (j : \u2102))\u207b\u00b9\u2016\n = \u2211 j \u2208 Finset.range (j\u2080 - 1), \u2016(w + (j : \u2102))\u207b\u00b9\u2016\n + \u2016(w + ((j\u2080 - 1 : \u2115) : \u2102))\u207b\u00b9\u2016 := hdecomp\n _ \u2264 (1 + Real.log m) + 1 / c := add_le_add hrest_l hlast\n _ = 1 / c + (1 + Real.log m) := by ring\n have hcc : (2 : \u211d) / c = 1 / c + 1 / c := by ring\n rw [hcc]\n linarith [hleft, hright]\n\n/-! ## 4. The near-axis left-plane bound (A) -/\n\n/-- The digamma recurrence over a natural shift, pole-avoidance form\n(weaker hypothesis than LiReflect's `digamma_add_natCast`, which needs\nim w \u2260 0 \u2014 the near-axis application includes real points). -/\ntheorem digamma_add_natCast' {w : \u2102} (hw : \u2200 k : \u2115, w \u2260 -(k : \u2102)) (n : \u2115) :\n Complex.digamma (w + n) = Complex.digamma w + \u2211 j \u2208 Finset.range n, (w + (j : \u2102))\u207b\u00b9 := by\n induction n with\n | zero => simp\n | succ k ih =>\n have hne : \u2200 m : \u2115, w + (k : \u2102) \u2260 -(m : \u2102) := by\n intro m h\n apply hw (k + m)\n have h3 : w = -(m : \u2102) - (k : \u2102) := by\n have h4 := congrArg (\u00b7 - (k : \u2102)) h\n rwa [add_sub_cancel_right] at h4\n rw [h3]\n push_cast\n ring\n have h1 := Complex.digamma_apply_add_one (w + (k : \u2102)) hne\n rw [show w + ((k + 1 : \u2115) : \u2102) = (w + (k : \u2102)) + 1 by push_cast; ring, h1, ih,\n Finset.sum_range_succ]\n ring\n\n/-- **The near-axis left-plane digamma bound (A)**: for re w \u2264 2 and\ndist(w, \u2212\u2115) \u2265 c > 0, \u2016\u03c8(w)\u2016 \u2264 (46 + 2/c) + 23\u00b7log(2+\u2016w\u2016). Recurrence\nto re \u2208 [3, 4] (`digamma_add_natCast'`) + \u00a73's sum bound + the\nlanding-zone bound (StirlingVert for |im| \u2265 1/2, \u00a72's (B) for |im| < 1/2). -/\ntheorem norm_digamma_le_of_dist_nat {c : \u211d} (hc : 0 < c) {w : \u2102}\n (hwre : w.re \u2264 2) (hdist : \u2200 m : \u2115, c \u2264 \u2016w + (m : \u2102)\u2016) :\n \u2016Complex.digamma w\u2016 \u2264 (46 + 2 / c) + 23 * Real.log (2 + \u2016w\u2016) := by\n -- pole-avoidance from the dist condition\n have hpoles : \u2200 k : \u2115, w \u2260 -(k : \u2102) := by\n intro k h\n have h1 := hdist k\n rw [h] at h1\n rw [show (-(k : \u2102)) + (k : \u2102) = 0 by ring, norm_zero] at h1\n linarith [hc, h1]\n -- the shift count: lands re(w + m) \u2208 [3, 4)\n set m := \u23082 - w.re\u2309\u208a + 1 with hm_def\n have hm1 : 1 \u2264 m := by omega\n have hm_ge : (2 : \u211d) - w.re \u2264 (m : \u211d) := by\n have h := Nat.le_ceil (2 - w.re)\n rw [hm_def]\n push_cast\n linarith [h]\n have hm_lt : (m : \u211d) < (2 - w.re) + 2 := by\n have h := Nat.ceil_lt_add_one (show (0 : \u211d) \u2264 2 - w.re by linarith [hwre])\n have h2 : ((\u23082 - w.re\u2309\u208a : \u2115) : \u211d) < (2 - w.re) + 1 := by exact_mod_cast h\n rw [hm_def]\n push_cast\n linarith [h2]\n set v := w + (m : \u2102) with hv_def\n have hvre : 3 \u2264 v.re \u2227 v.re < 4 := by\n have h1 : v.re = w.re + (m : \u211d) := by\n rw [hv_def]\n simp [Complex.add_re, Complex.natCast_re]\n rw [h1]\n constructor <;> linarith [hm_ge, hm_lt]\n have hvim : v.im = w.im := by\n rw [hv_def]\n simp [Complex.add_im, Complex.natCast_im]\n have hvnorm3 : 3 \u2264 \u2016v\u2016 := by\n have h1 := Complex.abs_re_le_norm v\n rw [abs_of_nonneg (by linarith [hvre.1])] at h1\n linarith [hvre.1, h1]\n -- j\u2080 for the sum bound\n have hj\u2080m : \u2308-w.re\u2309\u208a + 1 \u2264 m := by\n by_cases hre : 0 \u2264 -w.re\n \u00b7 have h1 : ((\u2308-w.re\u2309\u208a : \u2115) : \u211d) < -w.re + 1 := by\n have h := Nat.ceil_lt_add_one hre\n exact_mod_cast h\n have h2 : ((\u2308-w.re\u2309\u208a + 1 : \u2115) : \u211d) < (m : \u211d) := by\n have h3 : ((\u2308-w.re\u2309\u208a + 1 : \u2115) : \u211d) = ((\u2308-w.re\u2309\u208a : \u2115) : \u211d) + 1 := Nat.cast_add_one _\n linarith [h1, hm_ge, h3]\n have h3 : \u2308-w.re\u2309\u208a + 1 < m := by exact_mod_cast h2\n omega\n \u00b7 push Not at hre\n have h1 : \u2308-w.re\u2309\u208a = 0 := Nat.ceil_eq_zero.mpr (by linarith [hre])\n rw [h1]\n omega\n -- the recurrence + the sum bound\n have hshift : Complex.digamma v\n = Complex.digamma w + \u2211 j \u2208 Finset.range m, (w + (j : \u2102))\u207b\u00b9 := by\n rw [hv_def]\n exact digamma_add_natCast' hpoles m\n have hsum : \u2211 j \u2208 Finset.range m, \u2016(w + (j : \u2102))\u207b\u00b9\u2016 \u2264 2 / c + 2 + 2 * Real.log m :=\n digamma_recip_sum_le hc hdist hj\u2080m\n -- the landing-zone bound\n have hLZ : \u2016Complex.digamma v\u2016 \u2264 21 * Real.log (2 + \u2016v\u2016) := by\n by_cases him : 1 / 2 \u2264 |v.im|\n \u00b7 have hst := StirlingVert.digamma_stirling (by linarith [hvre.1] : (0 : \u211d) < v.re) him\n have hnorm12 : \u2016(1 / 2 : \u2102)\u2016 = 1 / 2 := by\n rw [show (1 / 2 : \u2102) = ((1 / 2 : \u211d) : \u2102) by norm_num, Complex.norm_real,\n Real.norm_eq_abs, abs_of_nonneg (by norm_num : (0 : \u211d) \u2264 1 / 2)]\n calc \u2016Complex.digamma v\u2016\n = \u2016(Complex.digamma v - Complex.log v + (1 / 2 : \u2102) / v) + Complex.log v\n - (1 / 2 : \u2102) / v\u2016 := by\n congr 1; ring\n _ \u2264 \u2016Complex.digamma v - Complex.log v + (1 / 2 : \u2102) / v\u2016 + \u2016Complex.log v\u2016\n + \u2016(1 / 2 : \u2102) / v\u2016 := by\n refine (norm_sub_le _ _).trans ?_\n exact add_le_add_left (norm_add_le _ _) _\n _ \u2264 3 / v.im ^ 2 + (Real.log \u2016v\u2016 + Real.pi) + (1 / 2) / \u2016v\u2016 := by\n refine add_le_add (add_le_add hst (norm_log_le_of_one_le (by linarith [hvnorm3]))) ?_\n rw [norm_div, hnorm12]\n _ \u2264 21 * Real.log (2 + \u2016v\u2016) := by\n have him2 : (1 : \u211d) / 4 \u2264 v.im ^ 2 := by\n calc (1 : \u211d) / 4 = (1 / 2) ^ 2 := by norm_num\n _ \u2264 |v.im| ^ 2 := pow_le_pow_left\u2080 (abs_nonneg _) him _\n _ = v.im ^ 2 := by rw [sq_abs]\n have hlogv : Real.log \u2016v\u2016 \u2264 Real.log (2 + \u2016v\u2016) :=\n Real.log_le_log (by linarith [hvnorm3]) (by linarith)\n have hlog5 : (0 : \u211d) \u2264 Real.log (2 + \u2016v\u2016) :=\n Real.log_nonneg (by linarith [hvnorm3])\n have hpi : Real.pi \u2264 4 := Real.pi_lt_d2.le.trans (by norm_num)\n have h1 : 3 / v.im ^ 2 \u2264 12 := by\n rw [div_le_iff\u2080 (by linarith [him2] : (0 : \u211d) < v.im ^ 2)]\n nlinarith [him2]\n have h2 : (1 / 2 : \u211d) / \u2016v\u2016 \u2264 1 := by\n rw [div_le_one (by linarith [hvnorm3] : (0 : \u211d) < \u2016v\u2016)]\n linarith [hvnorm3]\n nlinarith [h1, h2, hlogv, hpi, hlog5]\n \u00b7 push Not at him\n have hB := norm_digamma_le_of_two_le_re (by linarith [hvre.1] : (2 : \u211d) \u2264 v.re)\n (by linarith [him.le] : |v.im| \u2264 5)\n have hlognonneg : (0 : \u211d) \u2264 Real.log (2 + \u2016v\u2016) :=\n Real.log_nonneg (by linarith [hvnorm3])\n nlinarith [hB, hlognonneg]\n -- norms and log comparisons\n have hwm : (m : \u211d) \u2264 4 + \u2016w\u2016 := by\n have h1 : (m : \u211d) \u2264 (2 - w.re) + 2 := hm_lt.le\n have h2 : -w.re \u2264 \u2016w\u2016 := (neg_le_abs w.re).trans (Complex.abs_re_le_norm w)\n linarith [h1, h2]\n have hvnorm : \u2016v\u2016 \u2264 2 * \u2016w\u2016 + 4 := by\n rw [hv_def]\n calc \u2016w + (m : \u2102)\u2016 \u2264 \u2016w\u2016 + \u2016(m : \u2102)\u2016 := norm_add_le _ _\n _ = \u2016w\u2016 + (m : \u211d) := by rw [RCLike.norm_natCast]\n _ \u2264 2 * \u2016w\u2016 + 4 := by linarith [hwm]\n have hlogv_le : Real.log (2 + \u2016v\u2016) \u2264 2 + Real.log (2 + \u2016w\u2016) := by\n have h1 : 2 + \u2016v\u2016 \u2264 4 * (2 + \u2016w\u2016) := by linarith [hvnorm]\n have hposv : (0 : \u211d) < 2 + \u2016v\u2016 := by linarith [hvnorm3]\n have h2 : Real.log (2 + \u2016v\u2016) \u2264 Real.log (4 * (2 + \u2016w\u2016)) := Real.log_le_log hposv h1\n have h3 : Real.log (4 * (2 + \u2016w\u2016)) = Real.log 4 + Real.log (2 + \u2016w\u2016) :=\n Real.log_mul (by norm_num : (4 : \u211d) \u2260 0) (by positivity : (2 + \u2016w\u2016) \u2260 0)\n have h4 : Real.log 4 \u2264 2 := by\n have h5 := Real.log_two_lt_d9.le\n have h6 : Real.log 4 = 2 * Real.log 2 := by\n rw [show (4 : \u211d) = 2 ^ 2 by norm_num, Real.log_pow]\n push_cast\n ring\n linarith [h5, h6]\n linarith [h2, h3, h4]\n have hlogm : Real.log m \u2264 1 + Real.log (2 + \u2016w\u2016) := by\n have hmpos : (0 : \u211d) < (m : \u211d) := by exact_mod_cast hm1\n have h1 : (m : \u211d) \u2264 2 * (2 + \u2016w\u2016) := by linarith [hwm]\n have h2 : Real.log (m : \u211d) \u2264 Real.log (2 * (2 + \u2016w\u2016)) := Real.log_le_log hmpos h1\n have h3 : Real.log (2 * (2 + \u2016w\u2016)) = Real.log 2 + Real.log (2 + \u2016w\u2016) :=\n Real.log_mul (by norm_num) (by positivity)\n have h4 : Real.log 2 \u2264 1 := Real.log_two_lt_d9.le.trans (by norm_num)\n linarith [h2, h3, h4]\n -- the final assembly\n have hpsi : Complex.digamma w\n = Complex.digamma v - \u2211 j \u2208 Finset.range m, (w + (j : \u2102))\u207b\u00b9 := by\n linear_combination hshift\n rw [hpsi]\n calc \u2016Complex.digamma v - \u2211 j \u2208 Finset.range m, (w + (j : \u2102))\u207b\u00b9\u2016\n \u2264 \u2016Complex.digamma v\u2016 + \u2016\u2211 j \u2208 Finset.range m, (w + (j : \u2102))\u207b\u00b9\u2016 := norm_sub_le _ _\n _ \u2264 21 * Real.log (2 + \u2016v\u2016) + (2 / c + 2 + 2 * Real.log m) :=\n add_le_add hLZ ((norm_sum_le _ _).trans hsum)\n _ \u2264 (46 + 2 / c) + 23 * Real.log (2 + \u2016w\u2016) := by\n linarith [hlogv_le, hlogm]\n\n/-! ## 5. The general logDeriv \u0393R identity (G) -/\n\n/-- logDeriv of a finite product of the linear factors (z/2 + j),\nvalid for im s \u2260 0 (each factor nonzero). -/\ntheorem logDeriv_prod_range_linear {s : \u2102} (hs : s.im \u2260 0) (m : \u2115) :\n logDeriv (fun z : \u2102 => \u220f j \u2208 Finset.range m, (z / 2 + (j : \u2102))) s\n = \u2211 j \u2208 Finset.range m, (1 / 2 : \u2102) / (s / 2 + (j : \u2102)) := by\n have hne : \u2200 j : \u2115, (s / 2 + (j : \u2102)) \u2260 0 := by\n intro j h\n apply hs\n have h1 : (s / 2 + (j : \u2102)).im = 0 := by rw [h]; simp\n have h2 : (s / 2 + (j : \u2102)).im = s.im / 2 := by\n simp [Complex.add_im, Complex.natCast_im, Complex.div_ofNat_im]\n rw [h2] at h1\n linarith [h1]\n induction m with\n | zero => simp [logDeriv_const]\n | succ k ih =>\n rw [Finset.prod_range_succ]\n rw [logDeriv_mul s (Finset.prod_ne_zero_iff.mpr fun j _ => hne j) (hne k)\n (by fun_prop) (by fun_prop)]\n rw [ih]\n have hfac : logDeriv (fun z : \u2102 => z / 2 + (k : \u2102)) s = (1 / 2 : \u2102) / (s / 2 + (k : \u2102)) := by\n have h1 : HasDerivAt (fun z : \u2102 => z / 2 + (k : \u2102)) (1 / 2 : \u2102) s :=\n ((hasDerivAt_id' s).div_const 2).add_const (k : \u2102)\n rw [logDeriv_apply, h1.deriv]\n rw [hfac, Finset.sum_range_succ]\n\n/-- **(G) the general logDeriv \u0393R identity**: for im s \u2260 0,\nlogDeriv \u0393R s = \u2212(log \u03c0)/2 + \u00bd\u03c8(s/2) \u2014 the m-fold shift landing in\nre > 0 (`gamma_mul_prod` + `digamma_add_natCast` + 5d's EventuallyEq\nmachinery). -/\ntheorem logDeriv_Gamma\u211d_eq {s : \u2102} (hs : s.im \u2260 0) :\n logDeriv Complex.Gamma\u211d s\n = -(Real.log Real.pi : \u2102) / 2 + (1 / 2 : \u2102) * Complex.digamma (s / 2) := by\n set m := \u2308max 0 (-(s.re / 2))\u2309\u208a + 1 with hm_def\n have hmge : (2 : \u211d) \u2264 s.re + 2 * (m : \u211d) := by\n have h1 : max 0 (-(s.re / 2)) \u2264 ((\u2308max 0 (-(s.re / 2))\u2309\u208a : \u2115) : \u211d) := Nat.le_ceil _\n have h2 : -(s.re / 2) \u2264 max 0 (-(s.re / 2)) := le_max_right _ _\n rw [hm_def]\n push_cast\n linarith [h1, h2]\n have hres2 : (0 : \u211d) < (s + 2 * (m : \u2102)).re := by\n have h1 : (s + 2 * (m : \u2102)).re = s.re + 2 * (m : \u211d) := by\n simp [Complex.add_re, Complex.mul_re, Complex.natCast_re]\n rw [h1]\n linarith [hmge]\n have hs2im : (s / 2).im \u2260 0 := by\n have h1 : (s / 2).im = s.im / 2 := by simp [Complex.div_ofNat_im]\n rw [h1]\n exact div_ne_zero hs (by norm_num : (2 : \u211d) \u2260 0)\n -- the pointwise identity on U = {im \u2260 0}\n have hU : IsOpen {z : \u2102 | z.im \u2260 0} := isOpen_ne_fun Complex.continuous_im continuous_const\n have hPne : \u2200 z : \u2102, z.im \u2260 0 \u2192 (\u220f j \u2208 Finset.range m, (z / 2 + (j : \u2102))) \u2260 0 := by\n intro z hz\n apply Finset.prod_ne_zero_iff.mpr\n intro j _\n intro h\n apply hz\n have h1 : (z / 2 + (j : \u2102)).im = 0 := by rw [h]; simp\n have h2 : (z / 2 + (j : \u2102)).im = z.im / 2 := by\n simp [Complex.add_im, Complex.natCast_im, Complex.div_ofNat_im]\n rw [h2] at h1\n linarith [h1]\n have hpt : \u2200 z : \u2102, z.im \u2260 0 \u2192 Complex.Gamma\u211d z\n = ((Real.pi ^ m : \u211d) : \u2102) * Complex.Gamma\u211d (z + 2 * (m : \u2102))\n / \u220f j \u2208 Finset.range m, (z / 2 + (j : \u2102)) := by\n intro z hz\n have hside : \u2200 k : \u2115, k < m \u2192 z / 2 \u2260 -(k : \u2102) := by\n intro k _ h\n apply hz\n have h1 : (z / 2).im = 0 := by\n have h2 := congrArg Complex.im h\n simpa [Complex.neg_im, Complex.natCast_im] using h2\n simp [Complex.div_ofNat_im] at h1\n linarith [h1]\n have hrec := gamma_mul_prod (z / 2) m hside\n -- \u0393R(z+2m) = \u03c0^{\u2212(z+2m)/2}\u00b7\u0393(z/2+m) = (\u03c0^m)\u207b\u00b9\u00b7\u0393R(z)\u00b7\u220f\n have hG2 : Complex.Gamma\u211d (z + 2 * (m : \u2102))\n = ((Real.pi ^ m : \u211d) : \u2102)\u207b\u00b9 * Complex.Gamma\u211d z\n * \u220f j \u2208 Finset.range m, (z / 2 + (j : \u2102)) := by\n rw [Complex.Gamma\u211d_def, Complex.Gamma\u211d_def]\n rw [show (-(z + 2 * (m : \u2102)) / 2) = -z / 2 - (m : \u2102) by ring]\n rw [show ((z + 2 * (m : \u2102)) / 2) = z / 2 + (m : \u2102) by ring]\n -- the cpow split\n have hpi : (Real.pi : \u2102) ^ (-z / 2 - (m : \u2102))\n = (Real.pi : \u2102) ^ (-z / 2) * ((Real.pi ^ m : \u211d) : \u2102)\u207b\u00b9 := by\n have hlog : Complex.log (Real.pi : \u2102) = (Real.log Real.pi : \u2102) :=\n (Complex.ofReal_log Real.pi_nonneg).symm\n rw [Complex.cpow_def_of_ne_zero (by exact_mod_cast Real.pi_ne_zero : (Real.pi : \u2102) \u2260 0) _,\n Complex.cpow_def_of_ne_zero (by exact_mod_cast Real.pi_ne_zero : (Real.pi : \u2102) \u2260 0) _,\n hlog]\n have harg : (Real.log Real.pi : \u2102) * (-z / 2 - (m : \u2102))\n = (Real.log Real.pi : \u2102) * (-z / 2) + ((-(m : \u211d) * Real.log Real.pi : \u211d) : \u2102) := by\n push_cast\n ring\n rw [harg, Complex.exp_add, \u2190 Complex.ofReal_exp]\n have hexp : Real.exp (-(m : \u211d) * Real.log Real.pi) = (Real.pi ^ m)\u207b\u00b9 := by\n have h1 : (-(m : \u211d) * Real.log Real.pi) = Real.log ((Real.pi ^ m)\u207b\u00b9) := by\n rw [Real.log_inv, Real.log_pow]\n ring\n rw [h1, Real.exp_log (by positivity)]\n rw [hexp, Complex.ofReal_inv, Complex.ofReal_pow]\n rw [hpi, \u2190 hrec]\n ring\n rw [eq_div_iff (hPne z hz), hG2]\n field_simp [show ((Real.pi ^ m : \u211d) : \u2102) \u2260 0 by exact_mod_cast pow_ne_zero m Real.pi_ne_zero]\n ring\n -- the EventuallyEq + the logDeriv computation\n have hEv : Complex.Gamma\u211d =\u1da0[\ud835\udcdd s]\n fun z => ((Real.pi ^ m : \u211d) : \u2102) * Complex.Gamma\u211d (z + 2 * (m : \u2102))\n / \u220f j \u2208 Finset.range m, (z / 2 + (j : \u2102)) := by\n filter_upwards [hU.mem_nhds hs] with z hz using hpt z hz\n have hG2m : Complex.Gamma\u211d (s + 2 * (m : \u2102)) \u2260 0 :=\n Complex.Gamma\u211d_ne_zero_of_re_pos hres2\n have h\u03c0ne : ((Real.pi ^ m : \u211d) : \u2102) \u2260 0 := by exact_mod_cast pow_ne_zero m Real.pi_ne_zero\n have hdG2m : DifferentiableAt \u2102 (fun z : \u2102 => Complex.Gamma\u211d (z + 2 * (m : \u2102))) s := by\n have h1 : (s + 2 * (m : \u2102)).im \u2260 0 := by\n have h2 : (s + 2 * (m : \u2102)).im = s.im := by\n simp [Complex.add_im, Complex.mul_im, Complex.natCast_im]\n rwa [h2]\n exact (differentiableAt_Gamma\u211d_of_im_ne_zero' h1).comp s\n (differentiableAt_id.add_const _)\n have hdP : DifferentiableAt \u2102 (fun z : \u2102 => \u220f j \u2208 Finset.range m, (z / 2 + (j : \u2102))) s := by\n fun_prop\n rw [logDeriv_congr hEv]\n have hstep1 : logDeriv (fun z : \u2102 => ((Real.pi ^ m : \u211d) : \u2102) * Complex.Gamma\u211d (z + 2 * (m : \u2102))\n / \u220f j \u2208 Finset.range m, (z / 2 + (j : \u2102))) s\n = logDeriv (fun z : \u2102 => ((Real.pi ^ m : \u211d) : \u2102) * Complex.Gamma\u211d (z + 2 * (m : \u2102))) s\n - logDeriv (fun z : \u2102 => \u220f j \u2208 Finset.range m, (z / 2 + (j : \u2102))) s :=\n logDeriv_div s (mul_ne_zero h\u03c0ne hG2m) (hPne s hs)\n ((differentiableAt_const _).mul hdG2m) hdP\n have hstep2 : logDeriv (fun z : \u2102 => ((Real.pi ^ m : \u211d) : \u2102) * Complex.Gamma\u211d (z + 2 * (m : \u2102))) s\n = logDeriv Complex.Gamma\u211d (s + 2 * (m : \u2102)) := by\n rw [logDeriv_const_mul s _ h\u03c0ne]\n have hder : deriv (fun z : \u2102 => Complex.Gamma\u211d (z + 2 * (m : \u2102))) s\n = deriv Complex.Gamma\u211d (s + 2 * (m : \u2102)) := by\n have h1 : (s + 2 * (m : \u2102)).im \u2260 0 := by\n have h2 : (s + 2 * (m : \u2102)).im = s.im := by\n simp [Complex.add_im, Complex.mul_im, Complex.natCast_im]\n rwa [h2]\n have h3 := ((differentiableAt_Gamma\u211d_of_im_ne_zero' h1).hasDerivAt).comp s\n ((hasDerivAt_id' s).add_const (2 * (m : \u2102)))\n have h4 : deriv (fun z : \u2102 => Complex.Gamma\u211d (z + 2 * (m : \u2102))) s\n = deriv Complex.Gamma\u211d (s + 2 * (m : \u2102)) * 1 := h3.deriv\n rwa [mul_one] at h4\n simp only [logDeriv_apply, hder]\n rw [hstep1, hstep2]\n have hev : logDeriv Complex.Gamma\u211d (s + 2 * (m : \u2102))\n = -(Real.log Real.pi : \u2102) / 2 + (1 / 2 : \u2102) * Complex.digamma ((s + 2 * (m : \u2102)) / 2) :=\n RvM.logDeriv_Gamma\u211d hres2\n rw [hev, logDeriv_prod_range_linear hs m]\n rw [show (s + 2 * (m : \u2102)) / 2 = s / 2 + (m : \u2102) by ring, digamma_add_natCast hs2im m]\n have hsumform : \u2211 j \u2208 Finset.range m, (1 / 2 : \u2102) / (s / 2 + (j : \u2102))\n = (1 / 2 : \u2102) * \u2211 j \u2208 Finset.range m, (s / 2 + (j : \u2102))\u207b\u00b9 := by\n rw [Finset.mul_sum]\n apply Finset.sum_congr rfl\n intro j _\n rw [div_eq_mul_inv]\n rw [hsumform]\n ring\n\nend NguyenRH1\n\nend\n\n",
"structuredPatch": [
{
"oldStart": 730,
"oldLines": 7,
"newStart": 730,
"newLines": 7,
"lines": [
" -- the shift count: lands re(w + m) \u2208 [3, 4)",
" set m := \u23082 - w.re\u2309\u208a + 1 with hm_def",
" have hm1 : 1 \u2264 m := by omega",
"- have hm_ge : (2 : \u211d) - w.re \u2264 (m : \u211d) := by",
"+ have hm_ge : (2 : \u211d) - w.re + 1 \u2264 (m : \u211d) := by",
" have h := Nat.le_ceil (2 - w.re)",
" rw [hm_def]",
" push_cast"
]
}
],
"userModified": false,
"replaceAll": false
}
raw content_json (database row)
[{"type":"thinking","thinking":"The probe with `(fun z => dpsiTermC z n) = (fun s => 1/(↑n+1) − 1/(s+↑n+1))` by rfl works. So the function forms are fine.\n\nThe remaining possibility: in the FILE, the hf2 goal's function is NOT the reduced form — and my `show` produced the reduced form — but the error persists — meaning the show's term is NOT defeq to the goal's?! The hf2 goal: `DifferentiableAt ℂ (iteratedDerivWithin j (fun z ↦ f n z) dpsiDomain) r` with f := the family — the `fun z ↦ f n z` — with f = `fun (m:ℕ) => fun (s:ℂ) => dpsiTermC s m`?? — wait NO — the tsum in my iteratedDerivWithin_tsum_dpsiTermC's statement: `fun s : ℂ => ∑' m : ℕ, dpsiTermC s m` — the iteratedDerivWithin_tsum lemma is about `fun z ↦ ∑' n, f n z` with f : ι → 𝕜 → F — matching `∑' n, f n z` with `∑' m, dpsiTermC s m`: f n z := dpsiTermC z n — so f := fun m => fun z => dpsiTermC z m?? — hmm — the elaboration: `∑' m : ℕ, dpsiTermC s m` = tsum (fun m => dpsiTermC s m) — so the family is `fun m => dpsiTermC s m` — with s the OUTER lambda's bound var. When the lemma is instantiated, f := fun m => dpsiTermC ?s m — NO — the lemma's f is a fixed function ι → 𝕜 → F — the unification: (fun z => ∑' n, f n z) =?= (fun s => ∑' m, dpsiTermC s m) — so f n z := dpsiTermC z n — f := fun m => fun z => dpsiTermC z m — then hf2's `fun z ↦ f n z` = `fun z => (fun m => fun z => dpsiTermC z m) n z` — a beta-redex — and my show's target `fun z : ℂ => dpsiTermC z n` — defeq via beta ✓ — show should bridge...\n\nHmm — unless the error is happening at a DIFFERENT point than I think. Let me look at the current line 772's actual content after my edit — the `show` is at line ~767 now. The error at 772:10 — that's the `rw [h5]`?? or the show? Let me count: 765-777 area — the `show` is at 767-ish, `have h5` at 768-770, `rw [h5]` at 771-772. The error at 772:10 = rw [h5]. And the goal shown: `DifferentiableAt ℂ (iteratedDerivWithin j (fun z => dpsiTermC z n) dpsiDomain) r` — the show ALREADY changed the goal to the reduced form (the display matches h5's LHS exactly) — and rw [h5] STILL fails!?!? — that means h5's LHS term ≠ the goal's term as ELABORATED — both display identically — so there's a hidden instance/def difference. The candidates: the `iteratedDerivWithin` — the field instance — ℂ's DenselyNormedField etc. — could differ by instance PATH: my lemma iteratedDerivWithin_dpsiTermC was proved in the file with `open ... Real` etc. — the instances are the same... \n\nWAIT — I just realized — maybe it's the `dpsiTermC` — in hf2's goal, the family is the one from MY iteratedDerivWithin_tsum_dpsiTermC's statement — `fun s : ℂ => ∑' m : ℕ, dpsiTermC s m` — so the family inside hf2 is `fun m => dpsiTermC ?s m` with ?s := z (the hf2 lambda binder) — i.e. `fun z ↦ (fun m => dpsiTermC ?s m) ...` hmm.\n\nLet me take yet another approach to see the real terms: in the FILE, at the hf2 branch, add `show` with the FULLY-EXPLICIT expected — or better, use `conv` to unfold. Actually — cleanest: use `set_option tactic.hygienic false`? no. Let me use `change` with the exact term from h5's type, and if change fails, the error message will show the mismatch:\n\nActually — let me use a different strategy entirely: `first | rw [h5] | rw [h5']`? no. Let me use `Strachey`... no. Let me try `simp only [h5]`:","signature":""},{"type":"text","text":"Let me try `simp only [h5]` (which uses a different matching discipline than rw)."},{"type":"tool_use","id":"Edit_442","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigamma.lean","old_string":" · show DifferentiableAt ℂ (iteratedDerivWithin j (fun z : ℂ => dpsiTermC z n) dpsiDomain) r\n have h5 : iteratedDerivWithin j (fun z : ℂ => dpsiTermC z n) dpsiDomain r =\n -((-1 : ℂ)) ^ j * (j ! : ℂ) * (r + ↑n + 1) ^ (-(j : ℤ) - 1) :=\n iteratedDerivWithin_dpsiTermC j (by omega) n hr\n rw [h5]","new_string":" · have h5 : _ = _ := iteratedDerivWithin_dpsiTermC j (by omega) n hr\n simp only [h5]"},"extra_content":null}]