← Session 27 — ii′-5c/5d: Davenport disc + FE-reflection bounds
thinking (10788 chars)
The damage: §3's `digamma_recip_sum_le` theorem is incomplete (cuts off at line 577 mid-proof with `(Finset.Ico_self_singleton).symm...` and then all my planning text through line 664, then the end markers at 667/669). The helpers recip_norm_le_right (line 483) and recip_norm_le_left (line 514) are complete (they were in the good part of my edit before the contamination). The hsplit/hright part is partial.
I need to: replace from line 570 (the "-- RIGHT side" comment) through line 664 (end of contamination) with the clean complete digamma_recip_sum_le proof, keeping `end NguyenRH1 / end`.
The clean complete proof of digamma_recip_sum_le:
```
theorem digamma_recip_sum_le {c : ℝ} (hc : 0 < c) {w : ℂ}
(hdist : ∀ m : ℕ, c ≤ ‖w + (m : ℂ)‖) {m : ℕ} (hm : ⌈-w.re⌉₊ + 1 ≤ m) :
∑ j ∈ Finset.range m, ‖(w + (j : ℂ))⁻¹‖ ≤ 2 / c + 2 + 2 * Real.log m := by
set j₀ := ⌈-w.re⌉₊ with hj₀
have hj₀m : j₀ ≤ m := by omega
have hj₀1m : j₀ + 1 ≤ m := hm
have hsplit : ... (the range split, already present at 564-568) ...
rw [hsplit]
-- harmonic in inv-form
have hHarm : ∀ K : ℕ, ∑ i ∈ Finset.range K, ((i : ℝ) + 1)⁻¹ ≤ 1 + Real.log K := by
intro K
have h := sum_one_div_le_one_add_log K
simpa [one_div] using h
have hlogmono : ∀ {a b : ℕ}, 1 ≤ a → a ≤ b → 1 + Real.log a ≤ 1 + Real.log b := by
intro a b ha hab
have h1 : (0 : ℝ) < (a : ℝ) := by exact_mod_cast ha
have h2 : (a : ℝ) ≤ (b : ℝ) := by exact_mod_cast hab
have h3 := Real.log_le_log h1 h2
linarith [h3]
-- RIGHT side
have hfirst_r : ‖(w + (j₀ : ℂ))⁻¹‖ ≤ 1 / c := by
rw [norm_inv, show (1 : ℝ) / c = c⁻¹ by rw [one_div]]
have hpos : (0 : ℝ) < ‖w + (j₀ : ℂ)‖ := lt_of_lt_of_le hc (hdist j₀)
exact (inv_le_inv₀ hpos hc).mpr (hdist j₀)
have hrest_r : ∑ j ∈ Finset.Ico (j₀ + 1) m, ‖(w + (j : ℂ))⁻¹‖ ≤ 1 + Real.log m := by
calc ∑ j ∈ Finset.Ico (j₀ + 1) m, ‖(w + (j : ℂ))⁻¹‖
≤ ∑ j ∈ Finset.Ico (j₀ + 1) m, ((j - j₀ : ℕ) : ℝ)⁻¹ :=
Finset.sum_le_sum fun j hj => recip_norm_le_right hdist hj₀ (by
rw [Finset.mem_Ico] at hj; exact hj.1)
_ = ∑ i ∈ Finset.range (m - (j₀ + 1)), ((i : ℝ) + 1)⁻¹ := by
rw [Finset.sum_Ico_eq_sum_range]
apply Finset.sum_congr rfl
intro i _
have h1 : (j₀ + 1 + i) - j₀ = i + 1 := by omega
rw [h1, Nat.cast_add_one]
_ ≤ 1 + Real.log (m - (j₀ + 1)) := hHarm _
_ ≤ 1 + Real.log m := by
by_cases hcase : m - (j₀ + 1) = 0
· rw [hcase]
simp [Real.log_zero]
exact Real.log_nonneg (by exact_mod_cast (by omega : 1 ≤ m))
· exact hlogmono (by omega) (by omega)
have hright : ∑ j ∈ Finset.Ico j₀ m, ‖(w + (j : ℂ))⁻¹‖ ≤ 1 / c + (1 + Real.log m) := by
calc ∑ j ∈ Finset.Ico j₀ m, ‖(w + (j : ℂ))⁻¹‖
= ‖(w + (j₀ : ℂ))⁻¹‖ + ∑ j ∈ Finset.Ico (j₀ + 1) m, ‖(w + (j : ℂ))⁻¹‖ := by
rw [Finset.add_sum_erase _ _ (Finset.left_mem_Ico.mpr (by omega : j₀ < m)),
Finset.Ico_erase_left]
_ ≤ 1 / c + (1 + Real.log m) := add_le_add hfirst_r hrest_r
-- LEFT side
have hleft : ∑ j ∈ Finset.range j₀, ‖(w + (j : ℂ))⁻¹‖ ≤ 1 / c + (1 + Real.log m) := by
by_cases hj₀0 : j₀ = 0
· rw [hj₀0]
simp -- range 0 sum = 0 ≤ 1/c + (1 + log m): needs 0 ≤ 1/c (hc) and 0 ≤ 1 + log m: log m ≥ 0 for m ≥ 1: m ≥ j₀+1 = 1 ✓:
have h1 : (0 : ℝ) ≤ 1 / c := by positivity
have h2 : (0 : ℝ) ≤ Real.log m := Real.log_nonneg (by exact_mod_cast (by omega : 1 ≤ m))
linarith [h1, h2]
· have hj₀1 : 1 ≤ j₀ := Nat.one_le_iff_ne_zero.mpr hj₀0
-- range j₀ = range (j₀−1) + the j₀−1 term
have hdecomp : ∑ j ∈ Finset.range j₀, ‖(w + (j : ℂ))⁻¹‖
= ∑ j ∈ Finset.range (j₀ - 1), ‖(w + (j : ℂ))⁻¹‖ + ‖(w + ((j₀ - 1 : ℕ)) : ℂ)‖⁻¹ := by
conv_lhs => rw [show j₀ = (j₀ - 1) + 1 by omega]
rw [Finset.sum_range_succ]
-- the last term ≤ 1/c
have hlast : ‖(w + ((j₀ - 1 : ℕ)) : ℂ)⁻¹‖ ≤ 1 / c := by
have hcast : ((j₀ - 1 : ℕ) : ℂ) = (j₀ : ℂ) - 1 := by
rw [Nat.cast_sub hj₀1]
push_cast
ring
-- dist at j₀−1 (a nat): hdist (j₀−1) : c ≤ ‖w + ↑(j₀−1)‖
have hpos : (0 : ℝ) < ‖w + ((j₀ - 1 : ℕ) : ℂ)‖ := lt_of_lt_of_le hc (hdist (j₀ - 1))
rw [norm_inv, show (1 : ℝ) / c = c⁻¹ by rw [one_div]]
exact (inv_le_inv₀ hpos hc).mpr (hdist (j₀ - 1))
-- the earlier terms: recip_norm_le_left + reflect reindex
have hrest_l : ∑ j ∈ Finset.range (j₀ - 1), ‖(w + (j : ℂ))⁻¹‖ ≤ 1 + Real.log m := by
calc ∑ j ∈ Finset.range (j₀ - 1), ‖(w + (j : ℂ))⁻¹‖
≤ ∑ j ∈ Finset.range (j₀ - 1), ((j₀ - 1 - j : ℕ) : ℝ)⁻¹ :=
Finset.sum_le_sum fun j hj => recip_norm_le_left hdist hj₀ (by
rw [Finset.mem_range] at hj; omega)
_ = ∑ i ∈ Finset.range (j₀ - 1), ((i : ℝ) + 1)⁻¹ := by
-- reflect: the map j ↦ j₀−1−j on range (j₀−1) hits {1,...,j₀−1}
have h1 : ∀ j ∈ Finset.range (j₀ - 1),
((j₀ - 1 - j : ℕ) : ℝ)⁻¹ = ((j₀ - 1 - j : ℕ) : ℝ)⁻¹ := fun j _ => rfl
-- use sum_range_reflect with f i := ((i+1 : ℕ):ℝ)⁻¹...
rw [Finset.sum_range_reflect (fun x : ℕ => (((x : ℕ) + 1 : ℕ) : ℝ)⁻¹) (j₀ - 1)]
-- hmm: sum_range_reflect f n : ∑ i ∈ range n, f (n − 1 − i) = ∑ i ∈ range n, f i
-- with n := j₀−1: LHS = ∑ i ∈ range (j₀−1), f (j₀−1−1−i) = ∑ f (j₀−2−i)
-- I need to first rewrite MY sum into the f (j₀−2−j) form:
...
```
Hmm — the left reindex: my sum's term after recip_norm_le_left is ((j₀−1−j : ℕ):ℝ)⁻¹ for j ∈ range (j₀−1). Target form: ((i:ℝ)+1)⁻¹ = ((i+1:ℕ):ℝ)⁻¹. The reflect gives ∑ f (n−1−i) = ∑ f i with n := j₀−1, f x := ((x+1:ℕ):ℝ)⁻¹: LHS terms f (j₀−1−1−i) = f (j₀−2−i) = ((j₀−2−i+1:ℕ):ℝ)⁻¹ = ((j₀−1−i:ℕ):ℝ)⁻¹ (omega: j₀−2−i+1 = j₀−1−i for i ≤ j₀−2 ✓... j₀−2−i+1 = j₀−1−i needs j₀ ≥ ... j₀−2−i: careful when j₀ = 1: range (j₀−1) = range 0 = empty ✓ trivial). So:
```
_ = ∑ i ∈ Finset.range (j₀ - 1), ((i : ℝ) + 1)⁻¹ := by
rw [Finset.sum_range_reflect (fun x : ℕ => (((x : ℕ) + 1 : ℕ) : ℝ)⁻¹) (j₀ - 1)]
apply Finset.sum_congr rfl
intro j hj
rw [Finset.mem_range] at hj
-- f (j₀−1−1−j) = ((j₀−1−1−j : ℕ)+1 : ℝ)⁻¹ = ((j₀−1−j : ℕ):ℝ)⁻¹ (the goal's term)
have h1 : (j₀ - 1 - 1 - j) + 1 = j₀ - 1 - j := by omega
rw [h1] -- hmm the f's cast: (((j₀−1−1−j : ℕ)+1 : ℕ):ℝ)⁻¹: the inner (x+1 : ℕ): after h1: ((j₀−1−j : ℕ):ℝ)⁻¹ — the cast chain: ((↑(j₀−1−1−j)+1 : ℕ):ℝ) — wait f x := (((x:ℕ)+1 : ℕ):ℝ)⁻¹ — the +1 is in ℕ then cast: ↑(x+1) = ↑x + 1 — my target ((i:ℝ)+1)⁻¹: ↑i + 1: matches after Nat.cast_add_one. And the LHS of the per-term congr: f (j₀−1−1−j) with x := j₀−1−1−j: ((↑(j₀−1−1−j)+1 : ℕ... hmm the +1 in f is the ℕ-addition (x+1 : ℕ): after h1 (j₀−1−1−j + 1 = j₀−1−j): the cast becomes ↑(j₀−1−j):ℝ: and the goal-side per-term is ((j₀−1−j : ℕ):ℝ)⁻¹ — MATCH... wait what's the goal at that point: after rw [sum_range_reflect ...] the goal becomes: ∑ j ∈ range (j₀−1), f (j₀−1−1−j)?? no — rw [sum_range_reflect f (j₀−1)] rewrites occurrences of ∑ i ∈ range (j₀−1), f (j₀−1−1−i)?? the lemma: sum_range_reflect f n : ∑ i ∈ range n, f (n−1−i) = ∑ i ∈ range n, f i — rw rewrites the LHS-pattern ∑_{range (j₀−1)} f (·−1−·)... my goal's LHS is ∑ ((j₀−1−j:ℕ):ℝ)⁻¹ — NOT of the form ∑ f (n−1−i) with f := fun x => ((x+1:ℕ):ℝ)⁻¹ — because f (j₀−1−j) = ((j₀−1−j)+1 : ℕ→ℝ)⁻¹ = ((j₀−j : ℕ):ℝ)⁻¹ — that's ((j₀−j))⁻¹ NOT my ((j₀−1−j))⁻¹. WRONG f. Take f x := ((x : ℕ):ℝ)⁻¹: then f (j₀−1−j) = ((j₀−1−j):ℕ→ℝ)⁻¹ ✓ MY term. reflect: ∑_{range (j₀−1)} f (j₀−1−1−j) = ∑_{range (j₀−1)} f j: the LHS pattern with n := j₀−1: f (n−1−j) = f (j₀−2−j) = ((j₀−2−j : ℕ):ℝ)⁻¹ — my LHS is ∑ f (j₀−1−j) — NOT the reflect's LHS pattern (which is f (j₀−2−j)). So rw [sum_range_reflect f (j₀−1)] rewrites ∑_{range(j₀−1)} f (j₀−2−j) — not present in my goal (I have f (j₀−1−j)) — FAIL.
Correct approach: my sum = ∑_{j ∈ range (j₀−1)} f (j₀−1−j) with f x := ((x:ℕ):ℝ)⁻¹. The reflect with n := j₀: ∑_{j ∈ range j₀} f (j₀−1−j) = ∑_{j ∈ range j₀} f j. My sum is over range (j₀−1) — one fewer. Hmm — handle via: ∑_{j ∈ range j₀} f (j₀−1−j) = [my sum over range (j₀−1)] + f (j₀−1−(j₀−1)) = my sum + f 0 = my sum + 0⁻¹ = my sum + 0 (inv_zero: 0⁻¹ = 0 — ((0:ℕ):ℝ)⁻¹ = 0⁻¹ = 0 ✓ inv_zero). So my sum = ∑_{range j₀} f (j₀−1−j) − 0 = ∑_{range j₀} f j [reflect] = ∑_{range (j₀−1)} f j + f (j₀−1) [sum_range_succ, j₀ = (j₀−1)+1]: f (j₀−1) = ((j₀−1:ℕ):ℝ)⁻¹ and ∑_{range (j₀−1)} f j = ∑_{j<j₀−1} (j:ℝ)⁻¹·... hmm the f j = (j:ℝ)⁻¹ for j = 0: 0⁻¹ = 0 ✓: so ∑_{range j₀} f j = ∑_{j=1}^{j₀−1} (j:ℝ)⁻¹ = H_{j₀−1}-ish in inv form = ∑_{i ∈ range (j₀−1)} ((i:ℝ)+1)⁻¹ [reindex j = i+1: ∑_{j ∈ range j₀, j ≥ 1} = ...] — ANOTHER reindex.
Ugh — the reflect path keeps generating off-by-one friction. Let me use a cleaner bij: `Finset.sum_nbij` or the direct: ∑_{j ∈ range (j₀−1)} f (j₀−1−j) = ∑_{i ∈ range (j₀−1)} f (i+1): via Finset.sum_bij with i := fun j _ => j₀−2−j (the involution on range (j₀−1) = {0,...,j₀−2}):
Finset.sum_bij (i : ℕ → ℕ) (hi : ∀ j ∈ s, i j ∈ t) (hi_inj : InjOn i s) (hi_surj : SurjOn i s t) (h : ∀ j ∈ s, f j = g (i j)) : ∑ s f = ∑ t g — the signature in this Mathlib: `Finset.sum_bij {ι κ} {s : Finset ι} {t : Finset κ} {f : ι → M} {g : κ → M} (i : ι → κ) (hi : ∀ a ∈ s, i a ∈ t) (i_inj : Set.InjOn i s) (i_surj : Set.SurjOn i s t) (h : ∀ a ∈ s, f a = g (i a)) : ∑ x ∈ s, f x = ∑ x ∈ t, g x` ✓ roughly. With: s = t = range (j₀−1); i j := j₀−2−j; f j := ((j₀−1−j : ℕ):ℝ)⁻¹; g i := ((i:ℝ)+1)⁻¹. Check: i j ∈ range (j₀−1) for j ∈ range (j₀−1): j ≤ j₀−2 ⟹ j₀−2−j ∈ [0, j₀−2] ✓ omega. InjOn: j₀−2−j is injective on the range (sub by constant) ✓ (omega-driven: intro a _ b _ h; omega). SurjOn: for i ∈ range (j₀−1): preimage j := j₀−2−i ∈ range ✓ and i (j₀−2−i) = j₀−2−(j₀−2−i) = i ✓ omega. The function equation: f j = g (i j): ((j₀−1−j:ℕ):ℝ)⁻¹ = ((j₀−2−j : ℝ)+1)⁻¹: j₀−1−j = (j₀−2−j)+1 as nats for j ≤ j₀−2 ✓ then cast: ↑(j₀−2−j)+1 = ↑(j₀−1−j)... : ((j₀−2−j:ℕ):ℝ)+1 = ((j₀−1−j:ℕ):ℝ): Nat.cast_sub chains... omega + push_cast. So h : ∀ j ∈ range (j₀−1), ((j₀−1−j:ℕ):ℝ)⁻¹ = (((j₀−2−j:ℕ):ℝ)+1)⁻¹: per-term: congr 1: ((j₀−1−j:ℕ):ℝ) = ((j₀−2−j:ℕ):ℝ)+1: by rw [Nat.cast_sub (by omega), Nat.cast_sub (by omega)]; push_cast; ring? hmm — ↑(j₀−1−j) = ↑j₀−1−j... Nat.cast_sub (h : j ≤ j₀−1): ↑(j₀−1−j) = ↑(j₀−1) − ↑j: and ↑(j₀−1) = ↑j₀ − 1 (Nat.cast_sub (1 ≤ j₀)): so LHS = ↑j₀ − 1 − ↑j; RHS = (↑j₀ − 2 − ↑j) + 1: equal by ring after those unfolds ✓.
OK this is all doable but VERY long. I'm going to write the complete §3 now via a full replacement of the contaminated region (lines 555–664), being extremely careful to paste ONLY Lean code. The edit's old_string anchors on the theorem start line 555 and the end markers at 667.
The contamination is extensive (lines 555–664). Replacing the whole §3 region with the complete clean proof.
tool: Edit
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigammaLeft.lean",
"old_string": "/-- **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 -- split range m = range j\u2080 \u222a Ico j\u2080 m\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]",
"new_string": "/-- **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 -- the harmonic bound in inv-form\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 -- split range m = range j\u2080 \u222a Ico j\u2080 m\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 (m - (j\u2080 + 1)) := hHarm _\n _ \u2264 1 + Real.log m := by\n by_cases hcase : m - (j\u2080 + 1) = 0\n \u00b7 rw [hcase]\n simp [Real.log_zero]\n exact Real.log_nonneg (by exact_mod_cast hm1)\n \u00b7 exact hlogmono (by omega) (by omega)\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 calc \u2211 j \u2208 Finset.Ico j\u2080 m, \u2016(w + (j : \u2102))\u207b\u00b9\u2016\n = \u2016(w + (j\u2080 : \u2102))\u207b\u00b9\u2016 + \u2211 j \u2208 Finset.Ico (j\u2080 + 1) m, \u2016(w + (j : \u2102))\u207b\u00b9\u2016 := by\n rw [Finset.add_sum_erase _ _ (Finset.left_mem_Ico.mpr (by omega : j\u2080 < m)),\n Finset.Ico_erase_left]\n _ \u2264 1 / c + (1 + Real.log m) := add_le_add hfirst_r hrest_r\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 -- the reversal bijection j \u21a6 j\u2080\u22122\u2212j on range (j\u2080\u22121)\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 -- ((j\u2080\u22121\u2212j : \u2115):\u211d)\u207b\u00b9 = ((j\u2080\u22122\u2212j : \u211d) + 1)\u207b\u00b9\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 push_cast\n ring\n rw [h1]\n _ \u2264 1 + Real.log (j\u2080 - 1) := hHarm _\n _ \u2264 1 + Real.log m := by\n by_cases hcase : j\u2080 - 1 = 0\n \u00b7 rw [hcase]\n simp [Real.log_zero]\n exact Real.log_nonneg (by exact_mod_cast hm1)\n \u00b7 exact hlogmono (by omega) (by omega)\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 -- combine\n linarith [hleft, hright]"
}
raw content_json (database row)
[{"type":"thinking","thinking":"The damage: §3's `digamma_recip_sum_le` theorem is incomplete (cuts off at line 577 mid-proof with `(Finset.Ico_self_singleton).symm...` and then all my planning text through line 664, then the end markers at 667/669). The helpers recip_norm_le_right (line 483) and recip_norm_le_left (line 514) are complete (they were in the good part of my edit before the contamination). The hsplit/hright part is partial.\n\nI need to: replace from line 570 (the \"-- RIGHT side\" comment) through line 664 (end of contamination) with the clean complete digamma_recip_sum_le proof, keeping `end NguyenRH1 / end`.\n\nThe clean complete proof of digamma_recip_sum_le:\n\n```\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 have hj₀1m : j₀ + 1 ≤ m := hm\n have hsplit : ... (the range split, already present at 564-568) ...\n rw [hsplit]\n -- harmonic in inv-form\n have hHarm : ∀ K : ℕ, ∑ i ∈ Finset.range K, ((i : ℝ) + 1)⁻¹ ≤ 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 : ∀ {a b : ℕ}, 1 ≤ a → a ≤ b → 1 + Real.log a ≤ 1 + Real.log b := by\n intro a b ha hab\n have h1 : (0 : ℝ) < (a : ℝ) := by exact_mod_cast ha\n have h2 : (a : ℝ) ≤ (b : ℝ) := by exact_mod_cast hab\n have h3 := Real.log_le_log h1 h2\n linarith [h3]\n -- RIGHT side\n have hfirst_r : ‖(w + (j₀ : ℂ))⁻¹‖ ≤ 1 / c := by\n rw [norm_inv, show (1 : ℝ) / c = c⁻¹ by rw [one_div]]\n have hpos : (0 : ℝ) < ‖w + (j₀ : ℂ)‖ := lt_of_lt_of_le hc (hdist j₀)\n exact (inv_le_inv₀ hpos hc).mpr (hdist j₀)\n have hrest_r : ∑ 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]\n apply Finset.sum_congr rfl\n intro i _\n have h1 : (j₀ + 1 + i) - j₀ = i + 1 := by omega\n rw [h1, Nat.cast_add_one]\n _ ≤ 1 + Real.log (m - (j₀ + 1)) := hHarm _\n _ ≤ 1 + Real.log m := by\n by_cases hcase : m - (j₀ + 1) = 0\n · rw [hcase]\n simp [Real.log_zero]\n exact Real.log_nonneg (by exact_mod_cast (by omega : 1 ≤ m))\n · exact hlogmono (by omega) (by omega)\n have hright : ∑ j ∈ Finset.Ico j₀ m, ‖(w + (j : ℂ))⁻¹‖ ≤ 1 / c + (1 + Real.log m) := by\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_r hrest_r\n -- LEFT side\n have hleft : ∑ j ∈ Finset.range j₀, ‖(w + (j : ℂ))⁻¹‖ ≤ 1 / c + (1 + Real.log m) := by\n by_cases hj₀0 : j₀ = 0\n · rw [hj₀0]\n simp -- range 0 sum = 0 ≤ 1/c + (1 + log m): needs 0 ≤ 1/c (hc) and 0 ≤ 1 + log m: log m ≥ 0 for m ≥ 1: m ≥ j₀+1 = 1 ✓: \n have h1 : (0 : ℝ) ≤ 1 / c := by positivity\n have h2 : (0 : ℝ) ≤ Real.log m := Real.log_nonneg (by exact_mod_cast (by omega : 1 ≤ m))\n linarith [h1, h2]\n · have hj₀1 : 1 ≤ j₀ := Nat.one_le_iff_ne_zero.mpr hj₀0\n -- range j₀ = range (j₀−1) + the j₀−1 term\n have hdecomp : ∑ j ∈ Finset.range j₀, ‖(w + (j : ℂ))⁻¹‖\n = ∑ j ∈ Finset.range (j₀ - 1), ‖(w + (j : ℂ))⁻¹‖ + ‖(w + ((j₀ - 1 : ℕ)) : ℂ)‖⁻¹ := by\n conv_lhs => rw [show j₀ = (j₀ - 1) + 1 by omega]\n rw [Finset.sum_range_succ]\n -- the last term ≤ 1/c\n have hlast : ‖(w + ((j₀ - 1 : ℕ)) : ℂ)⁻¹‖ ≤ 1 / c := by\n have hcast : ((j₀ - 1 : ℕ) : ℂ) = (j₀ : ℂ) - 1 := by\n rw [Nat.cast_sub hj₀1]\n push_cast\n ring\n -- dist at j₀−1 (a nat): hdist (j₀−1) : c ≤ ‖w + ↑(j₀−1)‖\n have hpos : (0 : ℝ) < ‖w + ((j₀ - 1 : ℕ) : ℂ)‖ := lt_of_lt_of_le hc (hdist (j₀ - 1))\n rw [norm_inv, show (1 : ℝ) / c = c⁻¹ by rw [one_div]]\n exact (inv_le_inv₀ hpos hc).mpr (hdist (j₀ - 1))\n -- the earlier terms: recip_norm_le_left + reflect reindex\n have hrest_l : ∑ j ∈ Finset.range (j₀ - 1), ‖(w + (j : ℂ))⁻¹‖ ≤ 1 + Real.log m := by\n calc ∑ j ∈ Finset.range (j₀ - 1), ‖(w + (j : ℂ))⁻¹‖\n ≤ ∑ j ∈ Finset.range (j₀ - 1), ((j₀ - 1 - j : ℕ) : ℝ)⁻¹ :=\n Finset.sum_le_sum fun j hj => recip_norm_le_left hdist hj₀ (by\n rw [Finset.mem_range] at hj; omega)\n _ = ∑ i ∈ Finset.range (j₀ - 1), ((i : ℝ) + 1)⁻¹ := by\n -- reflect: the map j ↦ j₀−1−j on range (j₀−1) hits {1,...,j₀−1}\n have h1 : ∀ j ∈ Finset.range (j₀ - 1),\n ((j₀ - 1 - j : ℕ) : ℝ)⁻¹ = ((j₀ - 1 - j : ℕ) : ℝ)⁻¹ := fun j _ => rfl\n -- use sum_range_reflect with f i := ((i+1 : ℕ):ℝ)⁻¹... \n rw [Finset.sum_range_reflect (fun x : ℕ => (((x : ℕ) + 1 : ℕ) : ℝ)⁻¹) (j₀ - 1)]\n -- hmm: sum_range_reflect f n : ∑ i ∈ range n, f (n − 1 − i) = ∑ i ∈ range n, f i\n -- with n := j₀−1: LHS = ∑ i ∈ range (j₀−1), f (j₀−1−1−i) = ∑ f (j₀−2−i)\n -- I need to first rewrite MY sum into the f (j₀−2−j) form:\n ...\n```\nHmm — the left reindex: my sum's term after recip_norm_le_left is ((j₀−1−j : ℕ):ℝ)⁻¹ for j ∈ range (j₀−1). Target form: ((i:ℝ)+1)⁻¹ = ((i+1:ℕ):ℝ)⁻¹. The reflect gives ∑ f (n−1−i) = ∑ f i with n := j₀−1, f x := ((x+1:ℕ):ℝ)⁻¹: LHS terms f (j₀−1−1−i) = f (j₀−2−i) = ((j₀−2−i+1:ℕ):ℝ)⁻¹ = ((j₀−1−i:ℕ):ℝ)⁻¹ (omega: j₀−2−i+1 = j₀−1−i for i ≤ j₀−2 ✓... j₀−2−i+1 = j₀−1−i needs j₀ ≥ ... j₀−2−i: careful when j₀ = 1: range (j₀−1) = range 0 = empty ✓ trivial). So:\n```\n _ = ∑ i ∈ Finset.range (j₀ - 1), ((i : ℝ) + 1)⁻¹ := by\n rw [Finset.sum_range_reflect (fun x : ℕ => (((x : ℕ) + 1 : ℕ) : ℝ)⁻¹) (j₀ - 1)]\n apply Finset.sum_congr rfl\n intro j hj\n rw [Finset.mem_range] at hj\n -- f (j₀−1−1−j) = ((j₀−1−1−j : ℕ)+1 : ℝ)⁻¹ = ((j₀−1−j : ℕ):ℝ)⁻¹ (the goal's term)\n have h1 : (j₀ - 1 - 1 - j) + 1 = j₀ - 1 - j := by omega\n rw [h1] -- hmm the f's cast: (((j₀−1−1−j : ℕ)+1 : ℕ):ℝ)⁻¹: the inner (x+1 : ℕ): after h1: ((j₀−1−j : ℕ):ℝ)⁻¹ — the cast chain: ((↑(j₀−1−1−j)+1 : ℕ):ℝ) — wait f x := (((x:ℕ)+1 : ℕ):ℝ)⁻¹ — the +1 is in ℕ then cast: ↑(x+1) = ↑x + 1 — my target ((i:ℝ)+1)⁻¹: ↑i + 1: matches after Nat.cast_add_one. And the LHS of the per-term congr: f (j₀−1−1−j) with x := j₀−1−1−j: ((↑(j₀−1−1−j)+1 : ℕ... hmm the +1 in f is the ℕ-addition (x+1 : ℕ): after h1 (j₀−1−1−j + 1 = j₀−1−j): the cast becomes ↑(j₀−1−j):ℝ: and the goal-side per-term is ((j₀−1−j : ℕ):ℝ)⁻¹ — MATCH... wait what's the goal at that point: after rw [sum_range_reflect ...] the goal becomes: ∑ j ∈ range (j₀−1), f (j₀−1−1−j)?? no — rw [sum_range_reflect f (j₀−1)] rewrites occurrences of ∑ i ∈ range (j₀−1), f (j₀−1−1−i)?? the lemma: sum_range_reflect f n : ∑ i ∈ range n, f (n−1−i) = ∑ i ∈ range n, f i — rw rewrites the LHS-pattern ∑_{range (j₀−1)} f (·−1−·)... my goal's LHS is ∑ ((j₀−1−j:ℕ):ℝ)⁻¹ — NOT of the form ∑ f (n−1−i) with f := fun x => ((x+1:ℕ):ℝ)⁻¹ — because f (j₀−1−j) = ((j₀−1−j)+1 : ℕ→ℝ)⁻¹ = ((j₀−j : ℕ):ℝ)⁻¹ — that's ((j₀−j))⁻¹ NOT my ((j₀−1−j))⁻¹. WRONG f. Take f x := ((x : ℕ):ℝ)⁻¹: then f (j₀−1−j) = ((j₀−1−j):ℕ→ℝ)⁻¹ ✓ MY term. reflect: ∑_{range (j₀−1)} f (j₀−1−1−j) = ∑_{range (j₀−1)} f j: the LHS pattern with n := j₀−1: f (n−1−j) = f (j₀−2−j) = ((j₀−2−j : ℕ):ℝ)⁻¹ — my LHS is ∑ f (j₀−1−j) — NOT the reflect's LHS pattern (which is f (j₀−2−j)). So rw [sum_range_reflect f (j₀−1)] rewrites ∑_{range(j₀−1)} f (j₀−2−j) — not present in my goal (I have f (j₀−1−j)) — FAIL. \n\nCorrect approach: my sum = ∑_{j ∈ range (j₀−1)} f (j₀−1−j) with f x := ((x:ℕ):ℝ)⁻¹. The reflect with n := j₀: ∑_{j ∈ range j₀} f (j₀−1−j) = ∑_{j ∈ range j₀} f j. My sum is over range (j₀−1) — one fewer. Hmm — handle via: ∑_{j ∈ range j₀} f (j₀−1−j) = [my sum over range (j₀−1)] + f (j₀−1−(j₀−1)) = my sum + f 0 = my sum + 0⁻¹ = my sum + 0 (inv_zero: 0⁻¹ = 0 — ((0:ℕ):ℝ)⁻¹ = 0⁻¹ = 0 ✓ inv_zero). So my sum = ∑_{range j₀} f (j₀−1−j) − 0 = ∑_{range j₀} f j [reflect] = ∑_{range (j₀−1)} f j + f (j₀−1) [sum_range_succ, j₀ = (j₀−1)+1]: f (j₀−1) = ((j₀−1:ℕ):ℝ)⁻¹ and ∑_{range (j₀−1)} f j = ∑_{j<j₀−1} (j:ℝ)⁻¹·... hmm the f j = (j:ℝ)⁻¹ for j = 0: 0⁻¹ = 0 ✓: so ∑_{range j₀} f j = ∑_{j=1}^{j₀−1} (j:ℝ)⁻¹ = H_{j₀−1}-ish in inv form = ∑_{i ∈ range (j₀−1)} ((i:ℝ)+1)⁻¹ [reindex j = i+1: ∑_{j ∈ range j₀, j ≥ 1} = ...] — ANOTHER reindex. \n\nUgh — the reflect path keeps generating off-by-one friction. Let me use a cleaner bij: `Finset.sum_nbij` or the direct: ∑_{j ∈ range (j₀−1)} f (j₀−1−j) = ∑_{i ∈ range (j₀−1)} f (i+1): via Finset.sum_bij with i := fun j _ => j₀−2−j (the involution on range (j₀−1) = {0,...,j₀−2}): \nFinset.sum_bij (i : ℕ → ℕ) (hi : ∀ j ∈ s, i j ∈ t) (hi_inj : InjOn i s) (hi_surj : SurjOn i s t) (h : ∀ j ∈ s, f j = g (i j)) : ∑ s f = ∑ t g — the signature in this Mathlib: `Finset.sum_bij {ι κ} {s : Finset ι} {t : Finset κ} {f : ι → M} {g : κ → M} (i : ι → κ) (hi : ∀ a ∈ s, i a ∈ t) (i_inj : Set.InjOn i s) (i_surj : Set.SurjOn i s t) (h : ∀ a ∈ s, f a = g (i a)) : ∑ x ∈ s, f x = ∑ x ∈ t, g x` ✓ roughly. With: s = t = range (j₀−1); i j := j₀−2−j; f j := ((j₀−1−j : ℕ):ℝ)⁻¹; g i := ((i:ℝ)+1)⁻¹. Check: i j ∈ range (j₀−1) for j ∈ range (j₀−1): j ≤ j₀−2 ⟹ j₀−2−j ∈ [0, j₀−2] ✓ omega. InjOn: j₀−2−j is injective on the range (sub by constant) ✓ (omega-driven: intro a _ b _ h; omega). SurjOn: for i ∈ range (j₀−1): preimage j := j₀−2−i ∈ range ✓ and i (j₀−2−i) = j₀−2−(j₀−2−i) = i ✓ omega. The function equation: f j = g (i j): ((j₀−1−j:ℕ):ℝ)⁻¹ = ((j₀−2−j : ℝ)+1)⁻¹: j₀−1−j = (j₀−2−j)+1 as nats for j ≤ j₀−2 ✓ then cast: ↑(j₀−2−j)+1 = ↑(j₀−1−j)... : ((j₀−2−j:ℕ):ℝ)+1 = ((j₀−1−j:ℕ):ℝ): Nat.cast_sub chains... omega + push_cast. So h : ∀ j ∈ range (j₀−1), ((j₀−1−j:ℕ):ℝ)⁻¹ = (((j₀−2−j:ℕ):ℝ)+1)⁻¹: per-term: congr 1: ((j₀−1−j:ℕ):ℝ) = ((j₀−2−j:ℕ):ℝ)+1: by rw [Nat.cast_sub (by omega), Nat.cast_sub (by omega)]; push_cast; ring? hmm — ↑(j₀−1−j) = ↑j₀−1−j... Nat.cast_sub (h : j ≤ j₀−1): ↑(j₀−1−j) = ↑(j₀−1) − ↑j: and ↑(j₀−1) = ↑j₀ − 1 (Nat.cast_sub (1 ≤ j₀)): so LHS = ↑j₀ − 1 − ↑j; RHS = (↑j₀ − 2 − ↑j) + 1: equal by ring after those unfolds ✓.\n\nOK this is all doable but VERY long. I'm going to write the complete §3 now via a full replacement of the contaminated region (lines 555–664), being extremely careful to paste ONLY Lean code. The edit's old_string anchors on the theorem start line 555 and the end markers at 667.","signature":""},{"type":"text","text":"The contamination is extensive (lines 555–664). Replacing the whole §3 region with the complete clean proof."},{"type":"tool_use","id":"Edit_392","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigammaLeft.lean","old_string":"/-- **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]","new_string":"/-- **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 have hm1 : 1 ≤ m := by omega\n -- the harmonic bound in inv-form\n have hHarm : ∀ K : ℕ, ∑ i ∈ Finset.range K, ((i : ℝ) + 1)⁻¹ ≤ 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 : ∀ {a b : ℕ}, 1 ≤ a → a ≤ b →\n 1 + Real.log (a : ℝ) ≤ 1 + Real.log (b : ℝ) := by\n intro a b ha hab\n have h1 : (0 : ℝ) < (a : ℝ) := by exact_mod_cast ha\n have h2 : (a : ℝ) ≤ (b : ℝ) := by exact_mod_cast hab\n have h3 := Real.log_le_log h1 h2\n linarith [h3]\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\n have hfirst_r : ‖(w + (j₀ : ℂ))⁻¹‖ ≤ 1 / c := by\n rw [norm_inv, show (1 : ℝ) / c = c⁻¹ by rw [one_div]]\n have hpos : (0 : ℝ) < ‖w + (j₀ : ℂ)‖ := lt_of_lt_of_le hc (hdist j₀)\n exact (inv_le_inv₀ hpos hc).mpr (hdist j₀)\n have hrest_r : ∑ 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]\n apply Finset.sum_congr rfl\n intro i _\n have h1 : (j₀ + 1 + i) - j₀ = i + 1 := by omega\n rw [h1, Nat.cast_add_one]\n _ ≤ 1 + Real.log (m - (j₀ + 1)) := hHarm _\n _ ≤ 1 + Real.log m := by\n by_cases hcase : m - (j₀ + 1) = 0\n · rw [hcase]\n simp [Real.log_zero]\n exact Real.log_nonneg (by exact_mod_cast hm1)\n · exact hlogmono (by omega) (by omega)\n have hright : ∑ j ∈ Finset.Ico j₀ m, ‖(w + (j : ℂ))⁻¹‖ ≤ 1 / c + (1 + Real.log m) := by\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_r hrest_r\n -- LEFT side\n have hleft : ∑ j ∈ Finset.range j₀, ‖(w + (j : ℂ))⁻¹‖ ≤ 1 / c + (1 + Real.log m) := by\n by_cases hj₀0 : j₀ = 0\n · rw [hj₀0]\n simp only [Finset.range_zero, Finset.sum_empty]\n have h1 : (0 : ℝ) ≤ 1 / c := by positivity\n have h2 : (0 : ℝ) ≤ Real.log m := Real.log_nonneg (by exact_mod_cast hm1)\n linarith [h1, h2]\n · have hj₀1 : 1 ≤ j₀ := Nat.one_le_iff_ne_zero.mpr hj₀0\n have hdecomp : ∑ j ∈ Finset.range j₀, ‖(w + (j : ℂ))⁻¹‖\n = ∑ j ∈ Finset.range (j₀ - 1), ‖(w + (j : ℂ))⁻¹‖\n + ‖(w + ((j₀ - 1 : ℕ) : ℂ))⁻¹‖ := by\n conv_lhs => rw [show j₀ = (j₀ - 1) + 1 by omega]\n rw [Finset.sum_range_succ]\n have hlast : ‖(w + ((j₀ - 1 : ℕ) : ℂ))⁻¹‖ ≤ 1 / c := by\n have hpos : (0 : ℝ) < ‖w + ((j₀ - 1 : ℕ) : ℂ)‖ := lt_of_lt_of_le hc (hdist (j₀ - 1))\n rw [norm_inv, show (1 : ℝ) / c = c⁻¹ by rw [one_div]]\n exact (inv_le_inv₀ hpos hc).mpr (hdist (j₀ - 1))\n have hrest_l : ∑ j ∈ Finset.range (j₀ - 1), ‖(w + (j : ℂ))⁻¹‖ ≤ 1 + Real.log m := by\n calc ∑ j ∈ Finset.range (j₀ - 1), ‖(w + (j : ℂ))⁻¹‖\n ≤ ∑ j ∈ Finset.range (j₀ - 1), ((j₀ - 1 - j : ℕ) : ℝ)⁻¹ :=\n Finset.sum_le_sum fun j hj => recip_norm_le_left hdist hj₀ (by\n rw [Finset.mem_range] at hj; omega)\n _ = ∑ i ∈ Finset.range (j₀ - 1), ((i : ℝ) + 1)⁻¹ := by\n -- the reversal bijection j ↦ j₀−2−j on range (j₀−1)\n apply Finset.sum_bij (fun j _ => j₀ - 2 - j)\n · intro j hj\n rw [Finset.mem_range] at hj\n exact Finset.mem_range.mpr (by omega)\n · intro j₁ hj₁ j₂ hj₂ h\n rw [Finset.mem_range] at hj₁ hj₂\n omega\n · intro i hi\n rw [Finset.mem_range] at hi\n exact ⟨j₀ - 2 - i, Finset.mem_range.mpr (by omega), by omega⟩\n · intro j hj\n rw [Finset.mem_range] at hj\n -- ((j₀−1−j : ℕ):ℝ)⁻¹ = ((j₀−2−j : ℝ) + 1)⁻¹\n have h1 : ((j₀ - 1 - j : ℕ) : ℝ) = ((j₀ - 2 - j : ℕ) : ℝ) + 1 := by\n rw [Nat.cast_sub (by omega : j ≤ j₀ - 1),\n Nat.cast_sub (by omega : j ≤ j₀ - 2),\n Nat.cast_sub hj₀1]\n push_cast\n ring\n rw [h1]\n _ ≤ 1 + Real.log (j₀ - 1) := hHarm _\n _ ≤ 1 + Real.log m := by\n by_cases hcase : j₀ - 1 = 0\n · rw [hcase]\n simp [Real.log_zero]\n exact Real.log_nonneg (by exact_mod_cast hm1)\n · exact hlogmono (by omega) (by omega)\n calc ∑ j ∈ Finset.range j₀, ‖(w + (j : ℂ))⁻¹‖\n = ∑ j ∈ Finset.range (j₀ - 1), ‖(w + (j : ℂ))⁻¹‖\n + ‖(w + ((j₀ - 1 : ℕ) : ℂ))⁻¹‖ := hdecomp\n _ ≤ (1 + Real.log m) + 1 / c := add_le_add hrest_l hlast\n _ = 1 / c + (1 + Real.log m) := by ring\n -- combine\n linarith [hleft, hright]"},"extra_content":null}]