[{"type":"thinking","thinking":"§1+§2 compile clean! That's the telescope + the right-half bound (B). Now §3 (C — the separated reciprocal sum), §4 (A — the near-axis bound), §5 (G — the general logDeriv ΓR identity). Let me write §3 (C) next.\n\n**(C) `digamma_recip_sum_le`**: for w with ∀ m : ℕ, c ≤ ‖w + ↑m‖ (c > 0) and j₀ := ⌈−w.re⌉₊ with j₀ + 1 ≤ m:\n  Σ_{j ∈ range m} ‖(w + ↑j)⁻¹‖ ≤ 2/c + 2 + 2·log m.\n\nPlan (V-split at j₀):\n- range m = range j₀ ∪ Ico j₀ m — via Finset.range_eq_Ico + sum_Ico_consecutive (reversed): ∑ range m = ∑ Ico 0 j₀ + ∑ Ico j₀ m hmm: Ico 0 m = Ico 0 j₀ ∪ Ico j₀ m (disjoint): Finset.sum_Ico_consecutive (f) (h1 : 0 ≤ j₀) (h2 : j₀ ≤ m) : ∑ Ico 0 j₀ + ∑ Ico j₀ m = ∑ Ico 0 m ✓. So ∑ range m f = ∑ range j₀ f + ∑ Ico j₀ m f (with range_eq_Ico).\n- Right side Ico j₀ m: split first term j₀ (≤ 1/c via hdist) + rest Ico (j₀+1) m: each ≤ 1/(j − j₀) (real-part bound): re(w + ↑j) = w.re + j ≥ j − j₀ (since w.re + j₀ ≥ 0: j₀ = ⌈−w.re⌉₊ ≥ −w.re ⟹ w.re + j₀ ≥ 0 ✓): so ‖w + ↑j‖ ≥ |re(w+↑j)| = w.re + j (nonneg ✓) ≥ (j:ℝ) − j₀: ‖(w+↑j)⁻¹‖ = ‖w+↑j‖⁻¹ ≤ ((j:ℝ)−j₀)⁻¹·... ((j:ℝ) − j₀: with j > j₀: (j−j₀ : ℕ) cast: ((j−j₀:ℕ):ℝ) = j − j₀ ≥ 1: so ≤ 1/(j−j₀) as positive reals. Then Σ_{j ∈ Ico (j₀+1) m} 1/(j−j₀) = Σ_{i ∈ range (m − j₀ − 1)} 1/(i+1) (reindex via Finset.sum_Ico_eq_sum_range) ≤ 1 + log(m − j₀ − 1) ≤ 1 + log m (sum_one_div_le_one_add_log + log mono...). Hmm — the reindex: ∑ j ∈ Ico (j₀+1) m, (1:ℝ)/((j:ℝ) − j₀)... the term is 1/((j:ℝ) − (j₀:ℝ))... with casts of Nat-sub. Let me phrase the term bound as ‖(w+↑j)⁻¹‖ ≤ ((j − j₀ : ℕ) : ℝ)⁻¹ (using the ℕ-sub cast): then reindex ∑ j ∈ Ico (j₀+1) m, ((j−j₀:ℕ):ℝ)⁻¹ = ∑ i ∈ range (m − (j₀+1)), (((j₀+1+i) − j₀ : ℕ):ℝ)⁻¹ = ∑ i, ((i+1:ℕ):ℝ)⁻¹ — via sum_Ico_eq_sum_range: ∑ i ∈ range (m − (j₀+1)), f (j₀+1+i): f j := ((j − j₀:ℕ):ℝ)⁻¹: f (j₀+1+i) = (((j₀+1+i) − j₀:ℕ):ℝ)⁻¹ = ((i+1:ℕ):ℝ)⁻¹: Nat-sub: (j₀+1+i) − j₀ = i+1 (omega) — `Nat.add_sub_cancel_left`? (j₀ + (1+i)) − j₀ = 1+i ✓ via add_comm/Nat.add_sub_cancel_left: j₀ + x − j₀ = x: `Nat.add_sub_cancel_left : n + m - n = m` ✓. Then the cast: ((i+1:ℕ):ℝ)⁻¹ = 1/(i+1): one_div... Then ∑ i ∈ range (m−j₀−1), 1/(i+1) ≤ 1 + log(m−j₀−1) ≤ 1 + log m (sum_one_div_le_one_add_log + Real.log_le_log (mono m−j₀−1 ≤ m)).\n  Hmm wait — sum_one_div_le_one_add_log N : ∑_{range N} 1/(↑n+1) ≤ 1 + log N — my reindexed form ∑ 1/(i+1) = same ✓ but with ((i+1:ℕ):ℝ)⁻¹ vs 1/((i:ℝ)+1): one_div + Nat.cast_add_one bridges ✓ (simp [one_div, Nat.cast_add_one]).\n- Left side range j₀ (= Ico 0 j₀): the LAST term j₀−1 (if j₀ ≥ 1): ≤ 1/c; the rest j ≤ j₀−2: |re(w+j)| = −(w.re + j) ≥ (j₀−1−j : ℝ): term ≤ 1/(j₀−1−j)... reindex similarly: ∑_{j < j₀−1} ≤ H. If j₀ = 0: left side empty ✓ (range 0).\n  For j ≤ j₀−2 (i.e., j < j₀−1): |re(w+↑j)| = −(w.re+j): re w + j < 0 (since j ≤ j₀−2 < j₀ = ⌈−re w⌉₊ ⟹ j < −re w·... hmm: j₀−1 < −re w (from j₀−1 < j₀ = ⌈−re w⌉₊ ≤ ... wait: ⌈−re w⌉₊ = j₀ ⟹ j₀ − 1 < −re w (Nat.ceil: j₀ − 1 < −re w ⟺ j₀ < −re w + 1 ⟺ ⌈−re w⌉₊ < −re w + 1: Nat.ceil_lt_add_one (needs 0 ≤ −re w — if −re w < 0 then j₀ = 0 and the left side is empty ✓ handle j₀ = 0 separately or note ⌈x⌉₊ < x+1 needs 0 ≤ x). So for re w < 0: j₀ ≥ ... j₀−1 < −re w: then for j ≤ j₀−1: re w + j ≤ re w + j₀ − 1 < 0 ✓. And |re(w+j)| = −(re w + j) ≥ −(re w + j₀−1) + (j₀−1−j) ≥ j₀−1−j... the first part −(re w + j₀−1) ∈ [0, 1): ≥ 0. So |re(w+j)| ≥ j₀−1−j ≥ 1 for j ≤ j₀−2 ✓.\n  Left side: term_{j₀−1} ≤ 1/c; Σ_{j=0}^{j₀−2} 1/(j₀−1−j) = H_{j₀−1} ≤ 1 + log(j₀−1) ≤ 1 + log m. So left ≤ 1/c + 1 + log m.\n- Total: ≤ (1/c + 1 + log m) + (1/c + 1 + log m) = 2/c + 2 + 2 log m ✓.\n\nThe reindexing and case splits in Lean... this is ~130 lines of fiddly finset manipulation. Let me think about whether there's a SHORTER Lean path for (C). \n\nAlternative: avoid the V-split by a two-sided monotone argument: for j ∈ range m: 1/‖w+j‖ ≤ 1/max(|re w + j|, c)... hmm. OR — map to the ℤ-line: the function j ↦ re(w+j) = re w + j: the values hit each unit interval at most... \n\nActually — here's a cleaner formulation avoiding the V-split: use the SYMMETRIC majorant: for j ∈ range m: ‖(w+j)⁻¹‖ ≤ g(j) where g(j) := 1/|re w + j| if |re w + j| ≥ 1, else 1/c. The set {j : |re w + j| < 1} has ≤ 2 members (the AP with diff 1 hits (−1,1) at most twice — actually at most ⌈2/1⌉ = 2). For the others: |re w + j| ≥ 1: 1/|re w + j| ≤ 1/⌊|re w + j|⌋... the floor-bin injection: at most 2 j's per bin [i, i+1) (i ≥ 1)... — the counting bound. Lean-wise the bin-counting is MORE painful than the V-split. Stick with the V-split.\n\nHmm — actually, simplest Lean encoding of the V-split I can manage: prove the two one-sided estimates as separate haves with the Ico reindexing, each ~35 lines. Plus the first/last term handling. Let me just write it.\n\nActually — WAIT. Simpler idea for the whole (C): use the EM-free DIRECT comparison with the harmonic sum via SORTING... no. Or: Σ_{j<m} 1/‖w+j‖ ≤ Σ_{j<m} 1/max(|re(w+j)|, c) ≤ ... pair the left/right sides by the map j ↦ ... hmm. The V-split is fine. Let me write it.\n\nActually, let me simplify the reindex pain: bound each side's sum by an INTEGRAL-free telescoping... no — the harmonic bound is already available (harmonic_le_one_add_log). The reindexing: ∑ j ∈ Ico (j₀+1) m, ((j:ℝ) − j₀)⁻¹ — work with the REAL-valued shift directly: ((j:ℝ) − j₀) = (j − j₀ : ℕ cast) for j ≥ j₀... Let me define the summand as ((j:ℝ) − (j₀:ℝ))⁻¹ and reindex: Finset.sum_Ico_eq_sum_range : ∑ i ∈ Ico a b, f i = ∑ i ∈ range (b−a), f (a+i): with f j := ((j:ℝ) − j₀)⁻¹: f (j₀+1+i) = ((j₀+1+i:ℝ) − j₀)⁻¹ = ((i:ℝ) + 1)⁻¹ (push_cast; ring_nf: (j₀+1+i : ℕ cast) − j₀ = i + 1 ✓). So the reindexed sum = ∑ i ∈ range (m−j₀−1), ((i:ℝ)+1)⁻¹ ≤ 1 + log(m−j₀−1) — via the harmonic bound in the ⁻¹ form (hS'-style: simpa [one_div]) and log-mono: log(m−j₀−1) ≤ log m (Real.log_le_log (0 < ...) (m−j₀−1 ≤ m): need m−j₀−1 ≥ 1 for the log domain... if m−j₀−1 = 0 the sum is empty = 0 ≤ anything ✓ handle the empty case: if m − (j₀+1) = 0 then the Ico is empty (sum = 0) ✓ via Finset.range... hmm the reindex sum range (m−j₀−1) with m−j₀−1 = 0: range 0 = empty: sum = 0 ≤ 1+c·... fine: the bound 1 + log(m−j₀−1) = 1 + log 0 = 1 + 0 = 1 (log 0 = 0 junk) ✓ still ≥ 0 ✓. And log(m−j₀−1) ≤ log m: Real.log_le_log needs 0 < m−j₀−1 — fails if 0! Handle: by_cases on m ≤ j₀ (then Ico empty: sum = 0 ≤ ...) else the mono. Let me structure with by_cases (m ≤ j₀ + 1): if so Ico (j₀+1) m is empty (Finset.Ico_eq_empty_iff: b ≤ a ⟹ empty: m ≤ j₀+1 ✓): sum = 0. Else 0 < m−j₀−1 and the mono chain works.\n\nOK — let me just write §3 carefully. Given the accumulating session length, and that §3+§4+§5 remain (~350 lines with iterations), let me write §3 now, compile, then assess whether to continue to §4/§5 or close the session at a green boundary with §1+§2+§3 (committing (T)+(B)+(C)) and push (A)+(G) to session 028. Given the pacing rule (sub-stages end clean), that's sensible. Actually — the commit boundaries so far: 5e-i is committed (e28eff6). §1+§2 (T)+(B) are uncommitted. Let me get §3 (C) in, then commit (T)+(B)+(C) as the 5e-ii-first-half, then (A)+(G) as the second half (possibly next session if this runs long).","signature":""},{"type":"text","text":"§1+§2 green (telescope + bound B). Now §3 — the separated reciprocal sum (C)."},{"type":"tool_use","id":"Edit_389","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigammaLeft.lean","old_string":"          have h3 : Real.log (‖w‖ + 1) ≤ Real.log (2 + ‖w‖) :=\n            Real.log_le_log (by positivity) (by linarith)\n          have hlognonneg : (0 : ℝ) ≤ Real.log (2 + ‖w‖) :=\n            Real.log_nonneg (by linarith [hw_norm_ge])\n          nlinarith [h2, h3, hlog4, hlognonneg]","new_string":"          have h3 : Real.log (‖w‖ + 1) ≤ Real.log (2 + ‖w‖) :=\n            Real.log_le_log (by positivity) (by linarith)\n          have hlognonneg : (0 : ℝ) ≤ Real.log (2 + ‖w‖) :=\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₀ = ⌈−re w⌉₊ and j > j₀,\n‖(w+j)⁻¹‖ ≤ 1/(j−j₀) (real parts are 1-separated and j₀ catches up to\n−re w). -/\ntheorem recip_norm_le_right {w : ℂ} {c : ℝ} (hdist : ∀ m : ℕ, c ≤ ‖w + (m : ℂ)‖)\n    {j₀ : ℕ} (hj₀ : j₀ = ⌈-w.re⌉₊) {j : ℕ} (hj : j₀ + 1 ≤ j) :\n    ‖(w + (j : ℂ))⁻¹‖ ≤ ((j - j₀ : ℕ) : ℝ)⁻¹ := by\n  have hj₀ge : -(w.re) ≤ (j₀ : ℝ) := by rw [hj₀]; exact Nat.le_ceil _\n  have hrewj : (w + (j : ℂ)).re = w.re + (j : ℝ) := by\n    simp [Complex.add_re, Complex.natCast_re]\n  have hnorm : ‖(w + (j : ℂ))⁻¹‖ = ‖w + (j : ℂ)‖⁻¹ := norm_inv\n  rw [hnorm]\n  have hge : ((j - j₀ : ℕ) : ℝ) ≤ ‖w + (j : ℂ)‖ := by\n    have h1 : (w + (j : ℂ)).re ≤ ‖w + (j : ℂ)‖ := by\n      have h2 := Complex.abs_re_le_norm (w + (j : ℂ))\n      rwa [abs_of_nonneg (by\n        rw [hrewj]\n        have h3 : (0 : ℝ) ≤ w.re + (j₀ : ℝ) := by linarith [hj₀ge]\n        have h4 : ((j₀ : ℝ) + 1) ≤ (j : ℝ) := by exact_mod_cast hj\n        linarith [h3, h4])] at h2\n    refine le_trans ?_ h1\n    rw [hrewj]\n    have h3 : (0 : ℝ) ≤ w.re + (j₀ : ℝ) := by linarith [hj₀ge]\n    have h4 : ((j - j₀ : ℕ) : ℝ) = (j : ℝ) - (j₀ : ℝ) := by\n      rw [Nat.cast_sub (by omega : j₀ ≤ j)]\n    rw [h4]\n    linarith [h3]\n  have hpos : (0 : ℝ) < ((j - j₀ : ℕ) : ℝ) := by\n    have h1 : (1 : ℕ) ≤ j - j₀ := by omega\n    have h2 : (0 : ℝ) < ((j - j₀ : ℕ) : ℝ) := by exact_mod_cast h1\n    exact h2\n  exact (inv_le_inv₀ (by linarith [hge, hpos]) hpos).mpr hge\n\n/-- The left half: for j < j₀ − 1 (so j₀ ≥ 2 and the real part is still\nnegative), ‖(w+j)⁻¹‖ ≤ 1/(j₀−1−j). -/\ntheorem recip_norm_le_left {w : ℂ} {c : ℝ} (hdist : ∀ m : ℕ, c ≤ ‖w + (m : ℂ)‖)\n    {j₀ : ℕ} (hj₀ : j₀ = ⌈-w.re⌉₊) {j : ℕ} (hj : j + 1 ≤ j₀ - 1) :\n    ‖(w + (j : ℂ))⁻¹‖ ≤ ((j₀ - 1 - j : ℕ) : ℝ)⁻¹ := by\n  have hj₀lt : (j₀ : ℝ) < -w.re + 1 := by\n    rw [hj₀]\n    by_cases hre : 0 ≤ -w.re\n    · have h := Nat.ceil_lt_add_one hre\n      have h2 : ((⌈-w.re⌉₊ : ℕ) : ℝ) < -w.re + 1 := by exact_mod_cast h\n      exact h2\n    · push Not at hre\n      have h1 : ⌈-w.re⌉₊ = 0 := by\n        apply Nat.ceil_eq_zero.mpr\n        linarith [hre]\n      rw [h1] at hj₀\n      -- j₀ = 0 but j + 1 ≤ j₀ − 1 = 0 − 1 = 0 in ℕ: impossible\n      omega\n  have hrewj : (w + (j : ℂ)).re = w.re + (j : ℝ) := by\n    simp [Complex.add_re, Complex.natCast_re]\n  have hneg : (w + (j : ℂ)).re < 0 := by\n    rw [hrewj]\n    have h4 : ((j : ℝ) + 1) ≤ (j₀ : ℝ) - 1 := by exact_mod_cast hj\n    linarith [hj₀lt, h4]\n  have hnorm : ‖(w + (j : ℂ))⁻¹‖ = ‖w + (j : ℂ)‖⁻¹ := norm_inv\n  rw [hnorm]\n  have hge : ((j₀ - 1 - j : ℕ) : ℝ) ≤ ‖w + (j : ℂ)‖ := by\n    have h1 : |(w + (j : ℂ)).re| ≤ ‖w + (j : ℂ)‖ := Complex.abs_re_le_norm _\n    rw [hrewj] at h1\n    have h2 : |(w.re + (j : ℝ))| = -(w.re + (j : ℝ)) := abs_of_neg (by rwa [← hrewj])\n    rw [h2] at h1\n    refine le_trans ?_ h1\n    have h4 : ((j₀ - 1 - j : ℕ) : ℝ) = (j₀ : ℝ) - 1 - (j : ℝ) := by\n      rw [Nat.cast_sub (by omega : j ≤ j₀ - 1), Nat.cast_sub (by omega : 1 ≤ j₀)]\n      push_cast\n      ring\n    rw [h4]\n    linarith [hj₀lt]\n  have hpos : (0 : ℝ) < ((j₀ - 1 - j : ℕ) : ℝ) := by\n    have h1 : (1 : ℕ) ≤ j₀ - 1 - j := by omega\n    exact_mod_cast h1\n  exact (inv_le_inv₀ (by linarith [hge, hpos]) hpos).mpr hge\n\n/-- **The separated reciprocal sum bound (C)**: for dist(w, −ℕ) ≥ c > 0,\nΣ_{j<m} ‖(w+j)⁻¹‖ ≤ 2/c + 2 + 2·log 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 : ℝ} (hc : 0 < c) {w : ℂ}\n    (hdist : ∀ m : ℕ, c ≤ ‖w + (m : ℂ)‖) {m : ℕ} (hm : ⌈-w.re⌉₊ + 1 ≤ m) :\n    ∑ j ∈ Finset.range m, ‖(w + (j : ℂ))⁻¹‖ ≤ 2 / c + 2 + 2 * Real.log m := by\n  set j₀ := ⌈-w.re⌉₊ with hj₀\n  have hj₀m : j₀ ≤ m := by omega\n  -- split range m = range j₀ ∪ Ico j₀ m\n  have hsplit : ∑ j ∈ Finset.range m, ‖(w + (j : ℂ))⁻¹‖\n      = ∑ j ∈ Finset.range j₀, ‖(w + (j : ℂ))⁻¹‖\n        + ∑ j ∈ Finset.Ico j₀ m, ‖(w + (j : ℂ))⁻¹‖ := by\n    rw [Finset.range_eq_Ico, Finset.range_eq_Ico,\n      ← Finset.sum_Ico_consecutive _ (Nat.zero_le j₀) hj₀m]\n  rw [hsplit]\n  -- RIGHT side: Ico j₀ m — the first term by dist, the rest by recip_norm_le_right\n  have hright : ∑ j ∈ Finset.Ico j₀ m, ‖(w + (j : ℂ))⁻¹‖\n      ≤ 1 / c + (1 + Real.log m) := by\n    by_cases hj₀1 : j₀ + 1 ≤ m\n    · -- Ico j₀ m = {j₀} ∪ Ico (j₀+1) m\n      have hdecomp : Finset.Ico j₀ m = {j₀} ∪ Finset.Ico (j₀ + 1) m := by\n        rw [Finset.Ico_union_Ico_eq_Ico (Nat.le_refl j₀) hj₀1]\n        exact (Finset.Ico_self_singleton).symm... \n```\nHmm — Ico j₀ (j₀+1) = {j₀}: `Finset.Ico_self_singleton`? the name... `Finset.Ico_succ_singleton : Ico n (n+1) = {n}` ✓ I believe. Then the union: Ico j₀ (j₀+1) ∪ Ico (j₀+1) m = Ico j₀ m via Finset.Ico_union_Ico_eq_Ico (le_refl) hj₀1 ✓. So Ico j₀ m = {j₀} ∪ Ico (j₀+1) m via rw [← Finset.Ico_succ_singleton... wait I need Ico j₀ m = {j₀} ∪ ...: {j₀} = Ico j₀ (j₀+1) via Ico_succ_singleton.symm; then Ico j₀ (j₀+1) ∪ Ico (j₀+1) m = Ico j₀ m via the union lemma. So:\n```\n      have hdecomp : Finset.Ico j₀ m = Finset.Ico j₀ (j₀ + 1) ∪ Finset.Ico (j₀ + 1) m :=\n        (Finset.Ico_union_Ico_eq_Ico (Nat.le_refl j₀) hj₀1).symm\n      rw [hdecomp, Finset.Ico_succ_singleton]  -- hmm Ico j₀ (j₀+1) = {j₀}: Finset.Ico_succ_singleton : Ico n (n+1) = {n} — rw turns it into {j₀}: then sum over {j₀} ∪ ...: Finset.sum_union (disjoint) — the disjointness: {j₀} ∩ Ico (j₀+1) m = ∅: Finset.disjoint_singleton_left: j₀ ∉ Ico (j₀+1) m: Finset.not_mem_Ico: j₀ < j₀+1 ≤ ... hmm `Finset.Ico_disjoint_Ico_consecutive`? there's `Finset.Ico_disjoint_Ico_consecutive (a b c) : Disjoint (Ico a b) (Ico b c)` ✓ I recall. So:\n      rw [hdecomp, Finset.Ico_succ_singleton,\n        Finset.sum_union (Finset.disjoint_singleton_left.mpr (by\n          simp [Finset.mem_Ico] : j₀ ∉ Finset.Ico (j₀+1) m)),  -- hmm the disjoint_singleton_left form\n        Finset.sum_singleton]\n```\nThis is getting heavy. SIMPLER alternative: use `Finset.sum_Ico_succ_top`? no that's the top. For the BOTTOM: `Finset.sum_Ico_eq_sum_range` reindex the whole Ico (j₀+1) m part and handle the j₀ term separately via... actually cleanest: DON'T peel the first term; instead bound the FIRST term inline via a case split in the sum: \n\nAlternative cleaner structure: bound ∑ Ico j₀ m directly:\n∑ j ∈ Ico j₀ m, term_j = term_{j₀} + ∑_{j ∈ Ico (j₀+1) m} term_j — the peeling: `Finset.sum_Ico_succ_top`? no. There IS `Finset.sum_Ico_eq_sub`? no. The bottom-peel: `Finset.Ico.erase`... Or use: `Finset.sum_Ico_succ_bot`? hmm — sum over Ico (a) b with a < b = f a + ∑ Ico (a+1) b: the lemma name might be `Finset.sum_Ico_eq_head_add_sum_tail`? not a thing. There IS: `Finset.sum_range_succ` and for Ico: `Finset.sum_Ico_eq_sum_range` + `Finset.sum_range_succ'`? Let me just do the reindex for the whole right side INCLUDING j₀'s term with a per-term piecewise bound:\n\nFor j ∈ Ico j₀ m: term_j ≤ h j where h j := if j = j₀ then 1/c else ((j − j₀ : ℕ):ℝ)⁻¹. Then ∑ = (peel j₀) ... still needs the peel. \n\nOK — the cleanest available: `Finset.sum_eq_sum_diff_singleton_add`? or `Finset.add_sum_erase`: ∑_{Ico j₀ m} f = f j₀ + ∑_{(Ico j₀ m).erase j₀} f — and (Ico j₀ m).erase j₀ = Ico (j₀+1) m: `Finset.Ico_erase_left : (Ico a b).erase a = Ico (a+1) b` ✓ I believe that exists. So:\n```\n      rw [← Finset.add_sum_erase _ _ (Finset.left_mem_Ico.mpr (by omega : j₀ < m))]  -- hmm add_sum_erase : f a + ∑ x ∈ s.erase a, f x = ∑ x ∈ s, f x for a ∈ s — so ← direction turns the sum into f j₀ + erase-sum ✓\n      rw [Finset.Ico_erase_left]  -- (Ico j₀ m).erase j₀ = Ico (j₀+1) m\n```\nFinset.left_mem_Ico : a ∈ Ico a b ↔ a < b ✓ (I think). Then:\n```\n      -- term at j₀: ≤ 1/c\n      have hfirst : ‖(w + (j₀ : ℂ))⁻¹‖ ≤ 1 / c := by\n        rw [norm_inv]\n        rw [show (1 : ℝ) / c = (c : ℝ)⁻¹ by rw [one_div]]\n        exact (inv_le_inv₀ hc (hdist j₀)).mpr (hdist j₀)  -- hmm inv_le_inv₀ (ha : 0 < a) (hb : 0 < b) : a⁻¹ ≤ b⁻¹ ↔ b ≤ a: ‖w+j₀‖⁻¹ ≤ c⁻¹ ⟺ c ≤ ‖w+j₀‖: (inv_le_inv₀ (by linarith [hdist j₀, hc] : (0:ℝ) < ‖w+j₀‖) hc).mpr (hdist j₀) ✓\n      -- the rest: reindex to the harmonic bound\n      have hrest : ∑ j ∈ Finset.Ico (j₀ + 1) m, ‖(w + (j : ℂ))⁻¹‖ ≤ 1 + Real.log m := by\n        calc ∑ j ∈ Finset.Ico (j₀ + 1) m, ‖(w + (j : ℂ))⁻¹‖\n            ≤ ∑ j ∈ Finset.Ico (j₀ + 1) m, ((j - j₀ : ℕ) : ℝ)⁻¹ :=\n              Finset.sum_le_sum fun j hj => recip_norm_le_right hdist hj₀ (by\n                rw [Finset.mem_Ico] at hj; exact hj.1)\n          _ = ∑ i ∈ Finset.range (m - (j₀ + 1)), ((i : ℝ) + 1)⁻¹ := by\n              rw [Finset.sum_Ico_eq_sum_range]  -- ∑ i ∈ range ((j₀+1) ... hmm: sum_Ico_eq_sum_range : ∑ i ∈ Ico a b, f i = ∑ i ∈ range (b − a), f (a + i): with a := j₀+1, b := m: ∑ i ∈ range (m − (j₀+1)), f (j₀+1+i): f (j₀+1+i) = (((j₀+1+i) − j₀ : ℕ):ℝ)⁻¹: (j₀+1+i) − j₀ = i+1: \n              apply Finset.sum_congr rfl\n              intro i _\n              -- ((j₀+1+i) − j₀ : ℕ) = i + 1\n              have h1 : (j₀ + 1 + i) - j₀ = i + 1 := by omega\n              rw [h1]  -- then casts: ((i+1 : ℕ):ℝ) = (i:ℝ)+1: Nat.cast_add_one\n              rw [Nat.cast_add_one]\n          _ ≤ 1 + Real.log (m - (j₀ + 1)) := by\n              have h := sum_one_div_le_one_add_log (m - (j₀ + 1))\n              -- h's form: ∑ 1/(↑n+1) ≤ 1 + log ↑(m−j₀−1): my form: ∑ (↑i+1)⁻¹: simpa [one_div]\n              simpa [one_div] using h\n          _ ≤ 1 + Real.log m := by\n              gcongr  -- 1 + log(m−j₀−1) ≤ 1 + log m: log mono: Real.log_le_log (0 < m−j₀−1) (m−j₀−1 ≤ m): the 0 < fails if m = j₀+1 — but then the range is empty... hmm the sum range (m−(j₀+1)) with m = j₀+1: range 0: sum = 0: and 0 ≤ 1 + log m ✓ (log m ≥ 0 for m ≥ 1: m ≥ j₀+1 ≥ 1 ✓... wait m ≥ 1: from hm : j₀+1 ≤ m and j₀ ≥ 0: m ≥ 1 ✓). The gcongr needs 0 < ↑(m−j₀−1) — fails when m = j₀+1 (then m−j₀−1 = 0: log 0 = 0 junk: the step (1 + log 0) = 1 + 0 = 1 ≤ 1 + log m ⟺ 0 ≤ log m ✓ m ≥ 1). Split: by_cases m = j₀+1: then the sum is over range 0 = 0: 0 ≤ 1 + log m ✓. Else: 1 ≤ m−j₀−1: log mono ✓. Let me write:\n              by_cases hcase : m - (j₀ + 1) = 0\n              · have : m - (j₀ + 1) = 0 := hcase\n                -- the sum ∑ i ∈ range 0 = 0 — but we're at the SECOND calc step's goal: (1 + log ↑(m−j₀−1)) ≤ 1 + log ↑m: with ↑(m−j₀−1) = 0: log 0 = 0: \n                rw [hcase]  -- ↑(0:ℕ) = 0: Nat.cast_zero: log 0 = 0: Real.log_zero\n                simp [Real.log_zero]  -- 1 + 0 ≤ 1 + log ↑m ⟺ 0 ≤ log ↑m: Real.log_nonneg (1 ≤ ↑m): m ≥ 1 ✓\n                exact Real.log_nonneg (by exact_mod_cast (by omega : 1 ≤ m))\n              · have h1 : (1 : ℕ) ≤ m - (j₀ + 1) := by omega\n                have h2 : (0 : ℝ) < ((m - (j₀ + 1) : ℕ) : ℝ) := by exact_mod_cast h1\n                have h3 : ((m - (j₀ + 1) : ℕ) : ℝ) ≤ (m : ℝ) := by\n                  rw [Nat.cast_sub (by omega : j₀ + 1 ≤ m)]\n                  push_cast\n                  have h4 : (0 : ℝ) ≤ (j₀ : ℝ) := by positivity\n                  linarith [h4]\n                have h4 : Real.log ((m - (j₀ + 1) : ℕ) : ℝ) ≤ Real.log (m : ℝ) :=\n                  Real.log_le_log h2 h3\n                linarith [h4]\n      -- combine\n      calc ∑ j ∈ Finset.Ico j₀ m, ‖(w + (j : ℂ))⁻¹‖\n          = ‖(w + (j₀ : ℂ))⁻¹‖ + ∑ j ∈ Finset.Ico (j₀ + 1) m, ‖(w + (j : ℂ))⁻¹‖ := by\n            rw [Finset.add_sum_erase _ _ (Finset.left_mem_Ico.mpr (by omega : j₀ < m)),\n              Finset.Ico_erase_left]\n        _ ≤ 1 / c + (1 + Real.log m) := add_le_add hfirst hrest\n    · -- ¬(j₀+1 ≤ m) ⟹ m ≤ j₀: the Ico is empty\n      push Not at hj₀1\n      have hempty : Finset.Ico j₀ m = ∅ := Finset.Ico_eq_empty_of_le (by omega : m ≤ j₀)  -- Finset.Ico_eq_empty_of_le (h : b ≤ a) : Ico a b = ∅? check name — maybe `Finset.Ico_eq_empty_iff : Ico a b = ∅ ↔ b ≤ a` — use .mpr\n      rw [hempty]\n      simp  -- ∑ ∅ = 0 ≤ 1/c + (1 + log m): positivity... needs 1/c > 0 and log m ≥ 0: m ≥ j₀+1−... hmm here m ≤ j₀: log m could be log 0 = 0 (m = 0) or log of small — m ≤ j₀ but from hm : j₀+1 ≤ m?? — WAIT hm : j₀ + 1 ≤ m is the THEOREM's hypothesis — and the by_cases hj₀1 : j₀+1 ≤ m is ALWAYS true by hm!! So the else branch is vacuous: hj₀1 contradicts hm: omega closes:\n      omega  -- hm : j₀ + 1 ≤ m and hj₀1 : ¬(j₀+1 ≤ m) — False ⟹ anything\n```\nWait — hm : ⌈−w.re⌉₊ + 1 ≤ m i.e. j₀ + 1 ≤ m — so the by_cases's second branch is vacuous ✓ just `omega` (deriving False from hm and hj₀1). Hmm — but the goal in that branch after `push Not at hj₀1`: hj₀1 : ¬ j₀ + 1 ≤ m; hm : j₀ + 1 ≤ m: `exact absurd hm hj₀1` closes any goal ✓ cleaner: `exact absurd hm hj₀1`. So drop the by_cases entirely — just use hj₀1 := hm. Simplify: the right side always has j₀+1 ≤ m ✓ no by_cases needed!\n\nSimilarly the LEFT side: range j₀: if j₀ = 0: empty ✓ handle via by_cases (j₀ = 0); else peel j₀−1 from the TOP: range j₀ = range (j₀−1) ∪ {j₀−1}... via Finset.sum_range_succ with j₀ = (j₀−1)+1: ∑ range j₀ f = ∑ range (j₀−1) f + f (j₀−1) (with j₀−1+1 = j₀ by omega-rewrite). The f (j₀−1) term ≤ 1/c (dist). The range (j₀−1) part: j ≤ j₀−2 ⟹ recip_norm_le_left (hj : j + 1 ≤ j₀ − 1): reindex: ∑ j ∈ range (j₀−1), ((j₀−1−j : ℕ):ℝ)⁻¹ = ∑ i ∈ range (j₀−1), ((i:ℝ)+1)⁻¹ (reverse the range! j ↦ j₀−1−j is an order-reversing bijection on range (j₀−1) — `Finset.sum_range_reflect`?? there IS `Finset.sum_range_reflect (f) (n) : ∑ i ∈ range n, f (n − 1 − i) = ∑ i ∈ range n, f i` ✓ I recall!). So ∑ j ∈ range (j₀−1), g (j₀−1−j) = ∑ j ∈ range (j₀−1), g j with g j := ((j+1 : ℕ):ℝ)⁻¹?? hmm: my term after recip_norm_le_left: ((j₀−1−j : ℕ):ℝ)⁻¹: let g x := ((x:ℕ):ℝ)⁻¹: the term is g (j₀−1−j) with... j₀−1−j for j ∈ range (j₀−1): j₀−1−j ∈ {j₀−1, j₀−2, ..., 1}: sum_range_reflect: ∑ j ∈ range (j₀−1), g (j₀−1−j) = ∑ j ∈ range (j₀−1), g j?? — sum_range_reflect : ∑ i ∈ range n, f (n − 1 − i) = ∑ i ∈ range n, f i: with n := j₀−1: f (n−1−i) = f (j₀−1−i)... my term: ((j₀−1−j:ℕ):ℝ)⁻¹ = f (j₀−1−j) with f x := ((x:ℕ):ℝ)⁻¹: but sum_range_reflect needs f (n − 1 − i) = f ((j₀−1) − 1 − j) = f (j₀−2−j) — OFF BY ONE from my j₀−1−j. Hmm: (j₀−1) − 1 − j = j₀−2−j ≠ j₀−1−j. So reflect on range j₀ instead? Let me reindex differently: ∑ j ∈ range (j₀−1), f (j₀−1−j) = ∑ i ∈ range (j₀−1), f (i+1)?? the values {j₀−1−j : j < j₀−1} = {1, 2, ..., j₀−1} = {i+1 : i < j₀−1} ✓: via the reflect at range j₀: ∑ j ∈ range j₀, g j = ∑ j ∈ range j₀, g (j₀−1−j) (sum_range_reflect (g) j₀: ∑_{range j₀} g (j₀−1−j) = ∑_{range j₀} g): so ∑ j ∈ range (j₀−1), f (j₀−1−j) — the j ranges over range (j₀−1) = {0..j₀−2}: the values j₀−1−j range over {1..j₀−1} = {i+1 : i ∈ range (j₀−1)}: so ∑ j ∈ range (j₀−1), f (j₀−1−j) = ∑ i ∈ range (j₀−1), f (i+1): via... define g on range j₀ with g 0 = 0-ish: ∑_{range j₀} g (j₀−1−j) = ∑_{range j₀} g j (reflect): the LHS = g (j₀−1) + g(j₀−2) + ... + g(0)... my sum is over j ≤ j₀−2 of f(j₀−1−j) = f(1) + f(2) + ... + f(j₀−1) — i.e., ∑_{i ∈ range (j₀−1)} f (i+1). To get there: ∑_{j ∈ range (j₀−1)} f (j₀−1−j): substitute i := j₀−1−j... simplest Lean route: `Finset.sum_range_reflect (fun x => ((x + 1 : ℕ):ℝ)⁻¹)?`... hmm: consider g j := ((j+1:ℕ):ℝ)⁻¹ for j ∈ range (j₀−1)... I want to show ∑_{j < j₀−1} ((j₀−1−j:ℕ):ℝ)⁻¹ = ∑_{i < j₀−1} ((i+1:ℕ):ℝ)⁻¹. Take f x := ((x:ℕ):ℝ)⁻¹ on range j₀: sum_range_reflect f j₀ : ∑_{j ∈ range j₀} f (j₀−1−j) = ∑_{j ∈ range j₀} f j. The LHS: j ∈ range j₀ = {0..j₀−1}: terms f (j₀−1−j) for j=0..j₀−1: = f(j₀−1), f(j₀−2), ..., f(0) — that includes f(0) = 0⁻¹ = 0 (junk but fine) — and f(1)...f(j₀−1). So ∑_{range j₀} f (j₀−1−j) = (my target sum) + f(0)·... my target: ∑_{j ∈ range (j₀−1)} f (j₀−1−j): the j = j₀−1 term of the reflect LHS would be f(0) = 0: so ∑_{range j₀} f(j₀−1−j) = ∑_{range (j₀−1)} f(j₀−1−j) + f(0)... hmm j = j₀−1: f (j₀−1−(j₀−1)) = f 0 = 0⁻¹ = 0: so the reflect-LHS = my-sum + 0: ∑_{range j₀} f(j₀−1−j) = ∑_{range (j₀−1)} f(j₀−1−j) + f 0 via sum_range_succ (range j₀ = range (j₀−1) + the j₀−1 term): so my sum = ∑_{range j₀} f (j₀−1−j) − f 0 = (∑_{range j₀} f j) − 0 [reflect] = ∑_{range j₀} f j = ∑_{range (j₀−1)} f j + f (j₀−1) [sum_range_succ]... I'm tying myself in knots. DIRECT: my sum = ∑_{j ∈ range (j₀−1)} f (j₀−1−j). Use Finset.sum_bij with the involution j ↦ j₀−2−j on range (j₀−1)? maps j ∈ {0..j₀−2} to j₀−2−j ∈ {0..j₀−2} ✓ involution: then ∑ f (j₀−1−j) = ∑_{i} f (j₀−1−(j₀−2−i)) = ∑ f (i+1): j₀−1−(j₀−2−i) = i+1 ✓ (omega). Finset.sum_bij (i : j ↦ j₀−2−j) (hi : maps into) (hi_inj) (hi_surj) (h : ∀ j, f (j₀−1−j) = f' j)?? the signature of sum_bij is heavy. Use `Finset.sum_nbij'`? or simplest: `Finset.sum_range_reflect`-based... \n\nActually — cleanest: reindex via sum_Ico_eq_sum_range-style but for the reverse: `Finset.sum_range_reflect (f : ℕ → M) (n : ℕ) : ∑ i ∈ range n, f (n − 1 − i) = ∑ i ∈ range n, f i` — apply with f x := ((x + 1 : ℕ):ℝ)⁻¹ and n := j₀ − 1: LHS: ∑ i ∈ range (j₀−1), f (j₀−1−1−i) = ∑ f (j₀−2−i) — values f (j₀−2−i) for i < j₀−1: {j₀−2, ..., 0} → f values {((j₀−2)+1)⁻¹...} hmm this gives f(j₀−2−i) with f x = (x+1)⁻¹: = (j₀−1−i)⁻¹ — YES: f (j₀−2−i) = ((j₀−2−i)+1)⁻¹ = ((j₀−1−i):ℕ)⁻¹ ✓ EXACTLY my term! So:\n∑ i ∈ range (j₀−1), ((j₀−1−i:ℕ):ℝ)⁻¹ = ∑ i ∈ range (j₀−1), f (j₀−2−i) [per-term defeq: ((j₀−1−i):ℕ)⁻¹ = ((j₀−2−i:ℕ)+1:ℕ...)⁻¹: j₀−1−i = (j₀−2−i)+1 by omega (for i ≤ j₀−2 ✓)] = ∑ i ∈ range (j₀−1), f i [sum_range_reflect] = ∑ i ∈ range (j₀−1), ((i:ℕ)+1:ℕ→ℝ)⁻¹ ≤ 1 + log(j₀−1) [harmonic bound] ≤ 1 + log m.\n\nOK. The Lean plumbing remains fiddly but doable. Time check: this §3 is long. Let me just write the full §3 now as an append, carefully, and compile. I'll write the two one-sided bounds as separate haves with all the reindexing inline."},"extra_content":null}]