← Session 22 — ii′-1: liCoeff pairing fix + residue machinery
thinking (9916 chars)
Wait — several concerns in iteratedDerivWithin_dpsiTermC:
1. The `rw [show ... from rfl]` lines are pointless (rfl identities don't rewrite anything meaningful). The issue: the goal after `rw [heq]` — heq's RHS is `(fun s => 1/(↑m+1)) + fun s => -(1/(s+↑m+1))` — wait I wrote heq's RHS as `(fun s : ℂ => 1 / ((m : ℂ) + 1)) + fun s : ℂ => -(1 / (s + ↑m + 1))` — that's `(lambda) + (lambda)` — HAdd of two lambdas — which is defeq to the Pi.add form `(fun s => ...) + (fun s => ...)`? — `(fun s => 1/(↑m+1)) + (fun s => -(1/(s+↑m+1)))` — HAdd.hAdd of the two lambda TERMS — NOT the same as Pi.add's application `(F + G)` — iteratedDeriv_add's LHS is `iteratedDeriv n (f + g) x` with `f + g` = Pi.add — HAdd.hAdd F G — and my lambda-sum `F + G` is also HAdd.hAdd F G — the Pi.instAdd's HAdd — same ✓. So the `show ... from rfl` line is vacuous — remove it. And the iteratedDeriv_add should apply directly.
2. The `rw [show (fun s : ℂ => s + ↑m + 1) = fun s : ℂ => s + (↑m + 1) from rfl] at *` — also vacuous/rfl — the association: my zpow lemma's conclusion has (s + c) with c := ↑m + 1 — so the base is `s + (↑m + 1)` — but the target form has `(s + ↑m + 1)` — `(s + ↑m) + 1` vs `s + (↑m + 1)` — DIFFERENT association — NOT defeq? — add_assoc: (a+b)+c = a+(b+c) — they ARE propositionally equal via add_assoc — not rfl. So the base in the zpow-lemma call's conclusion is `s + (↑m + 1)` but my lemma's stated conclusion has `(s + ↑m + 1)` — mismatch — fix: change the lemma's stated conclusion to use `s + (↑m + 1)`? — or call the zpow lemma with c := (↑m + 1) and then the conclusion's base is (s + (↑m+1)) — then convert via add_assoc — `rw [show (s : ℂ) + (↑m + 1) = s + ↑m + 1 from by ring]`? — direction: s + (↑m+1) = (s+↑m)+1 by (add_assoc).symm — hmm add_assoc : a+b+c = a+(b+c) — so (s+↑m)+1 = s+(↑m+1) is add_assoc and s+(↑m+1) = (s+↑m)+1 is add_assoc.symm — rw [add_assoc] turns s+(↑m+1) into (s+↑m)+1 ✓.
Let me restructure the ending of iteratedDerivWithin_dpsiTermC:
```lean
rw [heq]
have hcf : ContDiffAt ℂ k (fun s : ℂ => 1 / ((m : ℂ) + 1)) s := contDiff_const.contDiffAt
have hcg : ContDiffAt ℂ k (fun s : ℂ => -(1 / (s + ↑m + 1))) s := ...
rw [iteratedDeriv_add hcf hcg]
rw [iteratedDeriv_const, if_neg (by omega : k ≠ 0)]
have h4 := iteratedDeriv_neg_one_div_add_const k (↑m + 1) (c := (↑m : ℂ) + 1) (by ...)
-- h4 : iteratedDeriv k (fun s => -(1 / (s + (↑m+1)))) s = −(−1)^k·k!·(s + (↑m+1))^{−(k+1)}
...
```
Hmm — the function in hcg/h4 is fun s => -(1/(s + ↑m + 1)) — with base (s + ↑m + 1) — and the zpow lemma's function is fun s => -(1/(s + c)) with c := (↑m+1) — base (s + (↑m+1)) — the functions differ associationally: fun s => -(1/(s + ↑m + 1)) vs fun s => -(1/(s + (↑m+1))) — defeq? (s+↑m)+1 vs s+(↑m+1) — propositionally equal via add_assoc, not defeq — so the function equality needs funext+ring. Let me handle with a show:
```lean
have h4 : iteratedDeriv k (fun s : ℂ => -(1 / (s + ↑m + 1))) s =
-((-1 : ℂ)) ^ k * (k ! : ℂ) * (s + ↑m + 1) ^ (-(k : ℤ) - 1) := by
have h5 : (fun s : ℂ => -(1 / (s + ↑m + 1))) = fun s : ℂ => -(1 / (s + ((m : ℂ) + 1))) := by
funext s
rw [add_assoc]
rw [h5]
rw [iteratedDeriv_neg_one_div_add_const k ((m : ℂ) + 1) ?_]
· rw [add_assoc] -- hmm — the conclusion's base s + (↑m+1) → s+↑m+1 — wait direction
· -- s + (↑m+1) ≠ 0 from hsm: s + ↑m + 1 ≠ 0 — same value: add_assoc
rw [← add_assoc] -- hmm
exact hsm
```
careful: the side goal: s + (↑m + 1) ≠ 0 — from hsm : s + ↑m + 1 ≠ 0 — add_assoc.symm... — `rwa [add_assoc]`? — the side goal s + (↑m+1) ≠ 0 — rw [add_assoc] turns it into (s+↑m)+1 ≠ 0 — is that hsm's form? hsm : s + ↑m + 1 ≠ 0 — which parses as (s + ↑m) + 1 ≠ 0 ✓ — so rw [add_assoc] at the side goal makes it match hsm ✓ then exact hsm. And h4's conclusion base: (s + (↑m+1))^{...} — I want (s + ↑m + 1) — rw [add_assoc] turns s+(↑m+1) → s+↑m+1 ✓ — hmm direction: add_assoc : (a+b)+c = a+(b+c) — rw [add_assoc] rewrites (a+b)+c → a+(b+c) — I want the reverse: (s+↑m)+1 → s+(↑m+1) — that's ← add_assoc. And the side-goal s + (↑m+1) ≠ 0 → (s+↑m)+1 ≠ 0 is add_assoc forward. Ugh — let me just be careful:
- h4's conclusion after the zpow lemma: −(−1)^k·k!·(s + (↑m+1))^{−(k+1)} — I want to display it as (s + ↑m + 1)^{−(k+1)}: the base s + (↑m+1) → (s+↑m)+1 — via `rw [← add_assoc]`?? — no: add_assoc : (a+b)+c = a+(b+c) — the LHS form is (s+↑m)+1 — hmm — I have s + (↑m+1) and want s + ↑m + 1 = (s+↑m)+1 — so rewrite s+(↑m+1) → (s+↑m)+1: that's ← add_assoc (since add_assoc says (s+↑m)+1 = s+(↑m+1)) ✓ so rw [← add_assoc] on h4's conclusion. But rw [← add_assoc] might hit other additions — the conclusion has several +'s — risky. Use `show`:
```lean
rw [h5]
rw [iteratedDeriv_neg_one_div_add_const k ((m : ℂ) + 1) (by rw [add_assoc]; exact hsm)]
rw [← add_assoc]
```
Hmm — `rw [add_assoc]` on the side goal s + (↑m+1) ≠ 0: add_assoc forward turns s+(↑m+1) into (s+↑m)+1 ✓ matches hsm ✓. And the final `rw [← add_assoc]` on the main goal — the conclusion after the zpow-lemma rewrite: −(−1)^k·↑k!·(s+(↑m+1))^(−(k:ℤ)−1) — the base s + (↑m+1) — ← add_assoc rewrites it to (s+↑m)+1 ✓ — other additions: the exponent −(k:ℤ)−1 — contains subtraction not add ✓; the (↑m+1) inside the base is GONE (became (s+↑m)+1) — hmm — careful — ← add_assoc : a+(b+c) → (a+b)+c — the goal might have other a+(b+c) patterns — the exponent −(k:ℤ)−1 is a subtraction ✓; the (↑m+1) — wait after the rewrite the base becomes (s+↑m)+1 — and there's no other a+(b+c) shape... the k!'s etc no. Should be OK-ish; if it hits the wrong one, use show.
Actually — simplest robust: end with `show`ing the target and `ring_nf`-proving the whole equation? No — the zpow atom blocks ring. Alternative: make the FINAL statement use the base `s + (↑m + 1)` — i.e., state iteratedDerivWithin_dpsiTermC's conclusion with `(s + (↑m + 1))`?? — but the downstream (the sum at 1/2) computes with (1/2 + ↑m + 1) — association normalization needed SOMEWHERE. Let me just leave the lemma's conclusion as `(s + ↑m + 1)` and handle the association by `show`:
After all the rewrites, the goal is:
0 + (−(−1)^k·↑k!·(s + (↑m+1))^{−(k:ℤ)−1}) = −(−1)^k·↑k!·(s+↑m+1)^(−(k:ℤ)−1)
— zero_add first: then −(−1)^k·↑k!·(s+(↑m+1))^(...) = −(−1)^k·↑k!·(s+↑m+1)^(...) — the bases differ by association — `show` the RHS with the (s+(↑m+1)) form? no — the GOAL is the full equation — `congr 1`? — the two sides are products of atoms (−(−1)^k, ↑k!, the zpow) — congr 1 recursively splits into atom equalities — the zpow atom equality: (s+(↑m+1))^(−(k:ℤ)−1) = (s+↑m+1)^(−(k:ℤ)−1) — by congr 1 → s+(↑m+1) = s+↑m+1 → add_assoc ✓. So end with:
```lean
rw [zero_add] -- if the 0 + is there
congr 3 -- or congr 1 repeatedly — splits HMul chains: a*b*c = a'*b'*c' → a=a', b=b', c=c' — congr 2 maybe
rw [add_assoc]
```
Hmm — `congr 3` might overshoot (splitting into the exponent pieces etc.). Let me use: `congr 1; congr 1; rw [add_assoc]`... — fragile. SAFEST: keep the lemma statement's base as `(s + ↑m + 1)` and make the zpow-lemma application produce exactly that by choosing its function input as `fun s => -(1 / (s + ↑m + 1))` — i.e., prove the one-div lemma with the base as-written `s + c` and apply with c := ↑m + 1 — then the conclusion's base is `s + (↑m + 1)` — the association difference is INSIDE the base atom — Lean sees (s + (↑m+1)) vs (s + ↑m + 1) as different atoms. So the mismatch is unavoidable at the atom level — must add_assoc somewhere. Fine — end with:
```lean
simp only [zero_add]
rw [← add_assoc] -- no wait — I have s + (↑m+1), want (s+↑m)+1: ← add_assoc ✓ — but which occurrence — the goal after everything: −(−1)^k·↑k!·(s+(↑m+1))^(−(k:ℤ)−1) = −(−1)^k·↑k!·(s+↑m+1)^(−(k:ℤ)−1) — hmm — actually WAIT: after `rw [iteratedDeriv_neg_one_div_add_const ...]` the goal's LHS (the summand's iterated deriv) BECOMES the closed form — the goal is then:
(0 + −(−1)^k·↑k!·(s + (↑m+1))^(−(k:ℤ)−1)) = −(−1)^k·↑k!·(s + ↑m + 1)^(−(k:ℤ)−1)
rw [zero_add] -- LHS → the closed form
-- now the only difference: the base association
rw [add_assoc] -- (s+↑m)+1 → s+(↑m+1)?? — the RHS's base — hmm — add_assoc forward turns (s+↑m)+1 into s+(↑m+1) — the RHS's base is (s+↑m)+1 = displayed `s + ↑m + 1` — so rw [add_assoc] rewrites the RHS's base → s+(↑m+1) — matching the LHS ✓ rfl closed by rw.
```
So: rw [zero_add, add_assoc]. The add_assoc rewrites the FIRST (a+b)+c pattern — the RHS's base (s+↑m)+1 ✓... — but is there an earlier (a+b)+c in the goal? The LHS after zero_add: −(−1)^k·↑k!·(s+(↑m+1))^(−(k:ℤ)−1) — patterns (a+b)+c: (−(−1)^k·↑k!)·(zpow) — the multiplications not additions ✓; the exponent −(k:ℤ)−1 — subtraction ✓; (s+(↑m+1)) — the base: s + (↑m+1) — a+(b+c) form — add_assoc forward would rewrite THIS first if it comes first in the traversal!! — the goal LHS is −(−1)^k·↑k!·(s+(↑m+1))^(...) and RHS is −(−1)^k·↑k!·((s+↑m)+1)^(...) — the traversal order (outermost-first, left-to-right): LHS and RHS both have the same head Eq, then the LHS's product chain... — the first (a+b)+c occurrence scanning the goal: Eq LHS RHS — LHS: the product — contains (s + (↑m+1)) — that's a+(b+c) — add_assoc FORWARD matches a+(b+c) → (a+b)+c — rewriting the LHS's base to (s+↑m)+1 ✓ THEN both sides have (s+↑m)+1 ✓ rfl ✓. Hmm — so rw [add_assoc] forward on the LHS base: s+(↑m+1) → (s+↑m)+1 ✓ then goal LHS = RHS ✓. Wait — does rw [add_assoc] rewrite ALL matches of the first-found pattern or just the first? rw rewrites ALL instances of the pattern-instance (the first matched pattern determines the metavars, then all occurrences of that instance). First match: scanning the Eq goal — LHS first — finds s + (↑m+1) (a := s, b := ↑m, c := 1) — rewrites all occurrences of s + (↑m + 1) → (s + ↑m) + 1 — the LHS's base ✓ (the RHS has (s+↑m)+1 — not of the form a+(b+c) — untouched) — result: both sides identical ✓.
OK — let me apply this ending fix. Let me view the current end of the lemma and fix.
Let me fix the ending of the summand-derivative lemma.
tool: Edit ok
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigamma.lean",
"old_string": " rw [heq]\n have hcf : ContDiffAt \u2102 k (fun s : \u2102 => 1 / ((m : \u2102) + 1)) s := contDiff_const.contDiffAt\n have hcg : ContDiffAt \u2102 k (fun s : \u2102 => -(1 / (s + \u2191m + 1))) s := by\n have h2 : AnalyticAt \u2102 (fun s : \u2102 => s + \u2191m + 1) s :=\n (analyticAt_id.add analyticAt_const).add analyticAt_const\n have h3 : AnalyticAt \u2102 (fun s : \u2102 => 1 / (s + \u2191m + 1)) s :=\n analyticAt_const.div h2 hsm\n exact h3.neg.contDiffAt\n rw [show ((fun s : \u2102 => 1 / ((m : \u2102) + 1)) + fun s : \u2102 => -(1 / (s + \u2191m + 1))) =\n (fun s : \u2102 => 1 / ((m : \u2102) + 1)) + (fun s : \u2102 => -(1 / (s + \u2191m + 1))) from rfl]\n rw [iteratedDeriv_add hcf hcg]\n rw [iteratedDeriv_const, if_neg (by omega : k \u2260 0)]\n rw [show (fun s : \u2102 => s + \u2191m + 1) = fun s : \u2102 => s + (\u2191m + 1) from rfl] at *\n rw [iteratedDeriv_neg_one_div_add_const k (\u2191m + 1) (by simpa using hsm)]\n simp [add_assoc]\n\nend NguyenRH1",
"new_string": " rw [heq]\n have hcf : ContDiffAt \u2102 k (fun s : \u2102 => 1 / ((m : \u2102) + 1)) s := contDiff_const.contDiffAt\n have hcg : ContDiffAt \u2102 k (fun s : \u2102 => -(1 / (s + \u2191m + 1))) s := by\n have h2 : AnalyticAt \u2102 (fun s : \u2102 => s + \u2191m + 1) s :=\n (analyticAt_id.add analyticAt_const).add analyticAt_const\n have h3 : AnalyticAt \u2102 (fun s : \u2102 => 1 / (s + \u2191m + 1)) s :=\n analyticAt_const.div h2 hsm\n exact h3.neg.contDiffAt\n rw [iteratedDeriv_add hcf hcg]\n rw [iteratedDeriv_const, if_neg (by omega : k \u2260 0)]\n have h4 : iteratedDeriv k (fun s : \u2102 => -(1 / (s + \u2191m + 1))) s =\n -((-1 : \u2102)) ^ k * (k ! : \u2102) * (s + \u2191m + 1) ^ (-(k : \u2124) - 1) := by\n have h5 : (fun s : \u2102 => -(1 / (s + \u2191m + 1))) =\n fun s : \u2102 => -(1 / (s + ((m : \u2102) + 1))) := by\n funext s\n rw [add_assoc]\n rw [h5]\n rw [iteratedDeriv_neg_one_div_add_const k ((m : \u2102) + 1) (by rw [add_assoc]; exact hsm)]\n rw [\u2190 add_assoc]\n rw [h4]\n rw [zero_add]"
}
result 2026-08-22 08:30:45Z → 2026-08-23 19:55:48Z
{
"filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiCircleBound.lean",
"oldString": "lemma fiber_mult_count {X : \u211d} (hX : 200 \u2264 X) (j : \u2115) :\n \u2211 \u03c1 \u2208 (dyadClass_fiber_finite (by linarith : (0 : \u211d) < X) j).toFinset,\n (zeroMult (\u03c1 : \u2102) : \u211d)\n \u2264 A0count * ((2 : \u211d) ^ (j + 1) * X + 3) * Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) := by",
"newString": "lemma fiber_mult_count {X : \u211d} (hX : 200 \u2264 X) (j : \u2115) :\n \u2211 \u03c1 \u2208 ((dyadClass_fiber_finite (by linarith : (0 : \u211d) < X) j).inter\n {\u03c1 : {\u03c1 // IsNontrivialZero \u03c1} | X < |(\u03c1 : \u2102).im|}\n (Set.Finite.subset (Set.finite_lt_nat' ...))).toFinset,\n (zeroMult (\u03c1 : \u2102) : \u211d)\n \u2264 A0count * ((2 : \u211d) ^ (j + 1) * X + 3) * Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) := by",
"originalFile": "/-\nNguyenRH1/LiCircleBound.lean \u2014 tier ii\u2032 sub-stage ii\u2032-5e-v (D-068 \u00a75):\nthe circle bound for the partial-fraction difference and the squeeze to\nthe capstone identity.\n\n\u00a70: conjugate symmetry of the nontrivial zeros (for the lower-half\n circle arcs).\n\u00a71: the mult-weighted ordinate-window count bridges from Zeta23's RvM\n local count (`zeta_local_zero_count`: Ncount(t, t+1] \u2264 A\u2080\u00b7log(|t|+3)\n with multiplicity, ALL t \u2014 no perimeter): `A0count` + the dyadic\n interval count `Ncount_le_of_interval`.\n\u00a72: the Dirichlet bound `norm_logDeriv_zeta_le_dirichlet` (\u2016\u03b6\u2032/\u03b6 s\u2016 \u2264\n dirichletC2 for re s \u2265 2; \u2212\u03b6\u2032/\u03b6 = LSeries \u039b, termwise \u2264 the s = 2\n majorant) \u2014 the right near-axis arc input.\n\u00a73+: (this file, subsequent sub-stages) the series bound, the logDeriv\n assembly, the Fexpr circle bound, the Schwarz squeeze, and the\n capstone `partialFraction_identity`.\n\nArchive references: D-068 \u00a75, journal-029.\n-/\nimport Mathlib\nimport Zeta23.RvM.LocalCount\nimport NguyenRH1.LiFEntire\nimport NguyenRH1.LiGapCircles\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 0. Conjugate symmetry -/\n\n/-- The conjugate of a nontrivial zero is a nontrivial zero. -/\nlemma isNontrivialZero_conj {\u03c1 : \u2102} (h\u03c1 : IsNontrivialZero \u03c1) :\n IsNontrivialZero ((starRingEnd \u2102) \u03c1) := by\n refine \u27e8?_, ?_, ?_\u27e9\n \u00b7 rw [_root_.riemannZeta_conj, h\u03c1.1, map_zero]\n \u00b7 rw [Complex.conj_re]; exact h\u03c1.2.1\n \u00b7 rw [Complex.conj_re]; exact h\u03c1.2.2\n\n/-! ## 1. The mult-weighted window count bridges -/\n\n/-- The local-count constant: from Zeta23's RvM local count\n(`zeta_local_zero_count`, [Tit86 Thm 9.2] \u2014 mult-weighted, two-sided,\nall t, PROVED unconditionally in Zeta23). -/\ndef A0count : \u211d := Classical.choose Zeta23.RvM.zeta_local_zero_count\n\nlemma A0count_ge_one : (1 : \u211d) \u2264 A0count :=\n (Classical.choose_spec Zeta23.RvM.zeta_local_zero_count).1\n\nlemma A0count_pos : (0 : \u211d) < A0count := lt_of_lt_of_le one_pos A0count_ge_one\n\n/-- The unit-window bound: Ncount(t, t+1] \u2264 A\u2080\u00b7log(|t|+3). -/\nlemma Ncount_window_le (t : \u211d) :\n (Zeta23.Ncount t (t + 1) : \u211d) \u2264 A0count * Real.log (|t| + 3) :=\n (Classical.choose_spec Zeta23.RvM.zeta_local_zero_count).2 t\n\n/-- Window additivity: Ncount(a, c] = Ncount(a, b] + Ncount(b, c] for\na \u2264 b \u2264 c (the disjoint union of the ordinate windows). -/\nlemma Ncount_add_of_le {a b c : \u211d} (hab : a \u2264 b) (hbc : b \u2264 c) :\n Zeta23.Ncount a c = Zeta23.Ncount a b + Zeta23.Ncount b c := by\n have hunion : Zeta23.zerosIn a c = Zeta23.zerosIn a b \u222a Zeta23.zerosIn b c := by\n ext \u03c1\n constructor\n \u00b7 intro h\u03c1c\n obtain \u27e8h\u03c1, ha, hc\u27e9 := h\u03c1c\n rcases le_or_gt \u03c1.im b with h | h\n \u00b7 exact Set.mem_union_left _ \u27e8h\u03c1, ha, h\u27e9\n \u00b7 exact Set.mem_union_right _ \u27e8h\u03c1, h, hc\u27e9\n \u00b7 intro h\n rcases h with h\u03c1b | h\u03c1c\n \u00b7 obtain \u27e8h\u03c1, ha, hb\u27e9 := h\u03c1b\n exact \u27e8h\u03c1, ha, hb.trans hbc\u27e9\n \u00b7 obtain \u27e8h\u03c1, hb, hc\u27e9 := h\u03c1c\n exact \u27e8h\u03c1, hab.trans_lt hb, hc\u27e9\n have hdisj : Disjoint (Zeta23.zerosIn a b) (Zeta23.zerosIn b c) := by\n rw [Set.disjoint_iff]\n intro \u03c1 \u27e8h1, h2\u27e9\n exact absurd (h1.2.2.trans_lt h2.2.1) (lt_irrefl \u03c1.im)\n rw [Zeta23.Ncount, Zeta23.Ncount, Zeta23.Ncount, hunion]\n exact_mod_cast finsum_mem_union hdisj (Zeta23.zerosIn_finite a b)\n (Zeta23.zerosIn_finite b c)\n\n/-- The N-step unit-window chain: Ncount(a, a+N] \u2264 A\u2080\u00b7N\u00b7log(|a|+N+3). -/\nlemma Ncount_chain_le (a : \u211d) (N : \u2115) :\n (Zeta23.Ncount a (a + (N : \u211d)) : \u211d)\n \u2264 A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3) := by\n induction N with\n | zero =>\n simp only [Nat.cast_zero, add_zero]\n have h0 : Zeta23.zerosIn a a = \u2205 := by\n ext \u03c1\n constructor\n \u00b7 intro h\n obtain \u27e8-, h1, h2\u27e9 := h\n exact absurd (h2.trans_lt h1) (lt_irrefl _)\n \u00b7 intro h\n simp at h\n have hz : Zeta23.Ncount a a = 0 := by\n simp only [Zeta23.Ncount, h0, finsum_mem_empty]\n rw [hz, Nat.cast_zero]\n simp\n | succ N ih =>\n have hN0 : (0 : \u211d) \u2264 (N : \u211d) := Nat.cast_nonneg N\n have hsplit : Zeta23.Ncount a (a + (N : \u211d) + 1)\n = Zeta23.Ncount a (a + (N : \u211d)) + Zeta23.Ncount (a + (N : \u211d)) (a + (N : \u211d) + 1) :=\n Ncount_add_of_le (a := a) (b := a + (N : \u211d)) (c := a + (N : \u211d) + 1)\n (by linarith) (by linarith)\n have hcast : a + ((N + 1 : \u2115) : \u211d) = a + (N : \u211d) + 1 := by push_cast; ring\n rw [hcast, hsplit]\n have hwin := Ncount_window_le (a + (N : \u211d))\n have hlog : Real.log (|a + (N : \u211d)| + 3) \u2264 Real.log (|a| + (N : \u211d) + 3) := by\n apply Real.log_le_log (by positivity)\n have h1 : |a + (N : \u211d)| \u2264 |a| + (N : \u211d) :=\n (abs_add_le _ _).trans (by rw [abs_of_nonneg (show (0 : \u211d) \u2264 (N : \u211d) from Nat.cast_nonneg N)])\n linarith\n have hlogpos : (0 : \u211d) \u2264 Real.log (|a| + (N : \u211d) + 3) := by\n apply Real.log_nonneg\n have h1 : (1 : \u211d) \u2264 |a| + 3 := by linarith [abs_nonneg a]\n linarith [hN0]\n have hlogpos' : (0 : \u211d) \u2264 Real.log (|a| + ((N : \u211d) + 1) + 3) := by\n apply Real.log_nonneg\n have h1 : (1 : \u211d) \u2264 |a| + 3 := by linarith [abs_nonneg a]\n linarith [hN0]\n push_cast\n -- goal: \u2191(Ncount a (a+\u2191N)) + \u2191(Ncount (a+\u2191N) (a+\u2191N+1)) \u2264 A\u2080(\u2191N+1)\u00b7log(|a|+(\u2191N+1)+3)\n have hlogC : Real.log (|a| + (N : \u211d) + 3)\n \u2264 Real.log (|a| + ((N : \u211d) + 1) + 3) :=\n Real.log_le_log (by positivity) (by linarith)\n have hle1 : A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3)\n \u2264 A0count * (N : \u211d) * Real.log (|a| + ((N : \u211d) + 1) + 3) :=\n mul_le_mul_of_nonneg_left hlogC (mul_nonneg A0count_pos.le hN0)\n have hle2 : A0count * Real.log (|a + (N : \u211d)| + 3)\n \u2264 A0count * Real.log (|a| + ((N : \u211d) + 1) + 3) := by\n apply mul_le_mul_of_nonneg_left _ A0count_pos.le\n apply Real.log_le_log (by positivity)\n have h1 : |a + (N : \u211d)| \u2264 |a| + (N : \u211d) :=\n (abs_add_le _ _).trans (by rw [abs_of_nonneg (show (0 : \u211d) \u2264 (N : \u211d) from Nat.cast_nonneg N)])\n linarith\n have hsum : \u2191(Zeta23.Ncount a (a + (N : \u211d))) + \u2191(Zeta23.Ncount (a + (N : \u211d)) (a + (N : \u211d) + 1))\n \u2264 A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3)\n + A0count * Real.log (|a + (N : \u211d)| + 3) :=\n add_le_add ih hwin\n linarith [hsum, hle1, hle2]\n\n/-- The dyadic-interval count: Ncount(a, b] \u2264 A\u2080\u00b7(b\u2212a+1)\u00b7log(b+4) for\n0 \u2264 a \u2264 b (the unit-window chain + the ceil cover). -/\nlemma Ncount_le_of_interval {a b : \u211d} (ha : 0 \u2264 a) (hab : a \u2264 b) :\n (Zeta23.Ncount a b : \u211d) \u2264 A0count * (b - a + 1) * Real.log (b + 4) := by\n set N : \u2115 := \u2308b - a\u2309\u208a with hN\n have hNb : b \u2264 a + (N : \u211d) := by\n have h := Nat.le_ceil (b - a)\n rw [\u2190 hN] at h\n have h2 : (b - a : \u211d) \u2264 (N : \u211d) := h\n linarith\n have hsub : Zeta23.zerosIn a b \u2286 Zeta23.zerosIn a (a + (N : \u211d)) := by\n intro \u03c1 h\u03c1\n refine \u27e8h\u03c1.1, h\u03c1.2.1, ?_\u27e9\n exact h\u03c1.2.2.trans hNb\n have hle : Zeta23.Ncount a b \u2264 Zeta23.Ncount a (a + (N : \u211d)) := by\n rw [Zeta23.Ncount, Zeta23.Ncount]\n rw [finsum_mem_eq_finite_toFinset_sum _ (Zeta23.zerosIn_finite a b),\n finsum_mem_eq_finite_toFinset_sum _ (Zeta23.zerosIn_finite a (a + (N : \u211d)))]\n apply Finset.sum_le_sum_of_subset_of_nonneg\n \u00b7 intro \u03c1 h\u03c1\n rw [Set.Finite.mem_toFinset] at h\u03c1 \u22a2\n exact hsub h\u03c1\n \u00b7 intro \u03c1 _ _\n exact Nat.cast_nonneg _\n have hchain := Ncount_chain_le a N\n have hNle : (N : \u211d) \u2264 b - a + 1 := by\n have h := Nat.ceil_lt_add_one (sub_nonneg.mpr hab)\n rw [\u2190 hN] at h\n have h2 : ((N : \u211d)) < b - a + 1 := by exact_mod_cast h\n linarith\n have hlogle : Real.log (|a| + (N : \u211d) + 3) \u2264 Real.log (b + 4) := by\n apply Real.log_le_log (by positivity)\n rw [abs_of_nonneg ha]\n linarith\n calc (Zeta23.Ncount a b : \u211d)\n \u2264 (Zeta23.Ncount a (a + (N : \u211d)) : \u211d) := by exact_mod_cast hle\n _ \u2264 A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3) := hchain\n _ \u2264 A0count * (b - a + 1) * Real.log (b + 4) := by\n have hlogpos : (0 : \u211d) \u2264 Real.log (b + 4) := by\n apply Real.log_nonneg; linarith\n have h1 : A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3)\n \u2264 A0count * (N : \u211d) * Real.log (b + 4) :=\n mul_le_mul_of_nonneg_left hlogle (mul_nonneg A0count_pos.le (Nat.cast_nonneg N))\n have h2 : A0count * (N : \u211d) * Real.log (b + 4)\n \u2264 A0count * (b - a + 1) * Real.log (b + 4) := by\n apply mul_le_mul_of_nonneg_right _ hlogpos\n nlinarith [A0count_pos, hNle, sub_nonneg.mpr hab]\n exact h1.trans h2\n\n/-! ## 2. The Dirichlet bound -/\n\n/-- The Dirichlet majorant constant: the absolute sum of the von\nMangoldt L-series terms at s = 2 (summable since 2 > 1). -/\ndef dirichletC2 : \u211d :=\n \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016\n\n/-- \u2016\u03b6\u2032/\u03b6 s\u2016 \u2264 C\u2082 for re s \u2265 2 (the Dirichlet-series majorant:\n\u2212\u03b6\u2032/\u03b6 = LSeries \u039b for re > 1, termwise \u2264 the s = 2 sum). -/\nlemma norm_logDeriv_zeta_le_dirichlet {s : \u2102} (hs : 2 \u2264 s.re) :\n \u2016logDeriv riemannZeta s\u2016 \u2264 dirichletC2 := by\n have hs1 : (1 : \u211d) < s.re := by linarith\n have h1 : -logDeriv riemannZeta s\n = LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s := by\n have h2 := ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs1\n rw [logDeriv, Pi.div_apply, h2]\n ring\n have hsum2 : Summable (fun n : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n have hsumS : Summable (fun n : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt hs1\n have hle : \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s\u2016\n \u2264 dirichletC2 := by\n show \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016 \u2264 _\n calc \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016\n \u2264 \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016 :=\n norm_tsum_le_tsum_norm hsumS\n _ \u2264 \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016 :=\n Summable.tsum_le_tsum (fun n => LSeries.norm_term_le_of_re_le_re _ (by\n simp\n exact hs) n) hsumS hsum2\n _ = dirichletC2 := rfl\n calc \u2016logDeriv riemannZeta s\u2016\n = \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s\u2016 := by\n rw [\u2190 h1, norm_neg]\n _ \u2264 dirichletC2 := hle\n\n/-! ## 3. The tsum split + the generalized interval count + the low-zero\nconstant -/\n\n/-- Splitting a summable real tsum over a finset:\n\u2211' f = \u2211_{i \u2208 s} f i + \u2211' (if i \u2208 s then 0 else f i). -/\nlemma tsum_split_finset {\u03b9 : Type*} [DecidableEq \u03b9] {f : \u03b9 \u2192 \u211d} (hf : Summable f)\n (s : Finset \u03b9) :\n \u2211' i, f i = \u2211 i \u2208 s, f i + \u2211' i, (if i \u2208 s then 0 else f i) := by\n classical\n have h1 : Summable (fun i => if i \u2208 s then f i else 0) := by\n apply Summable.of_norm_bounded hf.norm\n intro i\n by_cases hi : i \u2208 s <;> simp [hi]\n have h2 : Summable (fun i => if i \u2208 s then 0 else f i) := by\n apply Summable.of_norm_bounded hf.norm\n intro i\n by_cases hi : i \u2208 s <;> simp [hi]\n have h3 : \u2211' i, f i\n = \u2211' i, ((if i \u2208 s then f i else 0) + (if i \u2208 s then 0 else f i)) := by\n apply tsum_congr\n intro i\n by_cases hi : i \u2208 s <;> simp [hi]\n rw [h3, Summable.tsum_add h1 h2]\n congr 1\n rw [tsum_eq_sum (s := s) (fun b hb => if_neg hb)]\n exact Finset.sum_congr rfl (fun b hb => if_pos hb)\n\n/-- The generalized dyadic-interval count (both signs):\nNcount(a, b] \u2264 A\u2080\u00b7(b\u2212a+1)\u00b7log(3\u00b7max|a||b| + 5). -/\nlemma Ncount_le_of_interval_gen {a b : \u211d} (hab : a \u2264 b) :\n (Zeta23.Ncount a b : \u211d)\n \u2264 A0count * (b - a + 1) * Real.log (3 * max |a| |b| + 5) := by\n set N : \u2115 := \u2308b - a\u2309\u208a with hN\n have hNb : b \u2264 a + (N : \u211d) := by\n have h := Nat.le_ceil (b - a)\n rw [\u2190 hN] at h\n linarith\n have hsub : Zeta23.zerosIn a b \u2286 Zeta23.zerosIn a (a + (N : \u211d)) := by\n intro \u03c1 h\u03c1\n exact \u27e8h\u03c1.1, h\u03c1.2.1, h\u03c1.2.2.trans hNb\u27e9\n have hle : Zeta23.Ncount a b \u2264 Zeta23.Ncount a (a + (N : \u211d)) := by\n rw [Zeta23.Ncount, Zeta23.Ncount]\n rw [finsum_mem_eq_finite_toFinset_sum _ (Zeta23.zerosIn_finite a b),\n finsum_mem_eq_finite_toFinset_sum _ (Zeta23.zerosIn_finite a (a + (N : \u211d)))]\n apply Finset.sum_le_sum_of_subset_of_nonneg\n \u00b7 intro \u03c1 h\u03c1\n rw [Set.Finite.mem_toFinset] at h\u03c1 \u22a2\n exact hsub h\u03c1\n \u00b7 intro \u03c1 _ _\n exact Nat.cast_nonneg _\n have hchain := Ncount_chain_le a N\n have hNle : (N : \u211d) \u2264 b - a + 1 := by\n have h := Nat.ceil_lt_add_one (sub_nonneg.mpr hab)\n rw [\u2190 hN] at h\n have h2 : ((N : \u211d)) < b - a + 1 := by exact_mod_cast h\n linarith\n have hlogle : Real.log (|a| + (N : \u211d) + 3)\n \u2264 Real.log (3 * max |a| |b| + 5) := by\n apply Real.log_le_log (by positivity)\n have hM1 : |a| \u2264 max |a| |b| := le_max_left _ _\n have hM2 : |b| \u2264 max |a| |b| := le_max_right _ _\n have hba : b - a \u2264 |b| + |a| := by\n have h1 := le_abs_self b\n have h2 : -a \u2264 |a| := by rw [\u2190 abs_neg a]; exact le_abs_self (-a)\n linarith\n nlinarith [hNle, hM1, hM2, hba, abs_nonneg a, abs_nonneg b]\n have hlogpos : (0 : \u211d) \u2264 Real.log (3 * max |a| |b| + 5) := by\n apply Real.log_nonneg\n have h1 : (0 : \u211d) \u2264 max |a| |b| := le_trans (abs_nonneg a) (le_max_left _ _)\n linarith\n calc (Zeta23.Ncount a b : \u211d)\n \u2264 (Zeta23.Ncount a (a + (N : \u211d)) : \u211d) := by exact_mod_cast hle\n _ \u2264 A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3) := hchain\n _ \u2264 A0count * (b - a + 1) * Real.log (3 * max |a| |b| + 5) := by\n have h1 : A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3)\n \u2264 A0count * (N : \u211d) * Real.log (3 * max |a| |b| + 5) :=\n mul_le_mul_of_nonneg_left hlogle (mul_nonneg A0count_pos.le (Nat.cast_nonneg N))\n have h2 : A0count * (N : \u211d) * Real.log (3 * max |a| |b| + 5)\n \u2264 A0count * (b - a + 1) * Real.log (3 * max |a| |b| + 5) := by\n apply mul_le_mul_of_nonneg_right _ hlogpos\n nlinarith [A0count_pos, hNle, sub_nonneg.mpr hab]\n exact h1.trans h2\n\n/-- The low-zero finset: nontrivial zeros with \u2016\u03c1\u2016 \u2264 3. -/\ndef lowZeros : Finset {\u03c1 : \u2102 // IsNontrivialZero \u03c1} :=\n (show {\u03c1 : {\u03c1 // IsNontrivialZero \u03c1} | \u2016(\u03c1 : \u2102)\u2016 \u2264 3}.Finite from\n (finite_subtype_norm_lt 4).subset\n (fun \u03c1 h\u03c1 => lt_of_le_of_lt (show \u2016(\u03c1 : \u2102)\u2016 \u2264 3 from h\u03c1) (by norm_num))).toFinset\n\n/-- The low-zero symbolic constant (a fixed finite sum of fixed positive\nreals; \u2016\u03c1\u2016 > 0 for nontrivial \u03c1 since re \u03c1 > 0). -/\ndef lowZeroConst : \u211d :=\n \u2211 \u03c1 \u2208 lowZeros, (zeroMult (\u03c1 : \u2102) : \u211d) * (1 + 1 / \u2016(\u03c1 : \u2102)\u2016)\n\nlemma lowZeroConst_nonneg : 0 \u2264 lowZeroConst :=\n Finset.sum_nonneg fun _\u03c1 _ => mul_nonneg (Nat.cast_nonneg _)\n (add_nonneg one_pos.le (div_nonneg one_pos.le (norm_nonneg _)))\n\n/-! ## 4. The far-tail bound -/\n\n/-- The dyadic log series closed form:\n\u2211' j, ((j+4)\u00b7log 2 + log X)/2^j = 10\u00b7log 2 + 2\u00b7log X. -/\nlemma tsum_dyadic_log (X : \u211d) :\n \u2211' j : \u2115, ((j + 4) * Real.log 2 + Real.log X) / (2 : \u211d) ^ j\n = 10 * Real.log 2 + 2 * Real.log X := by\n have hgeom2H : Summable (fun j : \u2115 => ((1 : \u211d) / 2) ^ j) := summable_geometric_two\n have hgeom2 : \u2211' j : \u2115, ((1 : \u211d) / 2) ^ j = 2 := tsum_geometric_two\n have hlinH := hasSum_coe_mul_geometric_of_norm_lt_one (r := (1 : \u211d) / 2) (by norm_num)\n have hlin : \u2211' j : \u2115, (j : \u211d) * ((1 : \u211d) / 2) ^ j = 2 := by\n have h := hlinH.tsum_eq\n norm_num at h\n exact h\n have hsplit : (fun j : \u2115 => ((j + 4) * Real.log 2 + Real.log X) / (2 : \u211d) ^ j)\n = fun j : \u2115 => Real.log 2 * ((j : \u211d) * ((1 : \u211d) / 2) ^ j)\n + (4 * Real.log 2 + Real.log X) * ((1 : \u211d) / 2) ^ j := by\n funext j\n have hj : (2 : \u211d) ^ j \u2260 0 := pow_ne_zero _ two_ne_zero\n rw [one_div_pow]\n field_simp\n ring\n rw [hsplit, Summable.tsum_add (hlinH.summable.mul_left _) (hgeom2H.mul_left _)]\n rw [tsum_mul_left, tsum_mul_left, hlin, hgeom2]\n ring\n\n/-- log 2 \u2264 1 (since 2 \u2264 e). -/\nlemma log_two_le_one : Real.log 2 \u2264 1 := by\n rw [show (1 : \u211d) = Real.log (Real.exp 1) by rw [Real.log_exp]]\n apply Real.log_le_log (by norm_num)\n have h := Real.exp_one_gt_d9\n linarith\n\n/-- For X \u2265 200: (4A\u2080/X)\u00b7(10\u00b7log 2 + 2\u00b7log X) \u2264 16\u00b7A\u2080\u00b7log X / X. -/\nlemma dyadic_tail_constant {X : \u211d} (hX : 200 \u2264 X) :\n (4 * A0count / X) * (10 * Real.log 2 + 2 * Real.log X)\n \u2264 16 * A0count * Real.log X / X := by\n have hX0 : (0 : \u211d) < X := by linarith\n have hlogX : 5 \u2264 Real.log X := by\n rw [show (5 : \u211d) = Real.log (Real.exp 5) by rw [Real.log_exp]]\n apply Real.log_le_log (Real.exp_pos _)\n have h1 : Real.exp 5 = (Real.exp 1) ^ 5 := by\n rw [\u2190 Real.exp_nat_mul]\n norm_num\n have h2 := Real.exp_one_lt_d9.le\n have h3 : (Real.exp 1) ^ 5 \u2264 (2.7182818286 : \u211d) ^ 5 :=\n pow_le_pow_left\u2080 (Real.exp_pos 1).le h2 5\n have h4 : (2.7182818286 : \u211d) ^ 5 \u2264 200 := by norm_num\n linarith [h1, h3, h4]\n have hlog2 := log_two_le_one\n have hA0 : (0 : \u211d) \u2264 4 * A0count / X :=\n div_nonneg (mul_nonneg (by norm_num) A0count_pos.le) hX0.le\n have h1 : 10 * Real.log 2 + 2 * Real.log X \u2264 4 * Real.log X := by linarith\n calc (4 * A0count / X) * (10 * Real.log 2 + 2 * Real.log X)\n \u2264 (4 * A0count / X) * (4 * Real.log X) := mul_le_mul_of_nonneg_left h1 hA0\n _ = 16 * A0count * Real.log X / X := by ring\n\n/-- The dyadic class of a zero relative to scale X:\nNat.log 2 \u230a|im \u03c1|/X\u230b\u208a, so 2^j\u00b7X \u2264 |im \u03c1| < 2^{j+1}\u00b7X when |im \u03c1| \u2265 X. -/\ndef dyadClass (X : \u211d) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) : \u2115 :=\n Nat.log 2 \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a\n\nlemma dyadClass_lower {X : \u211d} (hX : 0 < X) {\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}}\n (h\u03c1 : X \u2264 |(\u03c1 : \u2102).im|) :\n (2 : \u211d) ^ dyadClass X \u03c1 * X \u2264 |(\u03c1 : \u2102).im| := by\n have hfl : \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a \u2260 0 := by\n rw [Ne, Nat.floor_eq_zero]\n push Not\n have h1 : (1 : \u211d) \u2264 |(\u03c1 : \u2102).im| / X := (le_div_iff\u2080 hX).mpr (by linarith)\n linarith\n have h2 := Nat.pow_log_le_self 2 hfl\n have h3 : ((2 ^ dyadClass X \u03c1 : \u2115) : \u211d) \u2264 \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a := by exact_mod_cast h2\n have h4 : (\u230a|(\u03c1 : \u2102).im| / X\u230b\u208a : \u211d) \u2264 |(\u03c1 : \u2102).im| / X := Nat.floor_le (by positivity)\n have h5 : ((2 ^ dyadClass X \u03c1 : \u2115) : \u211d) = (2 : \u211d) ^ dyadClass X \u03c1 := by push_cast; ring\n rw [h5] at h3\n rw [le_div_iff\u2080 hX] at h4\n have h6 : (2 : \u211d) ^ dyadClass X \u03c1 * X \u2264 \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a * X :=\n mul_le_mul_of_nonneg_right h3 hX.le\n linarith\n\nlemma dyadClass_upper {X : \u211d} (hX : 0 < X) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) :\n |(\u03c1 : \u2102).im| < (2 : \u211d) ^ (dyadClass X \u03c1 + 1) * X := by\n have h2 : \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a < 2 ^ (dyadClass X \u03c1 + 1) :=\n Nat.lt_pow_succ_log_self (by norm_num) _\n have h3 : (\u230a|(\u03c1 : \u2102).im| / X\u230b\u208a : \u211d) + 1 \u2264 (2 : \u211d) ^ (dyadClass X \u03c1 + 1) := by\n have h4 : \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a + 1 \u2264 2 ^ (dyadClass X \u03c1 + 1) := h2\n have h5 : ((\u230a|(\u03c1 : \u2102).im| / X\u230b\u208a + 1 : \u2115) : \u211d) \u2264 ((2 ^ (dyadClass X \u03c1 + 1) : \u2115) : \u211d) := by\n exact_mod_cast h4\n push_cast at h5\n linarith\n have h6 : |(\u03c1 : \u2102).im| / X < (2 : \u211d) ^ (dyadClass X \u03c1 + 1) :=\n (Nat.lt_floor_add_one _).trans_le h3\n rw [div_lt_iff\u2080 hX] at h6\n linarith\n\n/-- The tail summand (if-form on the zero subtype). -/\ndef tailTerm (X : \u211d) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) : \u211d :=\n if X < |(\u03c1 : \u2102).im| then (zeroMult \u03c1 : \u211d) / (1 + ((\u03c1 : \u2102).im) ^ 2) else 0\n\nlemma tailTerm_nonneg {X : \u211d} (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) :\n 0 \u2264 tailTerm X \u03c1 := by\n by_cases h : X < |(\u03c1 : \u2102).im| <;>\n simp [tailTerm, h, div_nonneg (Nat.cast_nonneg _)\n (by positivity : (0 : \u211d) \u2264 1 + ((\u03c1 : \u2102).im) ^ 2)]\n\n/-- The tail summand is summable (dominated by 2\u00b7m/(1+\u2016\u03b3\u2016\u00b2) via\n1 + \u2016\u03b3\u2016\u00b2 \u2264 2(1 + im\u00b2)). -/\nlemma tailTerm_summable (X : \u211d) :\n Summable (tailTerm X) := by\n have hbase : Summable (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} =>\n 2 * ((zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102))))) :=\n (WeilEF.zero_sum_inv_sq zetaSeam).mul_left 2\n apply Summable.of_norm_bounded hbase\n intro \u03c1\n rw [tailTerm]\n by_cases h : X < |(\u03c1 : \u2102).im|\n \u00b7 rw [if_pos h]\n have hgam : Complex.normSq (gammaOf (\u03c1 : \u2102))\n = (\u03c1 : \u2102).im ^ 2 + (1 / 2 - (\u03c1 : \u2102).re) ^ 2 := by\n rw [Complex.normSq_apply, WeilEF.gammaOf_re, WeilEF.gammaOf_im]\n ring\n have hcmp : 1 + Complex.normSq (gammaOf (\u03c1 : \u2102)) \u2264 2 * (1 + (\u03c1 : \u2102).im ^ 2) := by\n rw [hgam]\n have hre : ((\u03c1 : \u2102).re - 1 / 2) ^ 2 \u2264 1 / 4 := by\n have h0 := \u03c1.2.2.1\n have h1 := \u03c1.2.2.2\n nlinarith [sq_nonneg ((\u03c1 : \u2102).re - 1 / 2)]\n nlinarith [sq_nonneg (\u03c1 : \u2102).im]\n have hpos1 : (0 : \u211d) < 1 + Complex.normSq (gammaOf (\u03c1 : \u2102)) := by\n have h := Complex.normSq_nonneg (gammaOf (\u03c1 : \u2102)); linarith\n have hpos2 : (0 : \u211d) < 1 + (\u03c1 : \u2102).im ^ 2 := by positivity\n have hfrac : 1 / (1 + (\u03c1 : \u2102).im ^ 2) \u2264 2 / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102))) := by\n rw [div_le_div_iff\u2080 hpos2 hpos1]\n nlinarith [hcmp]\n have hm : (0 : \u211d) \u2264 (zeroMult \u03c1 : \u211d) := Nat.cast_nonneg _\n calc \u2016(zeroMult \u03c1 : \u211d) / (1 + (\u03c1 : \u2102).im ^ 2)\u2016\n = (zeroMult \u03c1 : \u211d) / (1 + (\u03c1 : \u2102).im ^ 2) := by\n rw [Real.norm_eq_abs, abs_of_nonneg (div_nonneg (Nat.cast_nonneg _) hpos2.le)]\n _ \u2264 2 * ((zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102)))) := by\n rw [show (zeroMult \u03c1 : \u211d) / (1 + (\u03c1 : \u2102).im ^ 2)\n = (zeroMult \u03c1 : \u211d) * (1 / (1 + (\u03c1 : \u2102).im ^ 2)) from by ring]\n rw [show 2 * ((zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102))))\n = (zeroMult \u03c1 : \u211d) * (2 / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102)))) from by ring]\n exact mul_le_mul_of_nonneg_left hfrac hm\n \u00b7 rw [if_neg h, norm_zero]\n have hnn := Complex.normSq_nonneg (gammaOf (\u03c1 : \u2102))\n exact mul_nonneg (by norm_num) (div_nonneg (Nat.cast_nonneg _) (by linarith))\n\n/-- The dyadic log series is summable. -/\nlemma dyadicLog_summable (X : \u211d) :\n Summable (fun j : \u2115 => ((j + 4) * Real.log 2 + Real.log X) / (2 : \u211d) ^ j) := by\n have hlinH := hasSum_coe_mul_geometric_of_norm_lt_one (r := (1 : \u211d) / 2) (by norm_num)\n have hsplit : (fun j : \u2115 => ((j + 4) * Real.log 2 + Real.log X) / (2 : \u211d) ^ j)\n = fun j : \u2115 => Real.log 2 * ((j : \u211d) * ((1 : \u211d) / 2) ^ j)\n + (4 * Real.log 2 + Real.log X) * ((1 : \u211d) / 2) ^ j := by\n funext j\n have hj : (2 : \u211d) ^ j \u2260 0 := pow_ne_zero _ two_ne_zero\n rw [one_div_pow]\n field_simp\n ring\n rw [hsplit]\n exact (hlinH.summable.mul_left _).add (summable_geometric_two.mul_left _)\n\n/-- The dyadic fiber {dyadClass X \u03c1 = j} is finite. -/\nlemma dyadClass_fiber_finite {X : \u211d} (hX : 0 < X) (j : \u2115) :\n {\u03c1 : {\u03c1 // IsNontrivialZero \u03c1} | dyadClass X \u03c1 = j}.Finite := by\n apply (finite_subtype_norm_lt (1 + (2 : \u211d) ^ (j + 1) * X + 1)).subset\n intro \u03c1 h\u03c1\n have h\u03c1j : dyadClass X \u03c1 = j := h\u03c1\n have hup := dyadClass_upper hX \u03c1\n rw [h\u03c1j] at hup\n have hnorm : \u2016(\u03c1 : \u2102)\u2016 \u2264 |(\u03c1 : \u2102).re| + |(\u03c1 : \u2102).im| :=\n Complex.norm_le_abs_re_add_abs_im _\n have hre : |(\u03c1 : \u2102).re| \u2264 1 := by\n rw [abs_le]\n exact \u27e8by linarith [\u03c1.2.2.1], by linarith [\u03c1.2.2.2]\u27e9\n have h2pow : (0 : \u211d) \u2264 (2 : \u211d) ^ (j + 1) * X := by positivity\n show \u2016(\u03c1 : \u2102)\u2016 < 1 + (2 : \u211d) ^ (j + 1) * X + 1\n linarith\n\n/-- The fiber count: the zeros in the dyadic fiber with X < |\u03b3| have\nmultiplicity-sum \u2264 A\u2080\u00b7(2^{j+1}X+3)\u00b7log(3\u00b72^{j+1}X+5). -/\nlemma fiber_mult_count {X : \u211d} (hX : 200 \u2264 X) (j : \u2115) :\n \u2211 \u03c1 \u2208 (dyadClass_fiber_finite (by linarith : (0 : \u211d) < X) j).toFinset,\n (zeroMult (\u03c1 : \u2102) : \u211d)\n \u2264 A0count * ((2 : \u211d) ^ (j + 1) * X + 3) * Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) := by\n classical\n have hX0 : (0 : \u211d) < X := by linarith\n have h2jX : (0 : \u211d) < (2 : \u211d) ^ j * X := by positivity\n have h2j1X : (0 : \u211d) < (2 : \u211d) ^ (j + 1) * X := by positivity\n set FS := (dyadClass_fiber_finite (by linarith : (0 : \u211d) < X) j).toFinset with hFS\n have hmemFS : \u2200 \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1},\n \u03c1 \u2208 FS \u2194 dyadClass X \u03c1 = j \u2227 X < |(\u03c1 : \u2102).im| := by\n intro \u03c1\n rw [hFS, Set.Finite.mem_toFinset]\n exact Iff.rfl\n have hW1 : (Zeta23.zerosIn ((2 : \u211d) ^ j * X - 1) ((2 : \u211d) ^ (j + 1) * X)).Finite :=\n Zeta23.zerosIn_finite _ _\n have hW2 : (Zeta23.zerosIn (-((2 : \u211d) ^ (j + 1) * X)) (-((2 : \u211d) ^ j * X))).Finite :=\n Zeta23.zerosIn_finite _ _\n have himg : FS.image (Subtype.val) \u2286 hW1.toFinset \u222a hW2.toFinset := by\n intro z hz\n obtain \u27e8\u03c1, h\u03c1, rfl\u27e9 := Finset.mem_image.mp hz\n rw [hmemFS] at h\u03c1\n obtain \u27e8h\u03c1j, hgt\u27e9 := h\u03c1\n have hup : |(\u03c1 : \u2102).im| < (2 : \u211d) ^ (j + 1) * X := by\n have h := dyadClass_upper hX0 \u03c1\n rw [h\u03c1j] at h\n exact h\n have hlo : (2 : \u211d) ^ j * X \u2264 |(\u03c1 : \u2102).im| := by\n have h := dyadClass_lower hX0 (show X \u2264 |(\u03c1 : \u2102).im| from hgt.le)\n rw [h\u03c1j] at h\n exact h\n rcases le_or_gt 0 (\u03c1 : \u2102).im with him | him\n \u00b7 apply Finset.mem_union_left\n rw [Set.Finite.mem_toFinset]\n refine \u27e8\u03c1.2, ?_, ?_\u27e9\n \u00b7 rw [abs_of_nonneg him] at hlo\n linarith\n \u00b7 rw [abs_of_nonneg him] at hup\n linarith\n \u00b7 apply Finset.mem_union_right\n rw [Set.Finite.mem_toFinset]\n refine \u27e8\u03c1.2, ?_, ?_\u27e9\n \u00b7 rw [abs_of_neg him] at hup\n linarith\n \u00b7 rw [abs_of_neg him] at hlo\n linarith\n have hsum_img : \u2211 \u03c1 \u2208 FS, (zeroMult (\u03c1 : \u2102) : \u211d)\n = \u2211 z \u2208 FS.image (Subtype.val), (zeroMult z : \u211d) := by\n rw [Finset.sum_image (fun x _ y _ h => Subtype.val_injective h)]\n have hdisj : Disjoint hW1.toFinset hW2.toFinset := by\n rw [Finset.disjoint_left]\n intro z hz1 hz2\n rw [Set.Finite.mem_toFinset] at hz1 hz2\n have h1 : (2 : \u211d) ^ j * X - 1 < z.im := hz1.2.1\n have h2 : z.im \u2264 -((2 : \u211d) ^ j * X) := hz2.2.2\n have hge : (1 : \u211d) \u2264 (2 : \u211d) ^ j * X := by\n have h1le : (1 : \u211d) \u2264 (2 : \u211d) ^ j := by exact_mod_cast Nat.one_le_two_pow\n nlinarith [h1le, hX]\n linarith\n calc \u2211 \u03c1 \u2208 FS, (zeroMult (\u03c1 : \u2102) : \u211d)\n = \u2211 z \u2208 FS.image (Subtype.val), (zeroMult z : \u211d) := hsum_img\n _ \u2264 \u2211 z \u2208 hW1.toFinset \u222a hW2.toFinset, (zeroMult z : \u211d) :=\n Finset.sum_le_sum_of_subset_of_nonneg himg (fun z _ _ => Nat.cast_nonneg _)\n _ = \u2211 z \u2208 hW1.toFinset, (zeroMult z : \u211d) + \u2211 z \u2208 hW2.toFinset, (zeroMult z : \u211d) :=\n Finset.sum_union hdisj\n _ = (Zeta23.Ncount ((2 : \u211d) ^ j * X - 1) ((2 : \u211d) ^ (j + 1) * X) : \u211d)\n + (Zeta23.Ncount (-((2 : \u211d) ^ (j + 1) * X)) (-((2 : \u211d) ^ j * X)) : \u211d) := by\n rw [Zeta23.Ncount, Zeta23.Ncount, finsum_mem_eq_finite_toFinset_sum _ hW1,\n finsum_mem_eq_finite_toFinset_sum _ hW2, Nat.cast_sum, Nat.cast_sum]\n _ \u2264 A0count * ((2 : \u211d) ^ (j + 1) * X + 3) * Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) := by\n have h2jX1 : (1 : \u211d) \u2264 (2 : \u211d) ^ j * X := by\n have h1 : (1 : \u211d) \u2264 (2 : \u211d) ^ j := by exact_mod_cast Nat.one_le_two_pow\n nlinarith [h1, hX]\n have hpowX : (2 : \u211d) ^ (j + 1) * X = 2 * ((2 : \u211d) ^ j * X) := by\n rw [pow_succ']; ring\n have hlogpos : (0 : \u211d) \u2264 Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) := by\n apply Real.log_nonneg\n linarith [h2j1X]\n have h1 := Ncount_le_of_interval_gen (a := (2 : \u211d) ^ j * X - 1)\n (b := (2 : \u211d) ^ (j + 1) * X) (by linarith [hpowX, h2jX1])\n have h2 := Ncount_le_of_interval_gen (a := -((2 : \u211d) ^ (j + 1) * X))\n (b := -((2 : \u211d) ^ j * X)) (by linarith [hpowX, h2jX1])\n -- the log arguments match L = log(3\u00b72^{j+1}X + 5)\n have hlog1 : Real.log (3 * max |(2 : \u211d) ^ j * X - 1| |(2 : \u211d) ^ (j + 1) * X| + 5)\n \u2264 Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) := by\n apply Real.log_le_log (by positivity)\n have hmax : max |(2 : \u211d) ^ j * X - 1| |(2 : \u211d) ^ (j + 1) * X|\n \u2264 (2 : \u211d) ^ (j + 1) * X := by\n apply max_le\n \u00b7 rw [abs_of_nonneg (by linarith [h2jX1])]\n nlinarith [h2jX, h2j1X]\n \u00b7 rw [abs_of_nonneg h2j1X.le]\n linarith [hmax]\n have hlog2 : Real.log (3 * max |-((2 : \u211d) ^ (j + 1) * X)| |-((2 : \u211d) ^ j * X)| + 5)\n \u2264 Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) := by\n apply Real.log_le_log (by positivity)\n have hmax : max |-((2 : \u211d) ^ (j + 1) * X)| |-((2 : \u211d) ^ j * X)|\n \u2264 (2 : \u211d) ^ (j + 1) * X := by\n apply max_le\n \u00b7 rw [abs_neg, abs_of_nonneg h2j1X.le]\n \u00b7 rw [abs_neg, abs_of_nonneg h2jX.le]\n nlinarith [h2jX, h2j1X]\n linarith [hmax]\n -- the lengths: b\u2212a+1 = 2^jX + 2 and 2^jX + 1\n have hlen1 : (2 : \u211d) ^ (j + 1) * X - ((2 : \u211d) ^ j * X - 1) + 1\n = (2 : \u211d) ^ j * X + 2 := by\n have hpow : (2 : \u211d) ^ (j + 1) = 2 * (2 : \u211d) ^ j := by rw [pow_succ']\n rw [hpow]\n ring\n have hlen2 : -((2 : \u211d) ^ j * X) - (-((2 : \u211d) ^ (j + 1) * X)) + 1\n = (2 : \u211d) ^ j * X + 1 := by\n have hpow : (2 : \u211d) ^ (j + 1) = 2 * (2 : \u211d) ^ j := by rw [pow_succ']\n rw [hpow]\n ring\n rw [hlen1] at h1\n rw [hlen2] at h2\n -- assemble: A\u2080(2^jX+2)L + A\u2080(2^jX+1)L = A\u2080(2^{j+1}X+3)L\n have hA0 := A0count_pos.le\n have h1' : (Zeta23.Ncount ((2 : \u211d) ^ j * X - 1) ((2 : \u211d) ^ (j + 1) * X) : \u211d)\n \u2264 A0count * ((2 : \u211d) ^ j * X + 2) * Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) :=\n h1.trans (mul_le_mul_of_nonneg_left hlog1 (by positivity))\n have h2' : (Zeta23.Ncount (-((2 : \u211d) ^ (j + 1) * X)) (-((2 : \u211d) ^ j * X)) : \u211d)\n \u2264 A0count * ((2 : \u211d) ^ j * X + 1) * Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) :=\n h2.trans (mul_le_mul_of_nonneg_left hlog2 (by positivity))\n have hpow : (2 : \u211d) ^ (j + 1) * X = 2 * ((2 : \u211d) ^ j * X) := by rw [pow_succ']; ring\n rw [hpow] at h1' h2' \u22a2\n linarith [h1', h2', hA0, hlogpos]\n\nend NguyenRH1\n\nend\n",
"structuredPatch": [
{
"oldStart": 515,
"oldLines": 7,
"newStart": 515,
"newLines": 9,
"lines": [
" /-- The fiber count: the zeros in the dyadic fiber with X < |\u03b3| have",
" multiplicity-sum \u2264 A\u2080\u00b7(2^{j+1}X+3)\u00b7log(3\u00b72^{j+1}X+5). -/",
" lemma fiber_mult_count {X : \u211d} (hX : 200 \u2264 X) (j : \u2115) :",
"- \u2211 \u03c1 \u2208 (dyadClass_fiber_finite (by linarith : (0 : \u211d) < X) j).toFinset,",
"+ \u2211 \u03c1 \u2208 ((dyadClass_fiber_finite (by linarith : (0 : \u211d) < X) j).inter",
"+ {\u03c1 : {\u03c1 // IsNontrivialZero \u03c1} | X < |(\u03c1 : \u2102).im|}",
"+ (Set.Finite.subset (Set.finite_lt_nat' ...))).toFinset,",
" (zeroMult (\u03c1 : \u2102) : \u211d)",
" \u2264 A0count * ((2 : \u211d) ^ (j + 1) * X + 3) * Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) := by",
" classical"
]
}
],
"userModified": false,
"replaceAll": false
}
raw content_json (database row)
[{"type":"thinking","thinking":"Wait — several concerns in iteratedDerivWithin_dpsiTermC:\n\n1. The `rw [show ... from rfl]` lines are pointless (rfl identities don't rewrite anything meaningful). The issue: the goal after `rw [heq]` — heq's RHS is `(fun s => 1/(↑m+1)) + fun s => -(1/(s+↑m+1))` — wait I wrote heq's RHS as `(fun s : ℂ => 1 / ((m : ℂ) + 1)) + fun s : ℂ => -(1 / (s + ↑m + 1))` — that's `(lambda) + (lambda)` — HAdd of two lambdas — which is defeq to the Pi.add form `(fun s => ...) + (fun s => ...)`? — `(fun s => 1/(↑m+1)) + (fun s => -(1/(s+↑m+1)))` — HAdd.hAdd of the two lambda TERMS — NOT the same as Pi.add's application `(F + G)` — iteratedDeriv_add's LHS is `iteratedDeriv n (f + g) x` with `f + g` = Pi.add — HAdd.hAdd F G — and my lambda-sum `F + G` is also HAdd.hAdd F G — the Pi.instAdd's HAdd — same ✓. So the `show ... from rfl` line is vacuous — remove it. And the iteratedDeriv_add should apply directly.\n\n2. The `rw [show (fun s : ℂ => s + ↑m + 1) = fun s : ℂ => s + (↑m + 1) from rfl] at *` — also vacuous/rfl — the association: my zpow lemma's conclusion has (s + c) with c := ↑m + 1 — so the base is `s + (↑m + 1)` — but the target form has `(s + ↑m + 1)` — `(s + ↑m) + 1` vs `s + (↑m + 1)` — DIFFERENT association — NOT defeq? — add_assoc: (a+b)+c = a+(b+c) — they ARE propositionally equal via add_assoc — not rfl. So the base in the zpow-lemma call's conclusion is `s + (↑m + 1)` but my lemma's stated conclusion has `(s + ↑m + 1)` — mismatch — fix: change the lemma's stated conclusion to use `s + (↑m + 1)`? — or call the zpow lemma with c := (↑m + 1) and then the conclusion's base is (s + (↑m+1)) — then convert via add_assoc — `rw [show (s : ℂ) + (↑m + 1) = s + ↑m + 1 from by ring]`? — direction: s + (↑m+1) = (s+↑m)+1 by (add_assoc).symm — hmm add_assoc : a+b+c = a+(b+c) — so (s+↑m)+1 = s+(↑m+1) is add_assoc and s+(↑m+1) = (s+↑m)+1 is add_assoc.symm — rw [add_assoc] turns s+(↑m+1) into (s+↑m)+1 ✓.\n\nLet me restructure the ending of iteratedDerivWithin_dpsiTermC:\n```lean\n rw [heq]\n have hcf : ContDiffAt ℂ k (fun s : ℂ => 1 / ((m : ℂ) + 1)) s := contDiff_const.contDiffAt\n have hcg : ContDiffAt ℂ k (fun s : ℂ => -(1 / (s + ↑m + 1))) s := ...\n rw [iteratedDeriv_add hcf hcg]\n rw [iteratedDeriv_const, if_neg (by omega : k ≠ 0)]\n have h4 := iteratedDeriv_neg_one_div_add_const k (↑m + 1) (c := (↑m : ℂ) + 1) (by ...)\n -- h4 : iteratedDeriv k (fun s => -(1 / (s + (↑m+1)))) s = −(−1)^k·k!·(s + (↑m+1))^{−(k+1)}\n ...\n```\nHmm — the function in hcg/h4 is fun s => -(1/(s + ↑m + 1)) — with base (s + ↑m + 1) — and the zpow lemma's function is fun s => -(1/(s + c)) with c := (↑m+1) — base (s + (↑m+1)) — the functions differ associationally: fun s => -(1/(s + ↑m + 1)) vs fun s => -(1/(s + (↑m+1))) — defeq? (s+↑m)+1 vs s+(↑m+1) — propositionally equal via add_assoc, not defeq — so the function equality needs funext+ring. Let me handle with a show:\n```lean\n have h4 : iteratedDeriv k (fun s : ℂ => -(1 / (s + ↑m + 1))) s =\n -((-1 : ℂ)) ^ k * (k ! : ℂ) * (s + ↑m + 1) ^ (-(k : ℤ) - 1) := by\n have h5 : (fun s : ℂ => -(1 / (s + ↑m + 1))) = fun s : ℂ => -(1 / (s + ((m : ℂ) + 1))) := by\n funext s\n rw [add_assoc]\n rw [h5]\n rw [iteratedDeriv_neg_one_div_add_const k ((m : ℂ) + 1) ?_]\n · rw [add_assoc] -- hmm — the conclusion's base s + (↑m+1) → s+↑m+1 — wait direction\n · -- s + (↑m+1) ≠ 0 from hsm: s + ↑m + 1 ≠ 0 — same value: add_assoc\n rw [← add_assoc] -- hmm\n exact hsm\n```\ncareful: the side goal: s + (↑m + 1) ≠ 0 — from hsm : s + ↑m + 1 ≠ 0 — add_assoc.symm... — `rwa [add_assoc]`? — the side goal s + (↑m+1) ≠ 0 — rw [add_assoc] turns it into (s+↑m)+1 ≠ 0 — is that hsm's form? hsm : s + ↑m + 1 ≠ 0 — which parses as (s + ↑m) + 1 ≠ 0 ✓ — so rw [add_assoc] at the side goal makes it match hsm ✓ then exact hsm. And h4's conclusion base: (s + (↑m+1))^{...} — I want (s + ↑m + 1) — rw [add_assoc] turns s+(↑m+1) → s+↑m+1 ✓ — hmm direction: add_assoc : (a+b)+c = a+(b+c) — rw [add_assoc] rewrites (a+b)+c → a+(b+c) — I want the reverse: (s+↑m)+1 → s+(↑m+1) — that's ← add_assoc. And the side-goal s + (↑m+1) ≠ 0 → (s+↑m)+1 ≠ 0 is add_assoc forward. Ugh — let me just be careful:\n- h4's conclusion after the zpow lemma: −(−1)^k·k!·(s + (↑m+1))^{−(k+1)} — I want to display it as (s + ↑m + 1)^{−(k+1)}: the base s + (↑m+1) → (s+↑m)+1 — via `rw [← add_assoc]`?? — no: add_assoc : (a+b)+c = a+(b+c) — the LHS form is (s+↑m)+1 — hmm — I have s + (↑m+1) and want s + ↑m + 1 = (s+↑m)+1 — so rewrite s+(↑m+1) → (s+↑m)+1: that's ← add_assoc (since add_assoc says (s+↑m)+1 = s+(↑m+1)) ✓ so rw [← add_assoc] on h4's conclusion. But rw [← add_assoc] might hit other additions — the conclusion has several +'s — risky. Use `show`:\n```lean\n rw [h5]\n rw [iteratedDeriv_neg_one_div_add_const k ((m : ℂ) + 1) (by rw [add_assoc]; exact hsm)]\n rw [← add_assoc]\n```\nHmm — `rw [add_assoc]` on the side goal s + (↑m+1) ≠ 0: add_assoc forward turns s+(↑m+1) into (s+↑m)+1 ✓ matches hsm ✓. And the final `rw [← add_assoc]` on the main goal — the conclusion after the zpow-lemma rewrite: −(−1)^k·↑k!·(s+(↑m+1))^(−(k:ℤ)−1) — the base s + (↑m+1) — ← add_assoc rewrites it to (s+↑m)+1 ✓ — other additions: the exponent −(k:ℤ)−1 — contains subtraction not add ✓; the (↑m+1) inside the base is GONE (became (s+↑m)+1) — hmm — careful — ← add_assoc : a+(b+c) → (a+b)+c — the goal might have other a+(b+c) patterns — the exponent −(k:ℤ)−1 is a subtraction ✓; the (↑m+1) — wait after the rewrite the base becomes (s+↑m)+1 — and there's no other a+(b+c) shape... the k!'s etc no. Should be OK-ish; if it hits the wrong one, use show.\n\nActually — simplest robust: end with `show`ing the target and `ring_nf`-proving the whole equation? No — the zpow atom blocks ring. Alternative: make the FINAL statement use the base `s + (↑m + 1)` — i.e., state iteratedDerivWithin_dpsiTermC's conclusion with `(s + (↑m + 1))`?? — but the downstream (the sum at 1/2) computes with (1/2 + ↑m + 1) — association normalization needed SOMEWHERE. Let me just leave the lemma's conclusion as `(s + ↑m + 1)` and handle the association by `show`:\n\nAfter all the rewrites, the goal is:\n 0 + (−(−1)^k·↑k!·(s + (↑m+1))^{−(k:ℤ)−1}) = −(−1)^k·↑k!·(s+↑m+1)^(−(k:ℤ)−1)\n — zero_add first: then −(−1)^k·↑k!·(s+(↑m+1))^(...) = −(−1)^k·↑k!·(s+↑m+1)^(...) — the bases differ by association — `show` the RHS with the (s+(↑m+1)) form? no — the GOAL is the full equation — `congr 1`? — the two sides are products of atoms (−(−1)^k, ↑k!, the zpow) — congr 1 recursively splits into atom equalities — the zpow atom equality: (s+(↑m+1))^(−(k:ℤ)−1) = (s+↑m+1)^(−(k:ℤ)−1) — by congr 1 → s+(↑m+1) = s+↑m+1 → add_assoc ✓. So end with:\n```lean\n rw [zero_add] -- if the 0 + is there\n congr 3 -- or congr 1 repeatedly — splits HMul chains: a*b*c = a'*b'*c' → a=a', b=b', c=c' — congr 2 maybe\n rw [add_assoc]\n```\nHmm — `congr 3` might overshoot (splitting into the exponent pieces etc.). Let me use: `congr 1; congr 1; rw [add_assoc]`... — fragile. SAFEST: keep the lemma statement's base as `(s + ↑m + 1)` and make the zpow-lemma application produce exactly that by choosing its function input as `fun s => -(1 / (s + ↑m + 1))` — i.e., prove the one-div lemma with the base as-written `s + c` and apply with c := ↑m + 1 — then the conclusion's base is `s + (↑m + 1)` — the association difference is INSIDE the base atom — Lean sees (s + (↑m+1)) vs (s + ↑m + 1) as different atoms. So the mismatch is unavoidable at the atom level — must add_assoc somewhere. Fine — end with:\n```lean\n simp only [zero_add]\n rw [← add_assoc] -- no wait — I have s + (↑m+1), want (s+↑m)+1: ← add_assoc ✓ — but which occurrence — the goal after everything: −(−1)^k·↑k!·(s+(↑m+1))^(−(k:ℤ)−1) = −(−1)^k·↑k!·(s+↑m+1)^(−(k:ℤ)−1) — hmm — actually WAIT: after `rw [iteratedDeriv_neg_one_div_add_const ...]` the goal's LHS (the summand's iterated deriv) BECOMES the closed form — the goal is then:\n (0 + −(−1)^k·↑k!·(s + (↑m+1))^(−(k:ℤ)−1)) = −(−1)^k·↑k!·(s + ↑m + 1)^(−(k:ℤ)−1)\n rw [zero_add] -- LHS → the closed form\n -- now the only difference: the base association\n rw [add_assoc] -- (s+↑m)+1 → s+(↑m+1)?? — the RHS's base — hmm — add_assoc forward turns (s+↑m)+1 into s+(↑m+1) — the RHS's base is (s+↑m)+1 = displayed `s + ↑m + 1` — so rw [add_assoc] rewrites the RHS's base → s+(↑m+1) — matching the LHS ✓ rfl closed by rw.\n```\nSo: rw [zero_add, add_assoc]. The add_assoc rewrites the FIRST (a+b)+c pattern — the RHS's base (s+↑m)+1 ✓... — but is there an earlier (a+b)+c in the goal? The LHS after zero_add: −(−1)^k·↑k!·(s+(↑m+1))^(−(k:ℤ)−1) — patterns (a+b)+c: (−(−1)^k·↑k!)·(zpow) — the multiplications not additions ✓; the exponent −(k:ℤ)−1 — subtraction ✓; (s+(↑m+1)) — the base: s + (↑m+1) — a+(b+c) form — add_assoc forward would rewrite THIS first if it comes first in the traversal!! — the goal LHS is −(−1)^k·↑k!·(s+(↑m+1))^(...) and RHS is −(−1)^k·↑k!·((s+↑m)+1)^(...) — the traversal order (outermost-first, left-to-right): LHS and RHS both have the same head Eq, then the LHS's product chain... — the first (a+b)+c occurrence scanning the goal: Eq LHS RHS — LHS: the product — contains (s + (↑m+1)) — that's a+(b+c) — add_assoc FORWARD matches a+(b+c) → (a+b)+c — rewriting the LHS's base to (s+↑m)+1 ✓ THEN both sides have (s+↑m)+1 ✓ rfl ✓. Hmm — so rw [add_assoc] forward on the LHS base: s+(↑m+1) → (s+↑m)+1 ✓ then goal LHS = RHS ✓. Wait — does rw [add_assoc] rewrite ALL matches of the first-found pattern or just the first? rw rewrites ALL instances of the pattern-instance (the first matched pattern determines the metavars, then all occurrences of that instance). First match: scanning the Eq goal — LHS first — finds s + (↑m+1) (a := s, b := ↑m, c := 1) — rewrites all occurrences of s + (↑m + 1) → (s + ↑m) + 1 — the LHS's base ✓ (the RHS has (s+↑m)+1 — not of the form a+(b+c) — untouched) — result: both sides identical ✓.\n\nOK — let me apply this ending fix. Let me view the current end of the lemma and fix.","signature":""},{"type":"text","text":"Let me fix the ending of the summand-derivative lemma."},{"type":"tool_use","id":"Edit_409","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigamma.lean","old_string":" rw [heq]\n have hcf : ContDiffAt ℂ k (fun s : ℂ => 1 / ((m : ℂ) + 1)) s := contDiff_const.contDiffAt\n have hcg : ContDiffAt ℂ k (fun s : ℂ => -(1 / (s + ↑m + 1))) s := by\n have h2 : AnalyticAt ℂ (fun s : ℂ => s + ↑m + 1) s :=\n (analyticAt_id.add analyticAt_const).add analyticAt_const\n have h3 : AnalyticAt ℂ (fun s : ℂ => 1 / (s + ↑m + 1)) s :=\n analyticAt_const.div h2 hsm\n exact h3.neg.contDiffAt\n rw [show ((fun s : ℂ => 1 / ((m : ℂ) + 1)) + fun s : ℂ => -(1 / (s + ↑m + 1))) =\n (fun s : ℂ => 1 / ((m : ℂ) + 1)) + (fun s : ℂ => -(1 / (s + ↑m + 1))) from rfl]\n rw [iteratedDeriv_add hcf hcg]\n rw [iteratedDeriv_const, if_neg (by omega : k ≠ 0)]\n rw [show (fun s : ℂ => s + ↑m + 1) = fun s : ℂ => s + (↑m + 1) from rfl] at *\n rw [iteratedDeriv_neg_one_div_add_const k (↑m + 1) (by simpa using hsm)]\n simp [add_assoc]\n\nend NguyenRH1","new_string":" rw [heq]\n have hcf : ContDiffAt ℂ k (fun s : ℂ => 1 / ((m : ℂ) + 1)) s := contDiff_const.contDiffAt\n have hcg : ContDiffAt ℂ k (fun s : ℂ => -(1 / (s + ↑m + 1))) s := by\n have h2 : AnalyticAt ℂ (fun s : ℂ => s + ↑m + 1) s :=\n (analyticAt_id.add analyticAt_const).add analyticAt_const\n have h3 : AnalyticAt ℂ (fun s : ℂ => 1 / (s + ↑m + 1)) s :=\n analyticAt_const.div h2 hsm\n exact h3.neg.contDiffAt\n rw [iteratedDeriv_add hcf hcg]\n rw [iteratedDeriv_const, if_neg (by omega : k ≠ 0)]\n have h4 : iteratedDeriv k (fun s : ℂ => -(1 / (s + ↑m + 1))) s =\n -((-1 : ℂ)) ^ k * (k ! : ℂ) * (s + ↑m + 1) ^ (-(k : ℤ) - 1) := by\n have h5 : (fun s : ℂ => -(1 / (s + ↑m + 1))) =\n fun s : ℂ => -(1 / (s + ((m : ℂ) + 1))) := by\n funext s\n rw [add_assoc]\n rw [h5]\n rw [iteratedDeriv_neg_one_div_add_const k ((m : ℂ) + 1) (by rw [add_assoc]; exact hsm)]\n rw [← add_assoc]\n rw [h4]\n rw [zero_add]"},"extra_content":null}]