← Session 21 — Tier ii′ planning + launch: close SfBoundProp in Lean (D-064)
thinking (2105 chars)
Mathlib HAS a full RemovableSingularity.lean: `differentiableOn_update_limUnder_of_bddAbove` ✓. So the zetaA analyticity is standard.
Now I have everything needed. This is a big file to write — let me structure session 016's deliverable as ii′-1b(i) + (ii) if possible, with (iii) possibly going to session 017. Let me write `LiResidue.lean` with:
Part 1 (ii′-1b(i)): zetaA, hLi, lcoeff, ResW1 + the value theorem.
Part 2 (ii′-1b(ii)): principal-part integral.
Given the amount, I'll write Part 1 first, compile, then Part 2.
Let me write Part 1 now.
Key proofs:
1. `zetaA` := Function.update (fun w => (w - 1) * riemannZeta w) 1 1.
- `zetaA_apply (w : ℂ) (hw : w ≠ 1) : zetaA w = (w - 1) * riemannZeta w` := Function.update_of_ne hw
- `zetaA_one : zetaA 1 = 1` := Function.update_self ..
- `zetaA_analyticAt_one : AnalyticAt ℂ zetaA 1`:
- off 1: differentiable: fun w => (w−1)*riemannZeta w — differentiableAt at w ≠ 1: DifferentiableAt.mul (differentiableAt_id.sub const) (differentiableAt_riemannZeta hw) ✓.
- at 1: use the removable singularity: differentiableOn on a punctured ball + bddAbove near 1 (from the limit: (s−1)ζ(s) → 1 ⟹ bounded) ⟹ differentiableOn the update ⟹ AnalyticAt (differentiableOn at a nhd ⟹ analyticOnNhd? For ℂ, DifferentiableOn ℂ f s with s ∈ 𝓝 1 ⟹ AnalyticOnNhd? — differentiable on an open set in ℂ IS analytic: `DifferentiableOn.analyticOnNhd`? there's the theorem differentiableOn → analyticOnNhd for complex functions on open sets: `DifferentiableOn.analyticOnNhd (hd : DifferentiableOn ℂ f s) (ho : IsOpen s) : AnalyticOnNhd ℂ f s`? I believe `DifferentiableOn.analyticOnNhd` exists ✓ (holomorphic ⟺ analytic in ℂ).)
- boundedness: Tendsto (fun s => (s−1)ζ(s)) (𝓝[≠]1) (𝓝 1) ⟹ IsBoundedUnder (· ≤ ·) (𝓝[≠]1) (‖f‖) — Tendsto ⟹ bounded in a nhd: `Filter.Tendsto.isBoundedUnder...`? there's `Filter.Tendsto.norm_isBoundedUnder`? or: the removable lemma's hb argument takes BddAbove of ‖s−c‖·‖f s‖... Let me look at the exact signature of differentiableOn_update_limUnder_of_bddAbove.
Let me read RemovableSingularity.lean's exact statements.
Mathlib has full removable-singularity machinery. Let me read the exact signatures.
tool: Bash ok
input
{
"command": "sed -n '95,130p' /d/Python/Quantum/zeta-23-lean/.lake/packages/mathlib/Mathlib/Analysis/Complex/RemovableSingularity.lean",
"description": "Read removable singularity theorem signatures"
}
result 2026-08-21 20:55:28Z → 2026-08-28 23:57:52Z
rewrite -> probe.cgi (temporary) PATH_INFO : '/resources/ζ(3) — Status/' REQUEST_URI : '/resources/%CE%B6%283%29%20%E2%80%94%20Status/' SCRIPT_NAME : '/probe.cgi' QUERY_STRING : '' LANG/LC_ALL : None / None fs encoding : utf-8 PATH_INFO utf8: b'/resources/\xce\xb6(3) \xe2\x80\x94 Status/'
raw content_json (database row)
[{"type":"thinking","thinking":"Mathlib HAS a full RemovableSingularity.lean: `differentiableOn_update_limUnder_of_bddAbove` ✓. So the zetaA analyticity is standard. \n\nNow I have everything needed. This is a big file to write — let me structure session 016's deliverable as ii′-1b(i) + (ii) if possible, with (iii) possibly going to session 017. Let me write `LiResidue.lean` with:\n\nPart 1 (ii′-1b(i)): zetaA, hLi, lcoeff, ResW1 + the value theorem.\nPart 2 (ii′-1b(ii)): principal-part integral.\n\nGiven the amount, I'll write Part 1 first, compile, then Part 2.\n\nLet me write Part 1 now.\n\nKey proofs:\n1. `zetaA` := Function.update (fun w => (w - 1) * riemannZeta w) 1 1.\n - `zetaA_apply (w : ℂ) (hw : w ≠ 1) : zetaA w = (w - 1) * riemannZeta w` := Function.update_of_ne hw\n - `zetaA_one : zetaA 1 = 1` := Function.update_self ..\n - `zetaA_analyticAt_one : AnalyticAt ℂ zetaA 1`:\n - off 1: differentiable: fun w => (w−1)*riemannZeta w — differentiableAt at w ≠ 1: DifferentiableAt.mul (differentiableAt_id.sub const) (differentiableAt_riemannZeta hw) ✓.\n - at 1: use the removable singularity: differentiableOn on a punctured ball + bddAbove near 1 (from the limit: (s−1)ζ(s) → 1 ⟹ bounded) ⟹ differentiableOn the update ⟹ AnalyticAt (differentiableOn at a nhd ⟹ analyticOnNhd? For ℂ, DifferentiableOn ℂ f s with s ∈ 𝓝 1 ⟹ AnalyticOnNhd? — differentiable on an open set in ℂ IS analytic: `DifferentiableOn.analyticOnNhd`? there's the theorem differentiableOn → analyticOnNhd for complex functions on open sets: `DifferentiableOn.analyticOnNhd (hd : DifferentiableOn ℂ f s) (ho : IsOpen s) : AnalyticOnNhd ℂ f s`? I believe `DifferentiableOn.analyticOnNhd` exists ✓ (holomorphic ⟺ analytic in ℂ).)\n - boundedness: Tendsto (fun s => (s−1)ζ(s)) (𝓝[≠]1) (𝓝 1) ⟹ IsBoundedUnder (· ≤ ·) (𝓝[≠]1) (‖f‖) — Tendsto ⟹ bounded in a nhd: `Filter.Tendsto.isBoundedUnder...`? there's `Filter.Tendsto.norm_isBoundedUnder`? or: the removable lemma's hb argument takes BddAbove of ‖s−c‖·‖f s‖... Let me look at the exact signature of differentiableOn_update_limUnder_of_bddAbove.\n\nLet me read RemovableSingularity.lean's exact statements.","signature":""},{"type":"text","text":"Mathlib has full removable-singularity machinery. Let me read the exact signatures."},{"type":"tool_use","id":"Bash_189","name":"Bash","input":{"command":"sed -n '95,130p' /d/Python/Quantum/zeta-23-lean/.lake/packages/mathlib/Mathlib/Analysis/Complex/RemovableSingularity.lean","description":"Read removable singularity theorem signatures"},"extra_content":null}]