← Session 22 — ii′-1: liCoeff pairing fix + residue machinery
thinking (25949 chars)
Design note committed (62a1ddf). Now start Piece B — the ζ-piece coefficient reading. New file `LiZetaCoeff.lean`:
Contents:
1. `hLiExt` — the extension of (1 − hLi(1+s))/s to s = 0 with value −deriv hLi 1; analytic at 0.
2. The function identity s·hLiExt s = 1 − hLi(1+s).
3. The comp bridge iteratedDeriv m (hLi ∘ (1+·)) 0 = iteratedDeriv m hLi 1.
4. The Leibniz collapse.
5. Main: iteratedDeriv j hLiExt 0 = −(j! : ℂ)·lcoeff j.
Let me check the comp lemma name first: LiResidue used `iteratedDeriv_comp_sub_const` — signature: iteratedDeriv_comp_sub_const (n : ℕ) (f : ℂ → ℂ) (c : ℂ)? : iteratedDeriv n (f ∘ (· − c)) = fun x => iteratedDeriv n f (x − c)? — from A_iter's usage: congr_fun (iteratedDeriv_comp_sub_const i (fun w => w^n) (1:ℂ)) 1 : iteratedDeriv i ((fun w => w^n) ∘ (·−1)) 1 = iteratedDeriv i (fun w => w^n) (1−1)... So iteratedDeriv_comp_sub_const i f c : (iteratedDeriv i (f ∘ (· − c))) = fun x => iteratedDeriv i f (x − c) ✓.
For (1 + ·): hLi(1+s) = hLi ∘ (fun s => 1 + s) = hLi ∘ (· + 1)?? 1 + s — is there iteratedDeriv_comp_add_const : iteratedDeriv n (f ∘ (· + c)) x = iteratedDeriv n f (x + c)? Or derive from the sub version: 1 + s = s + 1 — (· + 1) = (· − (−1)) — use iteratedDeriv_comp_sub_const with c := −1: f ∘ (· − (−1)) — and (· − (−1)) = (· + 1) defeq ✓. Let me check the exact name/form of iteratedDeriv_comp_sub_const first. Also check if there's `iteratedDeriv_comp_add_const` directly.
For the analyticity of hLi on a ball around 1: need a ball where zetaA ≠ 0: zetaA_ne_zero_near_one : ∀ᶠ w in 𝓝 1, zetaA w ≠ 0 — extract a ball: Metric.eventually_nhds_iff... get ε > 0 with zetaA w ≠ 0 on ball 1 ε (punctured? at 1 zetaA 1 = 1 ≠ 0 too — the eventually is on 𝓝 1 (full) ✓ since zetaA 1 = 1 ≠ 0 and continuity ✓). On ball 1 ε: hLi analytic: hLi w = 1 − (w−1)(deriv zetaA w / zetaA w): zetaA analytic on the ball (zetaA_analyticOnNhd_univ), deriv zetaA analytic, quotient by zetaA ≠ 0 ✓. So hLi AnalyticOnNhd on the ball. Then (1 − hLi(1+s))/s differentiable for s ≠ 0 small: hLi(1+s): comp analytic at s (1+s ∈ ball). ✓
Then hLiExt := Function.update (fun s => (1 − hLi (1+s))/s) 0 (−deriv hLi 1) — wait the value: limUnder (𝓝[≠] 0) (fun s => (1−hLi(1+s))/s) = −deriv hLi 1? — the removable-singularity lemma `differentiableOn_update_limUnder_of_bddAbove` (used in zetaA_analyticAt_one) takes the update value := limUnder — so define hLiExt with value limUnder and separately prove limUnder = −deriv hLi 1. zetaA used `Function.update (fun w => (w−1)*ζ w) 1 1` with the value 1 directly + a separate hlim rewrite. Mirror: hLiExt := Function.update (fun s => (1 − hLi (1 + s)) / s) 0 (limUnder (𝓝[≠] 0) (fun s => (1 − hLi (1 + s)) / s)) — then a lemma limUnder ... = −deriv hLi 1 gives hLiExt 0 = −deriv hLi 1.
Hmm — actually let me structure it exactly like zetaA_analyticAt_one:
```lean
def hLiExt : ℂ → ℂ := Function.update (fun s => (1 - hLi (1 + s)) / s) 0 (limUnder (𝓝[≠] 0) (fun s => (1 - hLi (1 + s)) / s))
```
Wait — that's circular-ish but fine (update with the limUnder value). Actually zetaA := update ... 1 1 (explicit value 1, then proved lim = 1 separately and rw'd). For hLiExt I could put the explicit value −deriv hLi 1 and prove the limUnder equality first:
```lean
lemma hLiExt_lim : limUnder (𝓝[≠] (0 : ℂ)) (fun s => (1 - hLi (1 + s)) / s) = -deriv hLi 1 := by
-- (1 − hLi(1+s))/s = −(hLi(1+s) − hLi(1))/s → −deriv (hLi∘(1+·)) 0 = −deriv hLi 1
have hd : HasDerivAt (fun s : ℂ => hLi (1 + s)) (deriv hLi 1) 0 := by
have h1 : HasDerivAt hLi (deriv hLi 1) 1 := hLi_analyticAt_one.differentiableAt.hasDerivAt
have h2 : HasDerivAt (fun s : ℂ => 1 + s) 1 0 := by
simpa using (hasDerivAt_id (0:ℂ)).const_add 1
have h3 := h1.comp 0 h2
-- h3 : HasDerivAt (hLi ∘ (1+·)) (1 * deriv hLi 1)?? comp: HasDerivAt (hLi ∘ g) (deriv hLi (g 0) * dg) — for ℂ→ℂ→ℂ: HasDerivAt.comp (hf : HasDerivAt f f' (g x)) (hg : HasDerivAt g g' x) : HasDerivAt (f ∘ g) (f' * g')? or g' • f'? For ℂ it's mul: (f' * g')? session-016 note: "HasDerivAt.comp handles mixed fields via NormedAlgebra/IsScalarTower" — for ℂ→ℂ: HasDerivAt.comp x hf hg : HasDerivAt (f ∘ g) x (g' * f')?? order matters for noncomm — for ℂ comm either. The exact form: h1.comp 0 h2 : HasDerivAt (hLi ∘ fun s => 1 + s) (1 * deriv hLi 1)?? — comp order: h1 : HasDerivAt hLi (deriv hLi 1) (at (1+0) = 1 ✓ since g 0 = 1 + 0 = 1); h1.comp 0 h2 : HasDerivAt (hLi ∘ (fun s => 1+s)) ((deriv hLi 1) * 1) 0 — simpa to deriv hLi 1.
...
-- the slope tendsto
have hslope : Tendsto (fun s : ℂ => (hLi (1 + s) - hLi 1) / s) (𝓝[≠] 0) (𝓝 (deriv hLi 1)) := by
have := hasDerivAt_iff_tendsto_slope.mp hd
simpa [slope_fun_def_field, sub_zero] using this
-- (1 − hLi(1+s))/s = −(hLi(1+s) − hLi 1)/s on 𝓝[≠] 0: pointwise algebra + hLi_one
have hev : (fun s : ℂ => (1 - hLi (1 + s)) / s) =ᶠ[𝓝[≠] 0] (fun s => -((hLi (1 + s) - hLi 1) / s)) := by
filter_upwards [self_mem_nhdsWithin] with s hs
rw [hLi_one]; ring
rw [limUnder_congr hev] -- limUnder congr: f =ᶠ[l] g → limUnder l f = limUnder l g ✓ (`limUnder_congr`? or Filter.EventuallyEq.limUnder_eq? — there's `Filter.limUnder_congr`? hmm — `EventuallyEq.limUnder_eq`? — in LiResidue: `riemannZeta_residue_one.limUnder_eq` was used — that's Tendsto.limUnder_eq : Tendsto f l (𝓝 a) → limUnder l f = a ✓. For the congr: `limUnder_congr (h : f =ᶠ[l] g) : limUnder l f = limUnder l g`? — I believe `Filter.limUnder_congr` exists? or `EventuallyEq.limUnder_eq`? hmm — alternative: skip limUnder manipulation — prove the Tendsto directly: Tendsto (fun s => (1−hLi(1+s))/s) (𝓝[≠] 0) (𝓝 (−deriv hLi 1)) via hslope.neg + congr', then limUnder_eq. Let me restructure:
have hT : Tendsto (fun s : ℂ => (1 - hLi (1 + s)) / s) (𝓝[≠] 0) (𝓝 (-deriv hLi 1)) := by
apply hslope.neg.congr' -- hmm Tendsto.congr' direction — see session 017 note: f₁ =ᶠ f₂ → Tendsto f₁ → Tendsto f₂: here f₁ := the neg slope fun, f₂ := (1−hLi(1+s))/s: need (negslope) =ᶠ (target): hev.symm — hev : target =ᶠ negslope — wait I wrote hev : target =ᶠ[𝓝[≠] 0] negslope — hslope.neg : Tendsto negslope ... — Tendsto.congr' (hl : f₁ =ᶠ f₂) (h : Tendsto f₁) : Tendsto f₂ — with f₁ := target... I have h : Tendsto negslope — so need hl : negslope =ᶠ target := hev.symm ✓: hslope.neg.congr' hev.symm ✓.
exact hT.limUnder_eq
```
OK. Then:
```lean
def hLiExt : ℂ → ℂ := Function.update (fun s => (1 - hLi (1 + s)) / s) 0 (-deriv hLi 1)
lemma hLiExt_zero : hLiExt 0 = -deriv hLi 1 := Function.update_self _ _ _
lemma hLiExt_of_ne {s : ℂ} (hs : s ≠ 0) : hLiExt s = (1 - hLi (1 + s)) / s := Function.update_of_ne hs _ _
lemma hLiExt_analyticAt_zero : AnalyticAt ℂ hLiExt 0 := by
-- removable singularity pattern from zetaA_analyticAt_one
-- need: a punctured ball where differentiable + bounded
...
```
For the differentiability on a punctured ball: pick ε > 0 with zetaA w ≠ 0 for w ∈ ball 1 ε (from zetaA_ne_zero_near_one — ∀ᶠ w in 𝓝 1 — Metric.eventually_nhds_iff_ball or mem_nhds_iff: get ε). On ball 1 ε: hLi analytic:
```lean
have hball : ∀ᶠ w in 𝓝 (1:ℂ), AnalyticAt ℂ hLi w := hLi_analyticAt_one.eventually_analyticAt
```
Oh nice — `AnalyticAt.eventually_analyticAt : AnalyticAt f z₀ → ∀ᶠ z in 𝓝 z₀, AnalyticAt f z` ✓ (used in the vendored code line 245 ✓). So hLi analytic on a ball around 1. Then for s ∈ ball 0 ε, s ≠ 0: 1+s ∈ ball 1 ε: (1 − hLi(1+s))/s differentiable: quotient of differentiable (1 − hLi(1+s): comp analytic ✓) by s (≠ 0) ✓.
Bounded: the Tendsto hT gives boundedness on a punctured nhd (isBigO_one → BddAbove on a smaller punctured ball — the zetaA proof used IsBigO_to_BddAbove... — zetaA's proof: obtained δ from the tendsto's Metric.tendsto_nhdsWithin_nhds directly with the bound 1, then BddAbove by 2 via the triangle — mirror that: hT : Tendsto ... (𝓝 (−deriv hLi 1)): take ε = 1: ∃ δ > 0, ∀ s ≠ 0, dist < δ ⟹ ‖(1−hLi(1+s))/s − (−deriv hLi 1)‖ < 1 ⟹ ‖...‖ ≤ ‖deriv hLi 1‖ + 1 — BddAbove by that. Then differentiableOn_update_limUnder_of_bddAbove (ball_mem_nhds 0 (δ/2)) hdiff hbd — gives DifferentiableOn (update ... 0 (limUnder ...)) on ball 0 (δ/2) — with the limUnder value = −deriv hLi 1 by hLiExt_lim — rw. Then .analyticOnNhd isOpen_ball at 0 ✓ — exactly zetaA's proof shape.
Let me re-check zetaA_analyticAt_one's exact structure to clone (LiResidue lines 45-78):
- hT := riemannZeta_residue_one (Tendsto form)
- rw [Metric.tendsto_nhdsWithin_nhds] at hT; obtain ⟨δ, hδ0, hδ⟩ := hT 1 one_pos
- hdiff : DifferentiableOn ℂ (fun w => (w−1)*ζ w) (ball 1 (δ/2) \ {1})
- hbd : BddAbove ((fun z => ‖(z−1)*ζ z‖) '' (ball 1 (δ/2) \ {1})) — via the bound 2.
- h := differentiableOn_update_limUnder_of_bddAbove (ball_mem_nhds 1 (δ/2)) hdiff hbd
- hlim : limUnder (𝓝[≠] 1) ... = 1 := ...limUnder_eq; rw [hlim] at h
- han := h.analyticOnNhd isOpen_ball; exact han 1 (mem_ball_self ...)
So mirror with hT := hLiExt_lim... — wait hLiExt_lim is a limUnder equality; I need the Tendsto form for the Metric.tendsto_nhdsWithin_nhds extraction: use hT (the Tendsto) directly. So structure:
```lean
lemma hLiExt_tendsto : Tendsto (fun s : ℂ => (1 - hLi (1 + s)) / s) (𝓝[≠] 0) (𝓝 (-deriv hLi 1)) := ...
lemma hLiExt_analyticAt_zero : AnalyticAt ℂ hLiExt 0 := by
have hT := hLiExt_tendsto
rw [Metric.tendsto_nhdsWithin_nhds] at hT
obtain ⟨δ, hδ0, hδ⟩ := hT 1 one_pos
-- differentiability on ball 0 (δ/2) \ {0}
obtain ⟨ε, hε0, hε⟩ := ... hLi analytic ball around 1 (from eventually_analyticAt via Metric.eventually_nhds_iff...)
have hdiff : DifferentiableOn ℂ (fun s => (1 - hLi (1 + s)) / s) (Metric.ball 0 (min (δ/2) ε) \ {0}) := ...
have hbd : BddAbove (...) := ⟨‖deriv hLi 1‖ + 1, ...⟩
have h := differentiableOn_update_limUnder_of_bddAbove (Metric.ball_mem_nhds 0 (by positivity : (0:ℝ) < min (δ/2) ε)) hdiff hbd
rw [hLiExt_lim] at h -- the update value in h is limUnder ... — hLiExt's update value is −deriv hLi 1 — need: the update in h uses limUnder — hLiExt uses −deriv hLi 1 — bridge via hLiExt_lim: h's function update ... 0 (limUnder ...) — rw [hLiExt_lim] at h turns limUnder into −deriv hLi 1 ✓ then h's function is exactly hLiExt ✓
have han := h.analyticOnNhd Metric.isOpen_ball
exact han 0 (Metric.mem_ball_self (by positivity))
```
Wait — hLiExt is DEFINED with −deriv hLi 1 as the update value: hLiExt = update f 0 (−deriv hLi 1); the lemma gives DifferentiableOn (update f 0 (limUnder ...)) — with hLiExt_lim : limUnder = −deriv hLi 1 — rw [hLiExt_lim] at h: h : DifferentiableOn (update f 0 (−deriv hLi 1)) — and that's DEFINITIONALLY hLiExt — h : DifferentiableOn ℂ hLiExt (ball...) after defeq — `exact` or rw [hLiExt] at h? hLiExt is a def — the term `Function.update f 0 (−deriv hLi 1)` vs `hLiExt` — delta-eq — `show`-bridge or fold via `rw [← hLiExt]`? hmm: `rw [← hLiExt] at h`?? hLiExt's equation lemma: hLiExt = Function.update ... — rw [← hLiExt]... equation-lemma direction: rw [hLiExt] at h turns hLiExt into the update — I have the update and want hLiExt: `rw [← hLiExt]`?? Hmm — for defs, `rw [hLiExt]` uses the auto-equation hLiExt = update... — rewriting ← turns update... into hLiExt ✓ — hmm does the auto-equation work like that? For `def hLiExt : ℂ → ℂ := Function.update ...`, the equation lemma is `hLiExt.eq_def : hLiExt = Function.update ...` or `hLiExt.eq_...`. rw [← hLiExt] at h — should work if the equation lemma exists. Alternatively end with `exact han 0 ...` where han's type mentions the update-form and the goal has hLiExt — `exact` uses defeq ✓ — han 0 (...) : (update ...) ∈ ... wait — h.analyticOnNhd gives AnalyticOnNhd ℂ (update ...) (ball ...) — han 0 (mem) : AnalyticAt ℂ (update ...) 0 — goal: AnalyticAt ℂ hLiExt 0 — defeq ✓ exact works ✓. I'll rely on exact-defeq (it worked for zetaA: `exact han 1 (...)` — zetaA's proof ended exactly that way with zetaA's def ✓).
The function identity + Leibniz + comp bridge:
```lean
lemma hLiExt_mul_id : (fun s : ℂ => s * hLiExt s) = fun s => 1 - hLi (1 + s) := by
funext s
by_cases hs : s = 0
· subst hs
simp [hLiExt_zero, hLi_one] -- 0 * (−deriv hLi 1) = 0 and 1 − hLi 1 = 1 − 1 = 0
· rw [hLiExt_of_ne hs]
field_simp [hs] -- s * ((1 − hLi(1+s))/s) = 1 − hLi(1+s)
-- field_simp might close; else: rw [mul_div_cancel₀ ...]
```
mul_div_cancel₀ : a ≠ 0 → a * (b / a) = b? `mul_div_cancel_left₀ (ha : a ≠ 0) : a * b / a = b` — our form: s * ((1−hLi)/s) = (1−hLi): `mul_div_cancel_right₀`? : a * b / a?? the term is s * ((1−hLi(1+s))/s) = s * (1−hLi(1+s)) / s — mul_div_cancel_left₀ (hs) : s * X / s = X — is the expression s * (X/s) or s*X/s? After rw [hLiExt_of_ne hs]: goal s * ((1 − hLi (1+s))/s) = 1 − hLi (1+s) — the form s * (X/s): mul_div_cancel_left₀'s LHS is a * b / a — parses (a*b)/a — s * (X/s) parses as s * (X/s) — HMul s (HDiv X s) — different from (s*X)/s — need reassociation: `rw [mul_div_assoc', ...]`? mul_div_assoc' : a * (b / c) = (a * b) / c ✓ then mul_div_cancel_left₀ hs : (s * X)/s = X ✓. So: rw [hLiExt_of_ne hs, mul_div_assoc', mul_div_cancel_left₀ _ hs]... mul_div_cancel_left₀ (b) (ha : a ≠ 0)? — earlier session found: mul_div_cancel_left₀ (b : M₀) {a : M₀} (ha : a ≠ 0) : a * b / a = b — explicit b first! So `mul_div_cancel_left₀ _ hs` ✓.
Hmm wait — simpler: `field_simp [hs]` closes s * ((1−hLi)/s) = 1−hLi directly (field_simp clears /s then rfl) ✓ try field_simp first.
Then:
```lean
lemma iteratedDeriv_hLiExt (j : ℕ) :
iteratedDeriv j hLiExt 0 = -(Nat.factorial j : ℂ) * lcoeff j := by
have hcid : ContDiffAt ℂ (j + 1) (fun s : ℂ => s) 0 := contDiff_id.contDiffAt
have hcE : ContDiffAt ℂ (j + 1) hLiExt 0 := hLiExt_analyticAt_zero.contDiffAt
have h1 := iteratedDeriv_mul hcid hcE -- iteratedDeriv (j+1) ((fun s => s) * hLiExt) 0 = Σ ...
-- LHS via the function identity
have hfun : ((fun s : ℂ => s) * hLiExt) = fun s => 1 - hLi (1 + s) := by
funext s
show s * hLiExt s = 1 - hLi (1 + s) -- Pi.mul_apply defeq
... hLiExt_mul_id pointwise
-- iteratedDeriv (j+1) (fun s => 1 − hLi(1+s)) 0 = −iteratedDeriv (j+1) hLi 1
have hcomp : iteratedDeriv (j + 1) (fun s : ℂ => hLi (1 + s)) 0 = iteratedDeriv (j + 1) hLi 1 := by
-- comp with (1 + ·) = (· + 1) = (· − (−1))
have e := congr_fun (iteratedDeriv_comp_sub_const (j+1) hLi (-1 : ℂ)) 0
-- e : iteratedDeriv (j+1) (hLi ∘ (· − −1)) 0 = iteratedDeriv (j+1) hLi (0 − −1) = iteratedDeriv (j+1) hLi 1
simpa using e
...
```
Hmm — iteratedDeriv_comp_sub_const's exact form — from A_iter: `congr_fun (iteratedDeriv_comp_sub_const i (fun w : ℂ => w ^ n) (1 : ℂ)) 1` : so iteratedDeriv_comp_sub_const (i) (f) (c) : iteratedDeriv i (f ∘ (· − c)) = fun x => iteratedDeriv i f (x − c) — a FUNCTION equality. With f := hLi, c := −1: hLi ∘ (· − −1) = fun s => hLi (s + 1) — and I need fun s => hLi (1 + s) — s + 1 vs 1 + s — comm! add_comm. So:
```lean
have hcomp : iteratedDeriv (j + 1) (fun s : ℂ => hLi (1 + s)) 0 = iteratedDeriv (j + 1) hLi 1 := by
have e := congr_fun (iteratedDeriv_comp_sub_const (j + 1) hLi (-1 : ℂ)) 0
-- e : iteratedDeriv (j+1) (hLi ∘ (· − −1)) 0 = iteratedDeriv (j+1) hLi (0 − −1)
have e2 : (hLi ∘ (· - (-1 : ℂ))) = (fun s : ℂ => hLi (1 + s)) := by
funext s
simp [Function.comp_apply, sub_neg_eq_add, add_comm]
rw [e2] at e
simpa using e
```
simpa: 0 − −1 = 1 normalization ✓.
Hmm — actually I realize I should double-check `iteratedDeriv_comp_sub_const`'s exact signature in Mathlib — A_iter used it successfully: `iteratedDeriv_comp_sub_const i (fun w : ℂ => w ^ n) (1 : ℂ)` — three explicit args (i, f, c) returning a function equality (congr_fun applied) ✓.
Then the assembly:
```lean
-- iteratedDeriv (j+1) ((fun s => s) * hLiExt) 0 — via hfun → iteratedDeriv (j+1) (fun s => 1 − hLi(1+s)) 0 = −iteratedDeriv (j+1) hLi 1 (const deriv 0 + comp)
have hLHS : iteratedDeriv (j + 1) ((fun s : ℂ => s) * hLiExt) 0 = -iteratedDeriv (j + 1) hLi 1 := by
rw [hfun]
have hconst : ContDiffAt ℂ (j+1) (fun s : ℂ => (1:ℂ)) 0 := contDiff_const.contDiffAt
have hcompC : ContDiffAt ℂ (j+1) (fun s : ℂ => hLi (1 + s)) 0 := by
-- analytic: hLi analytic at 1 = 1+0: comp
have h1 : AnalyticAt ℂ hLi (1 + (0:ℂ)) := by simpa using hLi_analyticAt_one
have h2 : AnalyticAt ℂ (fun s : ℂ => 1 + s) 0 := analyticAt_const.add analyticAt_id
have h3 := h1.comp h2 -- AnalyticAt.comp : AnalyticAt f (g x) → AnalyticAt g x → AnalyticAt (f ∘ g) x
-- (hLi ∘ (1+·)) vs (fun s => hLi (1+s)): defeq
exact h3.contDiffAt
rw [show (fun s : ℂ => 1 - hLi (1 + s)) = (fun s => (1:ℂ)) - (fun s => hLi (1 + s)) from by funext s; simp [Pi.sub_apply]]
rw [iteratedDeriv_sub hconst hcompC]
simp [hcomp] -- iteratedDeriv (j+1) (fun s => 1) 0 = 0 (j+1 ≥ 1: deriv of const)
-- the RHS: iteratedDeriv_mul sum collapse
...
```
- `iteratedDeriv_sub` ✓ (used in A_iter).
- iteratedDeriv (j+1) (fun s => 1) 0 = 0 for j+1 ≥ 1: `iteratedDeriv_const`? : iteratedDeriv n (fun _ => c) x = 0 for n ≥ 1? there should be `iteratedDeriv_const (c) (hn : n ≠ 0)?`... I recall `iteratedDeriv_const : iteratedDeriv n (fun _ => c) = 0`? with n ≠ 0 condition. simp should handle via `iteratedDeriv_succ` + deriv_const... let me use: have : iteratedDeriv (j+1) (fun s : ℂ => (1:ℂ)) 0 = 0 := by rw [iteratedDeriv_succ']; simp [iteratedDeriv_const?]... hmm — `iteratedDeriv_succ' : iteratedDeriv (n+1) f = deriv (iteratedDeriv n f)`? then deriv of the const-function-iteratedDeriv... iteratedDeriv j (fun _ => 1) is the constant zero FUNCTION for j ≥ 1 (inductively) — circular. There IS `iteratedDeriv_const (c : 𝔸) (hn : 0 < n)?: iteratedDeriv n (fun _ => c) = 0` — I'll trust something like iteratedDeriv_const exists with a positivity side or simp lemma `iteratedDeriv_const_of_ne_zero`? Alternatively: contDiff_const... simplest: `by simp` — simp lemmas: iteratedDeriv_const? Let me just try `simp` and fix if needed.
- The Leibniz sum collapse: h1 : iteratedDeriv (j+1) ((fun s => s) * hLiExt) 0 = Σ_{i ∈ range (j+2)} (j+1).choose i * iteratedDeriv i (fun s => s) 0 * iteratedDeriv (j+1−i) hLiExt 0. iteratedDeriv i (fun s => s) 0: for i = 0: 0 (the value — (fun s => s) 0 = 0); i = 1: 1; i ≥ 2: 0. So the sum = the i = 1 term: (j+1).choose 1 * 1 * iteratedDeriv j hLiExt 0 = (j+1)·iteratedDeriv j hLiExt 0.
In Lean: Finset.sum_eq_single 1: side goals: (i) other terms vanish: i ∈ range(j+2), i ≠ 1: i = 0: iteratedDeriv 0 (fun s => s) 0 = 0 — `iteratedDeriv_zero : iteratedDeriv 0 f = f` ✓ then (fun s => s) 0 = 0 — `by simp [iteratedDeriv_zero]`? hmm iteratedDeriv_zero : iteratedDeriv 0 f = f — then f 0 = 0 by rfl (id 0 = 0 — the function is fun s => s — applied 0 = 0 ✓ rfl/simp). i ≥ 2: iteratedDeriv i (fun s => s) 0 = 0: iteratedDeriv of id beyond 1: deriv id = const 1, higher = 0: there might be `iteratedDeriv_id`? or prove: iteratedDeriv i (fun s => s) 0 = 0 for i ≥ 2: via iteratedDeriv_succ' twice: iteratedDeriv 2 id = deriv (deriv id) = deriv (fun _ => 1) = 0... — a mini-lemma:
```lean
have hid : ∀ i : ℕ, iteratedDeriv i (fun s : ℂ => s) 0 = if i = 1 then 1 else 0 := by
intro i
rcases i with _ | _ | i
· simp [iteratedDeriv_zero] -- i = 0: (fun s => s) 0 = 0
· simp [iteratedDeriv_one] -- i = 1: deriv (fun s => s) 0 = 1: iteratedDeriv_one : iteratedDeriv 1 f = deriv f; deriv_id''
· -- i ≥ 2
have : iteratedDeriv (i + 2) (fun s : ℂ => s) = fun _ => 0 := by
induction i with
| zero => -- iteratedDeriv 2 id: deriv (deriv id) = deriv (fun _ => 1) = 0
funext s
rw [iteratedDeriv_succ', iteratedDeriv_one, deriv_id'']
simp
| succ i ih => rw [iteratedDeriv_succ', ih]; simp
rw [this]
simp
```
Hmm wait iteratedDeriv_succ' : iteratedDeriv (n+1) f = deriv (iteratedDeriv n f)? or iteratedDeriv (n+1) f x = deriv (iteratedDeriv n f) x — roughly ✓ (there's iteratedDeriv_succ and iteratedDeriv_succ' — one is deriv (iteratedDeriv n f), the other iteratedDeriv n (deriv f)). For i = 2: iteratedDeriv 2 (fun s => s) = deriv (iteratedDeriv 1 (fun s => s)) [succ'] = deriv (deriv (fun s => s)) [iteratedDeriv_one] = deriv (fun _ => 1) [deriv_id''] = 0 [deriv_const] — funext s; simp [iteratedDeriv_succ', iteratedDeriv_one, deriv_id''] — should work with care.
This is getting long but standard. Then sum_eq_single 1: 1 ∈ range(j+2) ✓ (j ≥ 0 ⟹ 1 < j+2 ✓); the i = 1 term: (j+1).choose 1 * iteratedDeriv 1 (fun s => s) 0 * iteratedDeriv j hLiExt 0 = (j+1)·1·iteratedDeriv j hLiExt 0 — Nat.choose_one_right ✓ cast; iteratedDeriv 1 (fun s => s) 0 = 1 via hid (if_pos rfl) ✓.
Conclude: iteratedDeriv (j+1) ((fun s => s)*hLiExt) 0 = (j+1)·iteratedDeriv j hLiExt 0. Combined with hLHS: (j+1)·iteratedDeriv j hLiExt 0 = −iteratedDeriv (j+1) hLi 1. So iteratedDeriv j hLiExt 0 = −iteratedDeriv (j+1) hLi 1/(j+1) — and lcoeff j = iteratedDeriv (j+1) hLi 1/(j+1)! — so iteratedDeriv (j+1) hLi 1 = (j+1)!·lcoeff j — then iteratedDeriv j hLiExt 0 = −(j+1)!·lcoeff j/(j+1) = −j!·lcoeff j ✓ (factorial: (j+1)! = (j+1)·j! — `Nat.factorial_succ` ✓).
Cast management: the goal is `iteratedDeriv j hLiExt 0 = -(Nat.factorial j : ℂ) * lcoeff j`. From (j+1 : ℂ)·X = −Y with X := iteratedDeriv j hLiExt 0, Y := iteratedDeriv (j+1) hLi 1: X = −Y/(j+1) — field_simp with (j+1 : ℂ) ≠ 0 (Nat.cast — j+1 ≥ 1 ✓ `Nat.cast_ne_zero`); Y = ((j+1)! : ℂ)·lcoeff j (from lcoeff's def: lcoeff j = Y/(j+1)! — `lcoeff` def: iteratedDeriv (j+1) hLi 1 / (j+1)! — so Y = (j+1)!·lcoeff j via div_mul_cancel... `(j+1)!` cast ✓ nonzero ✓). Then X = −((j+1)!)·lcoeff j/(j+1) = −j!·lcoeff j via (j+1)! = (j+1)·j! ✓ field_simp/ring.
OK — this is a well-defined ~150-line file. One concern: `iteratedDeriv_mul` signature — from LiResidue's ResW1_eq_sum: `iteratedDeriv_mul hA hh` with hA hh : ContDiffAt ℂ n f 1 — the sum form: `∑ i ∈ Finset.range (n + 1), n.choose i * iteratedDeriv i f 1 * iteratedDeriv (n - i) g 1` ✓ (from the hmul in ResW1_eq_sum) ✓.
Another: `h1.comp 0 h2` for HasDerivAt comp — the mixed-field chain rule: session-016 note says HasDerivAt.comp handles ℂ→ℂ→ℂ via the algebra tower. The form: HasDerivAt.comp (x) (hf : HasDerivAt f f' (g x)) (hg : HasDerivAt g g' x) : HasDerivAt (f ∘ g) (g' • f')? — for ℂ→ℂ: the result's derivative is f' * g'? or g' * f'? — LiPrincipal's HIntegral_deriv used `h1.comp x h2` then `rw [mul_one] at hcomp` — so the comp gives (dg)•(df) or (df·dg) with a * 1 — the mul_one suggests the form (deriv G ...) * 1 — i.e. HasDerivAt (G ∘ path) (deriv G (...) * 1) — so it's df * dg order: HasDerivAt (f ∘ g) x (f' * g')? Hmm — for HIntegral_deriv: h1 : HasDerivAt G (deriv G p) p; h2 : HasDerivAt path 1 x; hcomp := h1.comp x h2 : HasDerivAt (G ∘ path) ((deriv G p) * 1)?? then mul_one — yes it gave f' * g' = deriv G p * 1 ✓. For my case: h1 : HasDerivAt hLi (deriv hLi 1) 1; h2 : HasDerivAt (fun s => 1 + s) 1 0; h3 := h1.comp 0 h2 : HasDerivAt (hLi ∘ (fun s => 1 + s)) ((deriv hLi 1) * 1) 0 — then mul_one → deriv hLi 1 ✓. But wait — h1's point is 1 and g 0 = 1 + 0 = 1 ✓ matches. And the composition hLi ∘ (fun s => 1 + s) vs my lambda fun s => hLi (1 + s) — defeq ✓ (comp_apply simp).
Also the eventual neighborhoods: for hLiExt_tendsto's hslope — hasDerivAt_iff_tendsto_slope.mp hd : Tendsto (slope (fun s => hLi (1+s)) 0) (𝓝[≠] 0) (𝓝 (deriv hLi 1)) — slope f a = fun x => (f x − f a)/(x − a) — at a = 0: (hLi(1+s) − hLi(1+0))/s — hLi(1+0) = hLi 1 ✓ — simpa [slope_fun_def_field, ...] using this — the slope_fun_def_field : slope f a = fun x => (f x − f a)/(x − a) ✓ — with the (1+0) → 1 normalization via simp ✓.
OK — I'm confident in the plan. Also note — lcoeff's def has `/ (k+1)!` with the Nat factorial cast — from LiResidue: `def lcoeff (k : ℕ) : ℂ := iteratedDeriv (k + 1) hLi 1 / (k + 1)!` ✓.
Let me also reconsider whether to include the H₁ext = "1/s + ζ′/ζ(1+s)" READING (the actual piece-B statement for the assembly): the assembly needs: the meromorphic function 1/s + ζ′/ζ(1+s) has Taylor coefficients −c_j at 0 — with my hLiExt: hLiExt(s) = (1 − hLi(1+s))/s — and (1 − hLi(1+s))/s = (1 + s·ζ′/ζ(1+s))/s = 1/s + ζ′/ζ(1+s) for s ≠ 0 near 0 (ζ(1+s) ≠ 0 eventually — from riemannZeta_residue_one.eventually_ne transported to s near 0: w = 1+s). So hLiExt =ᶠ[𝓝[≠] 0] (fun s => 1/s + ζ′/ζ(1+s))... wait — hLi(1+s) = (1+s−1)(−ζ′/ζ(1+s)) = s·(−ζ′/ζ(1+s)) for 1+s ≠ 1 (s ≠ 0) and ζ(1+s) ≠ 0 — via hLi_eq_of_ne (needs w ≠ 1 ∧ ζ w ≠ 0) ✓. So (1 − hLi(1+s))/s = (1 + s·ζ′/ζ(1+s))/s = 1/s + ζ′/ζ(1+s) ✓ — the reading lemma:
```lean
lemma hLiExt_eq_near_zero : ∀ᶠ s in 𝓝[≠] (0:ℂ), hLiExt s = 1/s + deriv riemannZeta (1+s) / riemannZeta (1+s) := by
-- from hLi_eq_of_ne + riemannZeta_residue_one.eventually_ne transported
```
This connects the abstract hLiExt to the actual ζ′/ζ — the assembly will need it. Include it.
The transport: ζ(1+s) ≠ 0 for s ∈ 𝓝[≠] 0 small: from riemannZeta_residue_one.eventually_ne : ∀ᶠ w in 𝓝[≠] 1, (w−1)·ζ w ≠ 0 — as a statement about w near 1 — I need it about s = w−1 near 0: Tendsto (fun s => 1 + s) (𝓝[≠] 0) (𝓝[≠] 1)?? — the map s ↦ 1+s sends 𝓝[≠] 0 into 𝓝[≠] 1 (continuous, 1+0 = 1, and s ≠ 0 ⟹ 1+s ≠ 1 ✓): `Tendsto (fun s => 1+s) (𝓝[≠] 0) (𝓝[≠] 1)` — via `tendsto_nhdsWithin_...`? There's tendsto_nhdsWithin_of... the composition: (fun s => 1+s) — Tendsto to 𝓝 1 ✓ (continuous) and maps {0}ᶜ into {1}ᶜ ✓ (s ≠ 0 ⟹ 1+s ≠ 1 by add_right... 1+s = 1 ⟺ s = 0 ✓ add_left_cancel). So `Filter.Tendsto.eventually`... h : ∀ᶠ w in 𝓝[≠] 1, p w and the map tends to 𝓝[≠] 1 ⟹ ∀ᶠ s in 𝓝[≠] 0, p (1+s) — `Tendsto.eventually (h : Tendsto f l₁ l₂) (hp : ∀ᶠ y in l₂, p y) : ∀ᶠ x in l₁, p (f x)` ✓ exists. The map-tendsto: Tendsto (fun s => 1+s) (𝓝[≠] 0) (𝓝[≠] 1): `tendsto_nhdsWithin` needs (Tendsto f (𝓝 0) (𝓝 1)) ∧ (maps {0}ᶜ into {1}ᶜ): `tendsto_nhdsWithin_iff : Tendsto f (𝓝[s] x) (𝓝[t] y) ↔ Tendsto f (𝓝 x) (𝓝 y) ∧ ∀ᶠ x' in 𝓝[s] x, f x' ∈ t` ✓. Continuous part: (continuousAt_const.add continuousAt_id... (1 + s): ContinuousAt (fun s => 1 + s) 0 — `continuousAt_const.add continuousAt_id` — gives Tendsto ... (𝓝 (1 + 0)) = 𝓝 1 ✓ simp. The mapsTo: ∀ᶠ s in 𝓝[≠] 0, 1 + s ∈ {1}ᶜ — from self_mem_nhdsWithin: s ≠ 0 ⟹ 1 + s ≠ 1 ✓.
OK. Writing the file now. Name: LiZetaCoeff.lean.
Now piece (B) — the ζ-piece coefficient reading. New file `LiZetaCoeff.lean`.
tool: Write ok
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiZetaCoeff.lean",
"content": "/-\nNguyenRH1/LiZetaCoeff.lean \u2014 tier ii\u2032 sub-stage ii\u2032-3a, piece (B)\n(D-066 \u00a72): the \u03b6-piece of the (4.10) coefficient split.\n\nThe meromorphic function 1/s + \u03b6\u2032/\u03b6(1+s) is analytic at s = 0 (the pole\ncancels: \u2212\u03b6\u2032/\u03b6(1+s) = 1/s + \u03a3_j c_j s^j), and its j-th Taylor coefficient\nat 0 is \u2212c_j = \u2212lcoeff j. We package this as the analytic function\n\n hLiExt s := (1 \u2212 hLi (1+s)) / s [extended by \u2212deriv hLi 1 at 0]\n\n(since hLi(1+s) = s\u00b7(\u2212\u03b6\u2032/\u03b6(1+s)) punctured near 0 by `hLi_eq_near_one`,\nhLiExt = 1/s + \u03b6\u2032/\u03b6(1+s) on a punctured neighbourhood \u2014\n`hLiExt_eq_near_zero`) and prove\n\n **iteratedDeriv j hLiExt 0 = \u2212(j!)\u00b7lcoeff j**\n\n\u2014 by the exact function identity s\u00b7hLiExt s = 1 \u2212 hLi(1+s)\n(`hLiExt_mul_id`), the Leibniz collapse (iteratedDeriv_mul with the\nidentity factor killing all but the i = 1 term), and the comp bridge\niteratedDeriv (j+1) (hLi(1+\u00b7)) 0 = iteratedDeriv (j+1) hLi 1.\n\nArchive references: D-066 (route \u03b24, piece B), D-064, journal-019.\n-/\nimport Mathlib\nimport NguyenRH1.LiResidue\n\nopen Zeta23 Complex Filter Topology\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. The limit value at 0 -/\n\n/-- The slope limit: (1 \u2212 hLi(1+s))/s \u2192 \u2212deriv hLi 1 as s \u2192 0, s \u2260 0. -/\nlemma hLiExt_tendsto :\n Tendsto (fun s : \u2102 => (1 - hLi (1 + s)) / s) (\ud835\udcdd[\u2260] 0) (\ud835\udcdd (-deriv hLi 1)) := by\n have hd : HasDerivAt (fun s : \u2102 => hLi (1 + s)) (deriv hLi 1) 0 := by\n have h1 : HasDerivAt hLi (deriv hLi 1) 1 := hLi_analyticAt_one.differentiableAt.hasDerivAt\n have h2 : HasDerivAt (fun s : \u2102 => 1 + s) 1 0 := by\n simpa using (hasDerivAt_id (0 : \u2102)).const_add 1\n have h3 := h1.comp 0 h2\n rw [mul_one] at h3\n have h4 : (hLi \u2218 fun s : \u2102 => 1 + s) = fun s : \u2102 => hLi (1 + s) := rfl\n rw [h4] at h3\n exact h3\n have hslope : Tendsto (fun s : \u2102 => (hLi (1 + s) - hLi 1) / s) (\ud835\udcdd[\u2260] 0)\n (\ud835\udcdd (deriv hLi 1)) := by\n have h := hasDerivAt_iff_tendsto_slope.mp hd\n simpa [slope_fun_def_field] using h\n have hev : (fun s : \u2102 => -((hLi (1 + s) - hLi 1) / s)) =\u1da0[\ud835\udcdd[\u2260] 0]\n (fun s => (1 - hLi (1 + s)) / s) := by\n filter_upwards [self_mem_nhdsWithin] with s hs\n rw [hLi_one]\n ring\n exact hslope.neg.congr' hev\n\n/-! ## 2. hLiExt: the analytic extension -/\n\n/-- hLiExt s := (1 \u2212 hLi(1+s))/s, extended by \u2212deriv hLi 1 at 0 \u2014 the\nanalytic-at-0 form of 1/s + \u03b6\u2032/\u03b6(1+s) (`hLiExt_eq_near_zero`). -/\ndef hLiExt : \u2102 \u2192 \u2102 := Function.update (fun s => (1 - hLi (1 + s)) / s) 0 (-deriv hLi 1)\n\nlemma hLiExt_zero : hLiExt 0 = -deriv hLi 1 := Function.update_self _ _ _\n\nlemma hLiExt_of_ne {s : \u2102} (hs : s \u2260 0) : hLiExt s = (1 - hLi (1 + s)) / s :=\n Function.update_of_ne hs _ _\n\n/-- hLiExt is analytic at 0 (removable singularity; the limit exists by\n`hLiExt_tendsto`). Mirrors `zetaA_analyticAt_one`. -/\nlemma hLiExt_analyticAt_zero : AnalyticAt \u2102 hLiExt 0 := by\n have hT := hLiExt_tendsto\n rw [Metric.tendsto_nhdsWithin_nhds] at hT\n obtain \u27e8\u03b4, h\u03b40, h\u03b4\u27e9 := hT 1 one_pos\n -- hLi is analytic on a ball around 1\n have hball : \u2200\u1da0 w in \ud835\udcdd (1 : \u2102), AnalyticAt \u2102 hLi w :=\n hLi_analyticAt_one.eventually_analyticAt\n rw [Metric.eventually_nhds_iff_ball] at hball\n obtain \u27e8\u03b5, h\u03b50, h\u03b5\u27e9 := hball\n -- differentiability on a punctured ball around 0\n have hdiff : DifferentiableOn \u2102 (fun s => (1 - hLi (1 + s)) / s)\n (Metric.ball 0 (min (\u03b4 / 2) \u03b5) \\ {0}) := by\n intro s hs\n have hs0 : s \u2260 0 := hs.2\n have hs1 : (1 + s) \u2208 Metric.ball 1 \u03b5 := by\n have hds : dist s 0 < \u03b5 := lt_of_lt_of_le hs.1 (min_le_right _ _)\n rw [Metric.mem_ball, dist_zero_right] at hds\n rw [Metric.mem_ball]\n have : (1 + s) - 1 = s := by ring\n rw [this]\n exact hds\n have ha : AnalyticAt \u2102 hLi (1 + s) := h\u03b5 (1 + s) hs1\n have hnum : DifferentiableAt \u2102 (fun s : \u2102 => 1 - hLi (1 + s)) s := by\n have hcomp : AnalyticAt \u2102 hLi (1 + s) := ha\n have hpath : AnalyticAt \u2102 (fun s : \u2102 => 1 + s) s :=\n analyticAt_const.add analyticAt_id\n have h := hcomp.comp hpath\n have heq : (hLi \u2218 fun s : \u2102 => 1 + s) = fun s : \u2102 => hLi (1 + s) := rfl\n rw [heq] at h\n exact analyticAt_const.sub h |>.differentiableAt\n exact hnum.div (differentiableAt_id) hs0 |>.differentiableWithinAt\n -- boundedness on the punctured ball\n have hbd : BddAbove ((fun s => \u2016(1 - hLi (1 + s)) / s\u2016) ''\n (Metric.ball 0 (min (\u03b4 / 2) \u03b5) \\ {0})) := by\n refine \u27e8\u2016deriv hLi 1\u2016 + 1, ?_\u27e9\n rintro _ \u27e8s, hs, rfl\u27e9\n have hs0 : s \u2260 0 := hs.2\n have hds : dist s 0 < \u03b4 := by\n have := hs.1\n rw [Metric.mem_ball] at this\n have h2 : dist s 0 < min (\u03b4 / 2) \u03b5 := this\n have h3 : min (\u03b4 / 2) \u03b5 \u2264 \u03b4 / 2 := min_le_left _ _\n linarith [h2, h3, h\u03b40]\n have h1 := h\u03b4 (Set.mem_compl_singleton_iff.mpr hs0) hds\n rw [dist_eq_norm] at h1\n have h2 : \u2016(1 - hLi (1 + s)) / s\u2016 \u2264 \u2016(1 - hLi (1 + s)) / s - (-deriv hLi 1)\u2016 +\n \u2016(-deriv hLi 1 : \u2102)\u2016 := by\n nth_rewrite 1 [show (1 - hLi (1 + s)) / s =\n ((1 - hLi (1 + s)) / s - (-deriv hLi 1)) + (-deriv hLi 1) from by ring]\n exact norm_add_le _ _\n rw [norm_neg] at h2\n linarith [h1, h2]\n have h := differentiableOn_update_limUnder_of_bddAbove\n (Metric.ball_mem_nhds 0 (by positivity : (0 : \u211d) < min (\u03b4 / 2) \u03b5)) hdiff hbd\n have hlim : limUnder (\ud835\udcdd[\u2260] (0 : \u2102)) (fun s => (1 - hLi (1 + s)) / s) = -deriv hLi 1 :=\n hLiExt_tendsto.limUnder_eq\n rw [hlim] at h\n have han := h.analyticOnNhd Metric.isOpen_ball\n exact han 0 (Metric.mem_ball_self (by positivity : (0 : \u211d) < min (\u03b4 / 2) \u03b5))\n\n/-! ## 3. The function identity and the coefficient reading -/\n\n/-- The exact global identity s\u00b7hLiExt s = 1 \u2212 hLi(1+s). -/\nlemma hLiExt_mul_id : (fun s : \u2102 => s) * hLiExt = fun s => 1 - hLi (1 + s) := by\n funext s\n by_cases hs : s = 0\n \u00b7 subst hs\n rw [hLiExt_zero, hLi_one]\n simp\n \u00b7 rw [hLiExt_of_ne hs]\n show s * ((1 - hLi (1 + s)) / s) = 1 - hLi (1 + s)\n rw [mul_div_assoc', mul_div_cancel_left\u2080 _ hs]\n\n/-- The comp bridge: iterated derivatives of hLi(1+\u00b7) at 0 = those of hLi at 1. -/\nlemma iteratedDeriv_hLi_one_add (m : \u2115) :\n iteratedDeriv m (fun s : \u2102 => hLi (1 + s)) 0 = iteratedDeriv m hLi 1 := by\n have e := congr_fun (iteratedDeriv_comp_sub_const m hLi (-1 : \u2102)) 0\n have e2 : (hLi \u2218 (\u00b7 - (-1 : \u2102))) = (fun s : \u2102 => hLi (1 + s)) := by\n funext s\n simp [Function.comp_apply, sub_neg_eq_add, add_comm]\n rw [e2] at e\n simpa using e\n\n/-- **Piece (B)** (D-066 \u00a72): the Taylor coefficients of hLiExt at 0 are\n\u2212j!\u00b7lcoeff j \u2014 i.e. 1/s + \u03b6\u2032/\u03b6(1+s) has j-th coefficient \u2212c_j. -/\ntheorem iteratedDeriv_hLiExt (j : \u2115) :\n iteratedDeriv j hLiExt 0 = -(Nat.factorial j : \u2102) * lcoeff j := by\n have hcid : ContDiffAt \u2102 (j + 1) (fun s : \u2102 => s) 0 := contDiff_id.contDiffAt\n have hcE : ContDiffAt \u2102 (j + 1) hLiExt 0 := hLiExt_analyticAt_zero.contDiffAt\n have h1 := iteratedDeriv_mul hcid hcE\n -- LHS via the function identity\n have hLHS : iteratedDeriv (j + 1) ((fun s : \u2102 => s) * hLiExt) 0 =\n -iteratedDeriv (j + 1) hLi 1 := by\n rw [hLiExt_mul_id]\n have hconst : ContDiffAt \u2102 (j + 1) (fun s : \u2102 => (1 : \u2102)) 0 := contDiff_const.contDiffAt\n have hcompC : ContDiffAt \u2102 (j + 1) (fun s : \u2102 => hLi (1 + s)) 0 := by\n have h1a : AnalyticAt \u2102 hLi (1 + (0 : \u2102)) := by simpa using hLi_analyticAt_one\n have h2a : AnalyticAt \u2102 (fun s : \u2102 => 1 + s) 0 := analyticAt_const.add analyticAt_id\n have h3 := h1a.comp h2a\n have heq : (hLi \u2218 fun s : \u2102 => 1 + s) = fun s : \u2102 => hLi (1 + s) := rfl\n rw [heq] at h3\n exact h3.contDiffAt\n rw [show (fun s : \u2102 => 1 - hLi (1 + s)) = (fun s => (1 : \u2102)) - (fun s => hLi (1 + s))\n from by funext s; simp [Pi.sub_apply]]\n rw [iteratedDeriv_sub hconst hcompC]\n have hconst' : iteratedDeriv (j + 1) (fun s : \u2102 => (1 : \u2102)) 0 = 0 := by\n have hj : j + 1 \u2260 0 := by omega\n exact iteratedDeriv_const hj _\n rw [hconst', zero_sub, iteratedDeriv_hLi_one_add]\n -- RHS: the Leibniz sum collapses to the i = 1 term\n have hid : \u2200 i : \u2115, iteratedDeriv i (fun s : \u2102 => s) 0 = if i = 1 then 1 else 0 := by\n intro i\n rcases i with _ | _ | i\n \u00b7 simp [iteratedDeriv_zero]\n \u00b7 simp [iteratedDeriv_one, deriv_id'']\n \u00b7 have h2 : iteratedDeriv (i + 2) (fun s : \u2102 => s) = fun _ => (0 : \u2102) := by\n induction i with\n | zero =>\n funext s\n rw [iteratedDeriv_succ', iteratedDeriv_one, deriv_id'']\n simp\n | succ i ih =>\n rw [iteratedDeriv_succ', ih]\n simp\n rw [h2]\n simp\n have hsum : iteratedDeriv (j + 1) ((fun s : \u2102 => s) * hLiExt) 0 =\n (j + 1 : \u2102) * iteratedDeriv j hLiExt 0 := by\n rw [h1]\n rw [Finset.sum_eq_single 1]\n \u00b7 rw [hid 1, if_pos rfl]\n simp [Nat.choose_one_right]\n \u00b7 intro i hi hi1\n rw [Finset.mem_range] at hi\n rw [hid i, if_neg hi1]\n simp\n \u00b7 intro h1'\n rw [Finset.mem_range] at h1'\n omega\n -- combine\n rw [hsum] at hLHS\n -- (j+1)\u00b7iteratedDeriv j hLiExt 0 = \u2212iteratedDeriv (j+1) hLi 1\n have hlc : iteratedDeriv (j + 1) hLi 1 = ((j + 1)! : \u2102) * lcoeff j := by\n rw [lcoeff]\n have hf : ((j + 1)! : \u2102) \u2260 0 := by simp [Nat.factorial_ne_zero]\n rw [show ((j + 1) ! : \u2102) = (Nat.factorial (j + 1) : \u2102) from rfl]\n field_simp [hf]\n rw [hlc] at hLHS\n have hj1 : ((j + 1 : \u2115) : \u2102) \u2260 0 := by\n simp [Nat.cast_ne_zero]\n have hjs : ((j + 1)! : \u2102) = (j + 1) * (j ! : \u2102) := by\n rw [Nat.factorial_succ]\n simp [Nat.cast_mul, Nat.factorial]\n rw [hjs] at hLHS\n -- (j+1)\u00b7X = \u2212(j+1)\u00b7j!\u00b7lcoeff j \u27f9 X = \u2212j!\u00b7lcoeff j\n have hcancel : (j + 1 : \u2102) * iteratedDeriv j hLiExt 0 =\n (j + 1 : \u2102) * (-(Nat.factorial j : \u2102) * lcoeff j) := by\n rw [hLHS]\n ring\n exact mul_left_cancel\u2080 hj1 hcancel\n\n/-! ## 4. The reading as 1/s + \u03b6\u2032/\u03b6(1+s) -/\n\n/-- On a punctured neighbourhood of 0, hLiExt s = 1/s + \u03b6\u2032/\u03b6(1+s). -/\nlemma hLiExt_eq_near_zero :\n \u2200\u1da0 s in \ud835\udcdd[\u2260] (0 : \u2102),\n hLiExt s = 1 / s + deriv riemannZeta (1 + s) / riemannZeta (1 + s) := by\n -- \u03b6(1+s) \u2260 0 on a punctured nhd of 0 (transport of residue_one.eventually_ne)\n have hne1 : \u2200\u1da0 w in \ud835\udcdd[\u2260] (1 : \u2102), riemannZeta w \u2260 0 := by\n have h := riemannZeta_residue_one.eventually_ne (show (1 : \u2102) \u2260 0 by norm_num)\n filter_upwards [h] with w hw\n have h2 := hw\n simp only [ne_eq, mul_eq_zero] at h2\n push Not at h2\n exact h2.2\n have hmap : Tendsto (fun s : \u2102 => 1 + s) (\ud835\udcdd[\u2260] (0 : \u2102)) (\ud835\udcdd[\u2260] (1 : \u2102)) := by\n rw [tendsto_nhdsWithin_iff]\n refine \u27e8?_, ?_\u27e9\n \u00b7 have hc : ContinuousAt (fun s : \u2102 => 1 + s) 0 :=\n continuousAt_const.add continuousAt_id\n simpa using hc.tendsto\n \u00b7 filter_upwards [self_mem_nhdsWithin] with s hs\n intro hcontra\n exact hs (by simpa using hcontra)\n have hne : \u2200\u1da0 s in \ud835\udcdd[\u2260] (0 : \u2102), riemannZeta (1 + s) \u2260 0 := hmap.eventually hne1\n filter_upwards [hne, self_mem_nhdsWithin] with s hs0 hs\n have hs1 : (1 : \u2102) + s \u2260 1 := by\n intro h\n exact hs (by linarith [h] |>.symm \u25b8 (by simp : (0:\u2102) = 0) |> fun x => x)\n sorry_replace\n sorry\n"
}
result 2026-08-22 05:24:16Z → 2026-08-28 23:59:33Z
{
"type": "create",
"filePath": "D:\\Python\\quantum-deploy\\probe6.cgi",
"content": "#!/opt/alt/python311/bin/python3.11\n\"\"\"One-off diagnostic: full app flow for the REAL rewrite environ \u2014\nnormalize, build request, resolve, call the view. DELETE AFTER USE.\"\"\"\nimport os\nimport sys\nimport traceback\n\nDOCROOT = os.path.dirname(os.path.abspath(__file__))\nAPP = os.path.join(DOCROOT, \"app\")\nsys.path.insert(0, os.path.join(APP, \"vendor\"))\nsys.path.insert(0, os.path.join(APP, \"web\"))\nos.environ.setdefault(\"DJANGO_SETTINGS_MODULE\", \"rhweb.settings\")\n\nfrom urllib.parse import unquote_to_bytes\n\n\ndef out(*a):\n print(*a)\n sys.stdout.flush()\n\n\nout(\"Content-Type: text/plain; charset=utf-8\")\nout()\n\ntry:\n import io\n import django\n django.setup()\n from django.core.handlers.wsgi import WSGIRequest\n from django.urls import resolve, Resolver404\n\n out(\"RAW PATH_INFO :\", repr(os.environ.get(\"PATH_INFO\")))\n out(\"RAW SCRIPT_URL :\", repr(os.environ.get(\"SCRIPT_URL\")))\n out(\"RAW REDIRECT_URL:\", repr(os.environ.get(\"REDIRECT_URL\")))\n out(\"RAW SCRIPT_NAME :\", repr(os.environ.get(\"SCRIPT_NAME\")))\n\n environ = dict(os.environ)\n for key in (\"PATH_INFO\", \"SCRIPT_URL\", \"REDIRECT_URL\"):\n v = environ.get(key)\n if v:\n environ[key] = unquote_to_bytes(v).decode(\"latin-1\")\n environ.setdefault(\"wsgi.input\", io.BytesIO(b\"\"))\n environ.setdefault(\"wsgi.errors\", sys.stderr)\n\n req = WSGIRequest(environ)\n out(\"path_info :\", repr(req.path_info))\n try:\n match = resolve(req.path_info)\n out(\"resolved :\", match.func.__module__ + \".\" + match.func.__name__)\n out(\"kwargs :\", match.kwargs)\n from dashboard import research_data as rd\n item = rd.collection_item(match.kwargs[\"kind\"], match.kwargs[\"name\"])\n out(\"collection_item :\", \"OK\" if item else \"None -> Http404\")\n if item is None:\n from pathlib import Path\n folder = Path(\"/app/research/resources\")\n want = folder / (match.kwargs[\"name\"] + \".txt\")\n out(\"want :\", repr(str(want)), \"exists:\", want.exists())\n out(\"dir listing :\", [repr(p.name) for p in sorted(folder.glob('*.txt')) if ord(p.name[0]) > 127])\n except Resolver404 as e:\n out(\"Resolver404 :\", e)\nexcept BaseException:\n out(\"TRACEBACK:\")\n out(traceback.format_exc())\n",
"structuredPatch": [],
"originalFile": null
}
raw content_json (database row)
[{"type":"thinking","thinking":"Design note committed (62a1ddf). Now start Piece B — the ζ-piece coefficient reading. New file `LiZetaCoeff.lean`:\n\nContents:\n1. `hLiExt` — the extension of (1 − hLi(1+s))/s to s = 0 with value −deriv hLi 1; analytic at 0.\n2. The function identity s·hLiExt s = 1 − hLi(1+s).\n3. The comp bridge iteratedDeriv m (hLi ∘ (1+·)) 0 = iteratedDeriv m hLi 1.\n4. The Leibniz collapse.\n5. Main: iteratedDeriv j hLiExt 0 = −(j! : ℂ)·lcoeff j.\n\nLet me check the comp lemma name first: LiResidue used `iteratedDeriv_comp_sub_const` — signature: iteratedDeriv_comp_sub_const (n : ℕ) (f : ℂ → ℂ) (c : ℂ)? : iteratedDeriv n (f ∘ (· − c)) = fun x => iteratedDeriv n f (x − c)? — from A_iter's usage: congr_fun (iteratedDeriv_comp_sub_const i (fun w => w^n) (1:ℂ)) 1 : iteratedDeriv i ((fun w => w^n) ∘ (·−1)) 1 = iteratedDeriv i (fun w => w^n) (1−1)... So iteratedDeriv_comp_sub_const i f c : (iteratedDeriv i (f ∘ (· − c))) = fun x => iteratedDeriv i f (x − c) ✓.\n\nFor (1 + ·): hLi(1+s) = hLi ∘ (fun s => 1 + s) = hLi ∘ (· + 1)?? 1 + s — is there iteratedDeriv_comp_add_const : iteratedDeriv n (f ∘ (· + c)) x = iteratedDeriv n f (x + c)? Or derive from the sub version: 1 + s = s + 1 — (· + 1) = (· − (−1)) — use iteratedDeriv_comp_sub_const with c := −1: f ∘ (· − (−1)) — and (· − (−1)) = (· + 1) defeq ✓. Let me check the exact name/form of iteratedDeriv_comp_sub_const first. Also check if there's `iteratedDeriv_comp_add_const` directly.\n\nFor the analyticity of hLi on a ball around 1: need a ball where zetaA ≠ 0: zetaA_ne_zero_near_one : ∀ᶠ w in 𝓝 1, zetaA w ≠ 0 — extract a ball: Metric.eventually_nhds_iff... get ε > 0 with zetaA w ≠ 0 on ball 1 ε (punctured? at 1 zetaA 1 = 1 ≠ 0 too — the eventually is on 𝓝 1 (full) ✓ since zetaA 1 = 1 ≠ 0 and continuity ✓). On ball 1 ε: hLi analytic: hLi w = 1 − (w−1)(deriv zetaA w / zetaA w): zetaA analytic on the ball (zetaA_analyticOnNhd_univ), deriv zetaA analytic, quotient by zetaA ≠ 0 ✓. So hLi AnalyticOnNhd on the ball. Then (1 − hLi(1+s))/s differentiable for s ≠ 0 small: hLi(1+s): comp analytic at s (1+s ∈ ball). ✓\n\nThen hLiExt := Function.update (fun s => (1 − hLi (1+s))/s) 0 (−deriv hLi 1) — wait the value: limUnder (𝓝[≠] 0) (fun s => (1−hLi(1+s))/s) = −deriv hLi 1? — the removable-singularity lemma `differentiableOn_update_limUnder_of_bddAbove` (used in zetaA_analyticAt_one) takes the update value := limUnder — so define hLiExt with value limUnder and separately prove limUnder = −deriv hLi 1. zetaA used `Function.update (fun w => (w−1)*ζ w) 1 1` with the value 1 directly + a separate hlim rewrite. Mirror: hLiExt := Function.update (fun s => (1 − hLi (1 + s)) / s) 0 (limUnder (𝓝[≠] 0) (fun s => (1 − hLi (1 + s)) / s)) — then a lemma limUnder ... = −deriv hLi 1 gives hLiExt 0 = −deriv hLi 1.\n\nHmm — actually let me structure it exactly like zetaA_analyticAt_one:\n```lean\ndef hLiExt : ℂ → ℂ := Function.update (fun s => (1 - hLi (1 + s)) / s) 0 (limUnder (𝓝[≠] 0) (fun s => (1 - hLi (1 + s)) / s))\n```\nWait — that's circular-ish but fine (update with the limUnder value). Actually zetaA := update ... 1 1 (explicit value 1, then proved lim = 1 separately and rw'd). For hLiExt I could put the explicit value −deriv hLi 1 and prove the limUnder equality first:\n\n```lean\nlemma hLiExt_lim : limUnder (𝓝[≠] (0 : ℂ)) (fun s => (1 - hLi (1 + s)) / s) = -deriv hLi 1 := by\n -- (1 − hLi(1+s))/s = −(hLi(1+s) − hLi(1))/s → −deriv (hLi∘(1+·)) 0 = −deriv hLi 1\n have hd : HasDerivAt (fun s : ℂ => hLi (1 + s)) (deriv hLi 1) 0 := by\n have h1 : HasDerivAt hLi (deriv hLi 1) 1 := hLi_analyticAt_one.differentiableAt.hasDerivAt\n have h2 : HasDerivAt (fun s : ℂ => 1 + s) 1 0 := by\n simpa using (hasDerivAt_id (0:ℂ)).const_add 1\n have h3 := h1.comp 0 h2\n -- h3 : HasDerivAt (hLi ∘ (1+·)) (1 * deriv hLi 1)?? comp: HasDerivAt (hLi ∘ g) (deriv hLi (g 0) * dg) — for ℂ→ℂ→ℂ: HasDerivAt.comp (hf : HasDerivAt f f' (g x)) (hg : HasDerivAt g g' x) : HasDerivAt (f ∘ g) (f' * g')? or g' • f'? For ℂ it's mul: (f' * g')? session-016 note: \"HasDerivAt.comp handles mixed fields via NormedAlgebra/IsScalarTower\" — for ℂ→ℂ: HasDerivAt.comp x hf hg : HasDerivAt (f ∘ g) x (g' * f')?? order matters for noncomm — for ℂ comm either. The exact form: h1.comp 0 h2 : HasDerivAt (hLi ∘ fun s => 1 + s) (1 * deriv hLi 1)?? — comp order: h1 : HasDerivAt hLi (deriv hLi 1) (at (1+0) = 1 ✓ since g 0 = 1 + 0 = 1); h1.comp 0 h2 : HasDerivAt (hLi ∘ (fun s => 1+s)) ((deriv hLi 1) * 1) 0 — simpa to deriv hLi 1.\n ...\n -- the slope tendsto\n have hslope : Tendsto (fun s : ℂ => (hLi (1 + s) - hLi 1) / s) (𝓝[≠] 0) (𝓝 (deriv hLi 1)) := by\n have := hasDerivAt_iff_tendsto_slope.mp hd\n simpa [slope_fun_def_field, sub_zero] using this\n -- (1 − hLi(1+s))/s = −(hLi(1+s) − hLi 1)/s on 𝓝[≠] 0: pointwise algebra + hLi_one\n have hev : (fun s : ℂ => (1 - hLi (1 + s)) / s) =ᶠ[𝓝[≠] 0] (fun s => -((hLi (1 + s) - hLi 1) / s)) := by\n filter_upwards [self_mem_nhdsWithin] with s hs\n rw [hLi_one]; ring\n rw [limUnder_congr hev] -- limUnder congr: f =ᶠ[l] g → limUnder l f = limUnder l g ✓ (`limUnder_congr`? or Filter.EventuallyEq.limUnder_eq? — there's `Filter.limUnder_congr`? hmm — `EventuallyEq.limUnder_eq`? — in LiResidue: `riemannZeta_residue_one.limUnder_eq` was used — that's Tendsto.limUnder_eq : Tendsto f l (𝓝 a) → limUnder l f = a ✓. For the congr: `limUnder_congr (h : f =ᶠ[l] g) : limUnder l f = limUnder l g`? — I believe `Filter.limUnder_congr` exists? or `EventuallyEq.limUnder_eq`? hmm — alternative: skip limUnder manipulation — prove the Tendsto directly: Tendsto (fun s => (1−hLi(1+s))/s) (𝓝[≠] 0) (𝓝 (−deriv hLi 1)) via hslope.neg + congr', then limUnder_eq. Let me restructure:\n have hT : Tendsto (fun s : ℂ => (1 - hLi (1 + s)) / s) (𝓝[≠] 0) (𝓝 (-deriv hLi 1)) := by\n apply hslope.neg.congr' -- hmm Tendsto.congr' direction — see session 017 note: f₁ =ᶠ f₂ → Tendsto f₁ → Tendsto f₂: here f₁ := the neg slope fun, f₂ := (1−hLi(1+s))/s: need (negslope) =ᶠ (target): hev.symm — hev : target =ᶠ negslope — wait I wrote hev : target =ᶠ[𝓝[≠] 0] negslope — hslope.neg : Tendsto negslope ... — Tendsto.congr' (hl : f₁ =ᶠ f₂) (h : Tendsto f₁) : Tendsto f₂ — with f₁ := target... I have h : Tendsto negslope — so need hl : negslope =ᶠ target := hev.symm ✓: hslope.neg.congr' hev.symm ✓.\n exact hT.limUnder_eq\n```\nOK. Then:\n\n```lean\ndef hLiExt : ℂ → ℂ := Function.update (fun s => (1 - hLi (1 + s)) / s) 0 (-deriv hLi 1)\n\nlemma hLiExt_zero : hLiExt 0 = -deriv hLi 1 := Function.update_self _ _ _\nlemma hLiExt_of_ne {s : ℂ} (hs : s ≠ 0) : hLiExt s = (1 - hLi (1 + s)) / s := Function.update_of_ne hs _ _\n\nlemma hLiExt_analyticAt_zero : AnalyticAt ℂ hLiExt 0 := by\n -- removable singularity pattern from zetaA_analyticAt_one\n -- need: a punctured ball where differentiable + bounded\n ...\n```\nFor the differentiability on a punctured ball: pick ε > 0 with zetaA w ≠ 0 for w ∈ ball 1 ε (from zetaA_ne_zero_near_one — ∀ᶠ w in 𝓝 1 — Metric.eventually_nhds_iff_ball or mem_nhds_iff: get ε). On ball 1 ε: hLi analytic: \n```lean\n have hball : ∀ᶠ w in 𝓝 (1:ℂ), AnalyticAt ℂ hLi w := hLi_analyticAt_one.eventually_analyticAt\n```\nOh nice — `AnalyticAt.eventually_analyticAt : AnalyticAt f z₀ → ∀ᶠ z in 𝓝 z₀, AnalyticAt f z` ✓ (used in the vendored code line 245 ✓). So hLi analytic on a ball around 1. Then for s ∈ ball 0 ε, s ≠ 0: 1+s ∈ ball 1 ε: (1 − hLi(1+s))/s differentiable: quotient of differentiable (1 − hLi(1+s): comp analytic ✓) by s (≠ 0) ✓.\n\nBounded: the Tendsto hT gives boundedness on a punctured nhd (isBigO_one → BddAbove on a smaller punctured ball — the zetaA proof used IsBigO_to_BddAbove... — zetaA's proof: obtained δ from the tendsto's Metric.tendsto_nhdsWithin_nhds directly with the bound 1, then BddAbove by 2 via the triangle — mirror that: hT : Tendsto ... (𝓝 (−deriv hLi 1)): take ε = 1: ∃ δ > 0, ∀ s ≠ 0, dist < δ ⟹ ‖(1−hLi(1+s))/s − (−deriv hLi 1)‖ < 1 ⟹ ‖...‖ ≤ ‖deriv hLi 1‖ + 1 — BddAbove by that. Then differentiableOn_update_limUnder_of_bddAbove (ball_mem_nhds 0 (δ/2)) hdiff hbd — gives DifferentiableOn (update ... 0 (limUnder ...)) on ball 0 (δ/2) — with the limUnder value = −deriv hLi 1 by hLiExt_lim — rw. Then .analyticOnNhd isOpen_ball at 0 ✓ — exactly zetaA's proof shape.\n\nLet me re-check zetaA_analyticAt_one's exact structure to clone (LiResidue lines 45-78): \n- hT := riemannZeta_residue_one (Tendsto form)\n- rw [Metric.tendsto_nhdsWithin_nhds] at hT; obtain ⟨δ, hδ0, hδ⟩ := hT 1 one_pos\n- hdiff : DifferentiableOn ℂ (fun w => (w−1)*ζ w) (ball 1 (δ/2) \\ {1})\n- hbd : BddAbove ((fun z => ‖(z−1)*ζ z‖) '' (ball 1 (δ/2) \\ {1})) — via the bound 2.\n- h := differentiableOn_update_limUnder_of_bddAbove (ball_mem_nhds 1 (δ/2)) hdiff hbd\n- hlim : limUnder (𝓝[≠] 1) ... = 1 := ...limUnder_eq; rw [hlim] at h\n- han := h.analyticOnNhd isOpen_ball; exact han 1 (mem_ball_self ...)\n\nSo mirror with hT := hLiExt_lim... — wait hLiExt_lim is a limUnder equality; I need the Tendsto form for the Metric.tendsto_nhdsWithin_nhds extraction: use hT (the Tendsto) directly. So structure:\n\n```lean\nlemma hLiExt_tendsto : Tendsto (fun s : ℂ => (1 - hLi (1 + s)) / s) (𝓝[≠] 0) (𝓝 (-deriv hLi 1)) := ...\n\nlemma hLiExt_analyticAt_zero : AnalyticAt ℂ hLiExt 0 := by\n have hT := hLiExt_tendsto\n rw [Metric.tendsto_nhdsWithin_nhds] at hT\n obtain ⟨δ, hδ0, hδ⟩ := hT 1 one_pos\n -- differentiability on ball 0 (δ/2) \\ {0}\n obtain ⟨ε, hε0, hε⟩ := ... hLi analytic ball around 1 (from eventually_analyticAt via Metric.eventually_nhds_iff...)\n have hdiff : DifferentiableOn ℂ (fun s => (1 - hLi (1 + s)) / s) (Metric.ball 0 (min (δ/2) ε) \\ {0}) := ...\n have hbd : BddAbove (...) := ⟨‖deriv hLi 1‖ + 1, ...⟩\n have h := differentiableOn_update_limUnder_of_bddAbove (Metric.ball_mem_nhds 0 (by positivity : (0:ℝ) < min (δ/2) ε)) hdiff hbd\n rw [hLiExt_lim] at h -- the update value in h is limUnder ... — hLiExt's update value is −deriv hLi 1 — need: the update in h uses limUnder — hLiExt uses −deriv hLi 1 — bridge via hLiExt_lim: h's function update ... 0 (limUnder ...) — rw [hLiExt_lim] at h turns limUnder into −deriv hLi 1 ✓ then h's function is exactly hLiExt ✓\n have han := h.analyticOnNhd Metric.isOpen_ball\n exact han 0 (Metric.mem_ball_self (by positivity))\n```\nWait — hLiExt is DEFINED with −deriv hLi 1 as the update value: hLiExt = update f 0 (−deriv hLi 1); the lemma gives DifferentiableOn (update f 0 (limUnder ...)) — with hLiExt_lim : limUnder = −deriv hLi 1 — rw [hLiExt_lim] at h: h : DifferentiableOn (update f 0 (−deriv hLi 1)) — and that's DEFINITIONALLY hLiExt — h : DifferentiableOn ℂ hLiExt (ball...) after defeq — `exact` or rw [hLiExt] at h? hLiExt is a def — the term `Function.update f 0 (−deriv hLi 1)` vs `hLiExt` — delta-eq — `show`-bridge or fold via `rw [← hLiExt]`? hmm: `rw [← hLiExt] at h`?? hLiExt's equation lemma: hLiExt = Function.update ... — rw [← hLiExt]... equation-lemma direction: rw [hLiExt] at h turns hLiExt into the update — I have the update and want hLiExt: `rw [← hLiExt]`?? Hmm — for defs, `rw [hLiExt]` uses the auto-equation hLiExt = update... — rewriting ← turns update... into hLiExt ✓ — hmm does the auto-equation work like that? For `def hLiExt : ℂ → ℂ := Function.update ...`, the equation lemma is `hLiExt.eq_def : hLiExt = Function.update ...` or `hLiExt.eq_...`. rw [← hLiExt] at h — should work if the equation lemma exists. Alternatively end with `exact han 0 ...` where han's type mentions the update-form and the goal has hLiExt — `exact` uses defeq ✓ — han 0 (...) : (update ...) ∈ ... wait — h.analyticOnNhd gives AnalyticOnNhd ℂ (update ...) (ball ...) — han 0 (mem) : AnalyticAt ℂ (update ...) 0 — goal: AnalyticAt ℂ hLiExt 0 — defeq ✓ exact works ✓. I'll rely on exact-defeq (it worked for zetaA: `exact han 1 (...)` — zetaA's proof ended exactly that way with zetaA's def ✓).\n\nThe function identity + Leibniz + comp bridge:\n```lean\nlemma hLiExt_mul_id : (fun s : ℂ => s * hLiExt s) = fun s => 1 - hLi (1 + s) := by\n funext s\n by_cases hs : s = 0\n · subst hs\n simp [hLiExt_zero, hLi_one] -- 0 * (−deriv hLi 1) = 0 and 1 − hLi 1 = 1 − 1 = 0\n · rw [hLiExt_of_ne hs]\n field_simp [hs] -- s * ((1 − hLi(1+s))/s) = 1 − hLi(1+s)\n -- field_simp might close; else: rw [mul_div_cancel₀ ...]\n```\nmul_div_cancel₀ : a ≠ 0 → a * (b / a) = b? `mul_div_cancel_left₀ (ha : a ≠ 0) : a * b / a = b` — our form: s * ((1−hLi)/s) = (1−hLi): `mul_div_cancel_right₀`? : a * b / a?? the term is s * ((1−hLi(1+s))/s) = s * (1−hLi(1+s)) / s — mul_div_cancel_left₀ (hs) : s * X / s = X — is the expression s * (X/s) or s*X/s? After rw [hLiExt_of_ne hs]: goal s * ((1 − hLi (1+s))/s) = 1 − hLi (1+s) — the form s * (X/s): mul_div_cancel_left₀'s LHS is a * b / a — parses (a*b)/a — s * (X/s) parses as s * (X/s) — HMul s (HDiv X s) — different from (s*X)/s — need reassociation: `rw [mul_div_assoc', ...]`? mul_div_assoc' : a * (b / c) = (a * b) / c ✓ then mul_div_cancel_left₀ hs : (s * X)/s = X ✓. So: rw [hLiExt_of_ne hs, mul_div_assoc', mul_div_cancel_left₀ _ hs]... mul_div_cancel_left₀ (b) (ha : a ≠ 0)? — earlier session found: mul_div_cancel_left₀ (b : M₀) {a : M₀} (ha : a ≠ 0) : a * b / a = b — explicit b first! So `mul_div_cancel_left₀ _ hs` ✓.\n\nHmm wait — simpler: `field_simp [hs]` closes s * ((1−hLi)/s) = 1−hLi directly (field_simp clears /s then rfl) ✓ try field_simp first.\n\nThen:\n```lean\nlemma iteratedDeriv_hLiExt (j : ℕ) :\n iteratedDeriv j hLiExt 0 = -(Nat.factorial j : ℂ) * lcoeff j := by\n have hcid : ContDiffAt ℂ (j + 1) (fun s : ℂ => s) 0 := contDiff_id.contDiffAt\n have hcE : ContDiffAt ℂ (j + 1) hLiExt 0 := hLiExt_analyticAt_zero.contDiffAt\n have h1 := iteratedDeriv_mul hcid hcE -- iteratedDeriv (j+1) ((fun s => s) * hLiExt) 0 = Σ ...\n -- LHS via the function identity\n have hfun : ((fun s : ℂ => s) * hLiExt) = fun s => 1 - hLi (1 + s) := by\n funext s\n show s * hLiExt s = 1 - hLi (1 + s) -- Pi.mul_apply defeq\n ... hLiExt_mul_id pointwise\n -- iteratedDeriv (j+1) (fun s => 1 − hLi(1+s)) 0 = −iteratedDeriv (j+1) hLi 1\n have hcomp : iteratedDeriv (j + 1) (fun s : ℂ => hLi (1 + s)) 0 = iteratedDeriv (j + 1) hLi 1 := by\n -- comp with (1 + ·) = (· + 1) = (· − (−1))\n have e := congr_fun (iteratedDeriv_comp_sub_const (j+1) hLi (-1 : ℂ)) 0\n -- e : iteratedDeriv (j+1) (hLi ∘ (· − −1)) 0 = iteratedDeriv (j+1) hLi (0 − −1) = iteratedDeriv (j+1) hLi 1\n simpa using e\n ...\n```\nHmm — iteratedDeriv_comp_sub_const's exact form — from A_iter: `congr_fun (iteratedDeriv_comp_sub_const i (fun w : ℂ => w ^ n) (1 : ℂ)) 1` : so iteratedDeriv_comp_sub_const (i) (f) (c) : iteratedDeriv i (f ∘ (· − c)) = fun x => iteratedDeriv i f (x − c) — a FUNCTION equality. With f := hLi, c := −1: hLi ∘ (· − −1) = fun s => hLi (s + 1) — and I need fun s => hLi (1 + s) — s + 1 vs 1 + s — comm! add_comm. So:\n```lean\n have hcomp : iteratedDeriv (j + 1) (fun s : ℂ => hLi (1 + s)) 0 = iteratedDeriv (j + 1) hLi 1 := by\n have e := congr_fun (iteratedDeriv_comp_sub_const (j + 1) hLi (-1 : ℂ)) 0\n -- e : iteratedDeriv (j+1) (hLi ∘ (· − −1)) 0 = iteratedDeriv (j+1) hLi (0 − −1)\n have e2 : (hLi ∘ (· - (-1 : ℂ))) = (fun s : ℂ => hLi (1 + s)) := by\n funext s\n simp [Function.comp_apply, sub_neg_eq_add, add_comm]\n rw [e2] at e\n simpa using e\n```\nsimpa: 0 − −1 = 1 normalization ✓.\n\nHmm — actually I realize I should double-check `iteratedDeriv_comp_sub_const`'s exact signature in Mathlib — A_iter used it successfully: `iteratedDeriv_comp_sub_const i (fun w : ℂ => w ^ n) (1 : ℂ)` — three explicit args (i, f, c) returning a function equality (congr_fun applied) ✓. \n\nThen the assembly:\n```lean\n -- iteratedDeriv (j+1) ((fun s => s) * hLiExt) 0 — via hfun → iteratedDeriv (j+1) (fun s => 1 − hLi(1+s)) 0 = −iteratedDeriv (j+1) hLi 1 (const deriv 0 + comp)\n have hLHS : iteratedDeriv (j + 1) ((fun s : ℂ => s) * hLiExt) 0 = -iteratedDeriv (j + 1) hLi 1 := by\n rw [hfun]\n have hconst : ContDiffAt ℂ (j+1) (fun s : ℂ => (1:ℂ)) 0 := contDiff_const.contDiffAt\n have hcompC : ContDiffAt ℂ (j+1) (fun s : ℂ => hLi (1 + s)) 0 := by\n -- analytic: hLi analytic at 1 = 1+0: comp\n have h1 : AnalyticAt ℂ hLi (1 + (0:ℂ)) := by simpa using hLi_analyticAt_one\n have h2 : AnalyticAt ℂ (fun s : ℂ => 1 + s) 0 := analyticAt_const.add analyticAt_id\n have h3 := h1.comp h2 -- AnalyticAt.comp : AnalyticAt f (g x) → AnalyticAt g x → AnalyticAt (f ∘ g) x\n -- (hLi ∘ (1+·)) vs (fun s => hLi (1+s)): defeq\n exact h3.contDiffAt\n rw [show (fun s : ℂ => 1 - hLi (1 + s)) = (fun s => (1:ℂ)) - (fun s => hLi (1 + s)) from by funext s; simp [Pi.sub_apply]]\n rw [iteratedDeriv_sub hconst hcompC]\n simp [hcomp] -- iteratedDeriv (j+1) (fun s => 1) 0 = 0 (j+1 ≥ 1: deriv of const)\n -- the RHS: iteratedDeriv_mul sum collapse\n ...\n```\n- `iteratedDeriv_sub` ✓ (used in A_iter).\n- iteratedDeriv (j+1) (fun s => 1) 0 = 0 for j+1 ≥ 1: `iteratedDeriv_const`? : iteratedDeriv n (fun _ => c) x = 0 for n ≥ 1? there should be `iteratedDeriv_const (c) (hn : n ≠ 0)?`... I recall `iteratedDeriv_const : iteratedDeriv n (fun _ => c) = 0`? with n ≠ 0 condition. simp should handle via `iteratedDeriv_succ` + deriv_const... let me use: have : iteratedDeriv (j+1) (fun s : ℂ => (1:ℂ)) 0 = 0 := by rw [iteratedDeriv_succ']; simp [iteratedDeriv_const?]... hmm — `iteratedDeriv_succ' : iteratedDeriv (n+1) f = deriv (iteratedDeriv n f)`? then deriv of the const-function-iteratedDeriv... iteratedDeriv j (fun _ => 1) is the constant zero FUNCTION for j ≥ 1 (inductively) — circular. There IS `iteratedDeriv_const (c : 𝔸) (hn : 0 < n)?: iteratedDeriv n (fun _ => c) = 0` — I'll trust something like iteratedDeriv_const exists with a positivity side or simp lemma `iteratedDeriv_const_of_ne_zero`? Alternatively: contDiff_const... simplest: `by simp` — simp lemmas: iteratedDeriv_const? Let me just try `simp` and fix if needed.\n\n- The Leibniz sum collapse: h1 : iteratedDeriv (j+1) ((fun s => s) * hLiExt) 0 = Σ_{i ∈ range (j+2)} (j+1).choose i * iteratedDeriv i (fun s => s) 0 * iteratedDeriv (j+1−i) hLiExt 0. iteratedDeriv i (fun s => s) 0: for i = 0: 0 (the value — (fun s => s) 0 = 0); i = 1: 1; i ≥ 2: 0. So the sum = the i = 1 term: (j+1).choose 1 * 1 * iteratedDeriv j hLiExt 0 = (j+1)·iteratedDeriv j hLiExt 0.\n In Lean: Finset.sum_eq_single 1: side goals: (i) other terms vanish: i ∈ range(j+2), i ≠ 1: i = 0: iteratedDeriv 0 (fun s => s) 0 = 0 — `iteratedDeriv_zero : iteratedDeriv 0 f = f` ✓ then (fun s => s) 0 = 0 — `by simp [iteratedDeriv_zero]`? hmm iteratedDeriv_zero : iteratedDeriv 0 f = f — then f 0 = 0 by rfl (id 0 = 0 — the function is fun s => s — applied 0 = 0 ✓ rfl/simp). i ≥ 2: iteratedDeriv i (fun s => s) 0 = 0: iteratedDeriv of id beyond 1: deriv id = const 1, higher = 0: there might be `iteratedDeriv_id`? or prove: iteratedDeriv i (fun s => s) 0 = 0 for i ≥ 2: via iteratedDeriv_succ' twice: iteratedDeriv 2 id = deriv (deriv id) = deriv (fun _ => 1) = 0... — a mini-lemma:\n ```lean\n have hid : ∀ i : ℕ, iteratedDeriv i (fun s : ℂ => s) 0 = if i = 1 then 1 else 0 := by\n intro i\n rcases i with _ | _ | i\n · simp [iteratedDeriv_zero] -- i = 0: (fun s => s) 0 = 0\n · simp [iteratedDeriv_one] -- i = 1: deriv (fun s => s) 0 = 1: iteratedDeriv_one : iteratedDeriv 1 f = deriv f; deriv_id''\n · -- i ≥ 2\n have : iteratedDeriv (i + 2) (fun s : ℂ => s) = fun _ => 0 := by\n induction i with\n | zero => -- iteratedDeriv 2 id: deriv (deriv id) = deriv (fun _ => 1) = 0\n funext s\n rw [iteratedDeriv_succ', iteratedDeriv_one, deriv_id'']\n simp\n | succ i ih => rw [iteratedDeriv_succ', ih]; simp\n rw [this]\n simp\n ```\n Hmm wait iteratedDeriv_succ' : iteratedDeriv (n+1) f = deriv (iteratedDeriv n f)? or iteratedDeriv (n+1) f x = deriv (iteratedDeriv n f) x — roughly ✓ (there's iteratedDeriv_succ and iteratedDeriv_succ' — one is deriv (iteratedDeriv n f), the other iteratedDeriv n (deriv f)). For i = 2: iteratedDeriv 2 (fun s => s) = deriv (iteratedDeriv 1 (fun s => s)) [succ'] = deriv (deriv (fun s => s)) [iteratedDeriv_one] = deriv (fun _ => 1) [deriv_id''] = 0 [deriv_const] — funext s; simp [iteratedDeriv_succ', iteratedDeriv_one, deriv_id''] — should work with care.\n\n This is getting long but standard. Then sum_eq_single 1: 1 ∈ range(j+2) ✓ (j ≥ 0 ⟹ 1 < j+2 ✓); the i = 1 term: (j+1).choose 1 * iteratedDeriv 1 (fun s => s) 0 * iteratedDeriv j hLiExt 0 = (j+1)·1·iteratedDeriv j hLiExt 0 — Nat.choose_one_right ✓ cast; iteratedDeriv 1 (fun s => s) 0 = 1 via hid (if_pos rfl) ✓.\n Conclude: iteratedDeriv (j+1) ((fun s => s)*hLiExt) 0 = (j+1)·iteratedDeriv j hLiExt 0. Combined with hLHS: (j+1)·iteratedDeriv j hLiExt 0 = −iteratedDeriv (j+1) hLi 1. So iteratedDeriv j hLiExt 0 = −iteratedDeriv (j+1) hLi 1/(j+1) — and lcoeff j = iteratedDeriv (j+1) hLi 1/(j+1)! — so iteratedDeriv (j+1) hLi 1 = (j+1)!·lcoeff j — then iteratedDeriv j hLiExt 0 = −(j+1)!·lcoeff j/(j+1) = −j!·lcoeff j ✓ (factorial: (j+1)! = (j+1)·j! — `Nat.factorial_succ` ✓).\n \n Cast management: the goal is `iteratedDeriv j hLiExt 0 = -(Nat.factorial j : ℂ) * lcoeff j`. From (j+1 : ℂ)·X = −Y with X := iteratedDeriv j hLiExt 0, Y := iteratedDeriv (j+1) hLi 1: X = −Y/(j+1) — field_simp with (j+1 : ℂ) ≠ 0 (Nat.cast — j+1 ≥ 1 ✓ `Nat.cast_ne_zero`); Y = ((j+1)! : ℂ)·lcoeff j (from lcoeff's def: lcoeff j = Y/(j+1)! — `lcoeff` def: iteratedDeriv (j+1) hLi 1 / (j+1)! — so Y = (j+1)!·lcoeff j via div_mul_cancel... `(j+1)!` cast ✓ nonzero ✓). Then X = −((j+1)!)·lcoeff j/(j+1) = −j!·lcoeff j via (j+1)! = (j+1)·j! ✓ field_simp/ring.\n\nOK — this is a well-defined ~150-line file. One concern: `iteratedDeriv_mul` signature — from LiResidue's ResW1_eq_sum: `iteratedDeriv_mul hA hh` with hA hh : ContDiffAt ℂ n f 1 — the sum form: `∑ i ∈ Finset.range (n + 1), n.choose i * iteratedDeriv i f 1 * iteratedDeriv (n - i) g 1` ✓ (from the hmul in ResW1_eq_sum) ✓.\n\nAnother: `h1.comp 0 h2` for HasDerivAt comp — the mixed-field chain rule: session-016 note says HasDerivAt.comp handles ℂ→ℂ→ℂ via the algebra tower. The form: HasDerivAt.comp (x) (hf : HasDerivAt f f' (g x)) (hg : HasDerivAt g g' x) : HasDerivAt (f ∘ g) (g' • f')? — for ℂ→ℂ: the result's derivative is f' * g'? or g' * f'? — LiPrincipal's HIntegral_deriv used `h1.comp x h2` then `rw [mul_one] at hcomp` — so the comp gives (dg)•(df) or (df·dg) with a * 1 — the mul_one suggests the form (deriv G ...) * 1 — i.e. HasDerivAt (G ∘ path) (deriv G (...) * 1) — so it's df * dg order: HasDerivAt (f ∘ g) x (f' * g')? Hmm — for HIntegral_deriv: h1 : HasDerivAt G (deriv G p) p; h2 : HasDerivAt path 1 x; hcomp := h1.comp x h2 : HasDerivAt (G ∘ path) ((deriv G p) * 1)?? then mul_one — yes it gave f' * g' = deriv G p * 1 ✓. For my case: h1 : HasDerivAt hLi (deriv hLi 1) 1; h2 : HasDerivAt (fun s => 1 + s) 1 0; h3 := h1.comp 0 h2 : HasDerivAt (hLi ∘ (fun s => 1 + s)) ((deriv hLi 1) * 1) 0 — then mul_one → deriv hLi 1 ✓. But wait — h1's point is 1 and g 0 = 1 + 0 = 1 ✓ matches. And the composition hLi ∘ (fun s => 1 + s) vs my lambda fun s => hLi (1 + s) — defeq ✓ (comp_apply simp).\n\nAlso the eventual neighborhoods: for hLiExt_tendsto's hslope — hasDerivAt_iff_tendsto_slope.mp hd : Tendsto (slope (fun s => hLi (1+s)) 0) (𝓝[≠] 0) (𝓝 (deriv hLi 1)) — slope f a = fun x => (f x − f a)/(x − a) — at a = 0: (hLi(1+s) − hLi(1+0))/s — hLi(1+0) = hLi 1 ✓ — simpa [slope_fun_def_field, ...] using this — the slope_fun_def_field : slope f a = fun x => (f x − f a)/(x − a) ✓ — with the (1+0) → 1 normalization via simp ✓.\n\nOK — I'm confident in the plan. Also note — lcoeff's def has `/ (k+1)!` with the Nat factorial cast — from LiResidue: `def lcoeff (k : ℕ) : ℂ := iteratedDeriv (k + 1) hLi 1 / (k + 1)!` ✓.\n\nLet me also reconsider whether to include the H₁ext = \"1/s + ζ′/ζ(1+s)\" READING (the actual piece-B statement for the assembly): the assembly needs: the meromorphic function 1/s + ζ′/ζ(1+s) has Taylor coefficients −c_j at 0 — with my hLiExt: hLiExt(s) = (1 − hLi(1+s))/s — and (1 − hLi(1+s))/s = (1 + s·ζ′/ζ(1+s))/s = 1/s + ζ′/ζ(1+s) for s ≠ 0 near 0 (ζ(1+s) ≠ 0 eventually — from riemannZeta_residue_one.eventually_ne transported to s near 0: w = 1+s). So hLiExt =ᶠ[𝓝[≠] 0] (fun s => 1/s + ζ′/ζ(1+s))... wait — hLi(1+s) = (1+s−1)(−ζ′/ζ(1+s)) = s·(−ζ′/ζ(1+s)) for 1+s ≠ 1 (s ≠ 0) and ζ(1+s) ≠ 0 — via hLi_eq_of_ne (needs w ≠ 1 ∧ ζ w ≠ 0) ✓. So (1 − hLi(1+s))/s = (1 + s·ζ′/ζ(1+s))/s = 1/s + ζ′/ζ(1+s) ✓ — the reading lemma:\n```lean\nlemma hLiExt_eq_near_zero : ∀ᶠ s in 𝓝[≠] (0:ℂ), hLiExt s = 1/s + deriv riemannZeta (1+s) / riemannZeta (1+s) := by\n -- from hLi_eq_of_ne + riemannZeta_residue_one.eventually_ne transported\n```\nThis connects the abstract hLiExt to the actual ζ′/ζ — the assembly will need it. Include it.\n\nThe transport: ζ(1+s) ≠ 0 for s ∈ 𝓝[≠] 0 small: from riemannZeta_residue_one.eventually_ne : ∀ᶠ w in 𝓝[≠] 1, (w−1)·ζ w ≠ 0 — as a statement about w near 1 — I need it about s = w−1 near 0: Tendsto (fun s => 1 + s) (𝓝[≠] 0) (𝓝[≠] 1)?? — the map s ↦ 1+s sends 𝓝[≠] 0 into 𝓝[≠] 1 (continuous, 1+0 = 1, and s ≠ 0 ⟹ 1+s ≠ 1 ✓): `Tendsto (fun s => 1+s) (𝓝[≠] 0) (𝓝[≠] 1)` — via `tendsto_nhdsWithin_...`? There's tendsto_nhdsWithin_of... the composition: (fun s => 1+s) — Tendsto to 𝓝 1 ✓ (continuous) and maps {0}ᶜ into {1}ᶜ ✓ (s ≠ 0 ⟹ 1+s ≠ 1 by add_right... 1+s = 1 ⟺ s = 0 ✓ add_left_cancel). So `Filter.Tendsto.eventually`... h : ∀ᶠ w in 𝓝[≠] 1, p w and the map tends to 𝓝[≠] 1 ⟹ ∀ᶠ s in 𝓝[≠] 0, p (1+s) — `Tendsto.eventually (h : Tendsto f l₁ l₂) (hp : ∀ᶠ y in l₂, p y) : ∀ᶠ x in l₁, p (f x)` ✓ exists. The map-tendsto: Tendsto (fun s => 1+s) (𝓝[≠] 0) (𝓝[≠] 1): `tendsto_nhdsWithin` needs (Tendsto f (𝓝 0) (𝓝 1)) ∧ (maps {0}ᶜ into {1}ᶜ): `tendsto_nhdsWithin_iff : Tendsto f (𝓝[s] x) (𝓝[t] y) ↔ Tendsto f (𝓝 x) (𝓝 y) ∧ ∀ᶠ x' in 𝓝[s] x, f x' ∈ t` ✓. Continuous part: (continuousAt_const.add continuousAt_id... (1 + s): ContinuousAt (fun s => 1 + s) 0 — `continuousAt_const.add continuousAt_id` — gives Tendsto ... (𝓝 (1 + 0)) = 𝓝 1 ✓ simp. The mapsTo: ∀ᶠ s in 𝓝[≠] 0, 1 + s ∈ {1}ᶜ — from self_mem_nhdsWithin: s ≠ 0 ⟹ 1 + s ≠ 1 ✓.\n\nOK. Writing the file now. Name: LiZetaCoeff.lean.","signature":""},{"type":"text","text":"Now piece (B) — the ζ-piece coefficient reading. New file `LiZetaCoeff.lean`."},{"type":"tool_use","id":"Write_190","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiZetaCoeff.lean","content":"/-\nNguyenRH1/LiZetaCoeff.lean — tier ii′ sub-stage ii′-3a, piece (B)\n(D-066 §2): the ζ-piece of the (4.10) coefficient split.\n\nThe meromorphic function 1/s + ζ′/ζ(1+s) is analytic at s = 0 (the pole\ncancels: −ζ′/ζ(1+s) = 1/s + Σ_j c_j s^j), and its j-th Taylor coefficient\nat 0 is −c_j = −lcoeff j. We package this as the analytic function\n\n hLiExt s := (1 − hLi (1+s)) / s [extended by −deriv hLi 1 at 0]\n\n(since hLi(1+s) = s·(−ζ′/ζ(1+s)) punctured near 0 by `hLi_eq_near_one`,\nhLiExt = 1/s + ζ′/ζ(1+s) on a punctured neighbourhood —\n`hLiExt_eq_near_zero`) and prove\n\n **iteratedDeriv j hLiExt 0 = −(j!)·lcoeff j**\n\n— by the exact function identity s·hLiExt s = 1 − hLi(1+s)\n(`hLiExt_mul_id`), the Leibniz collapse (iteratedDeriv_mul with the\nidentity factor killing all but the i = 1 term), and the comp bridge\niteratedDeriv (j+1) (hLi(1+·)) 0 = iteratedDeriv (j+1) hLi 1.\n\nArchive references: D-066 (route β4, piece B), D-064, journal-019.\n-/\nimport Mathlib\nimport NguyenRH1.LiResidue\n\nopen Zeta23 Complex Filter Topology\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. The limit value at 0 -/\n\n/-- The slope limit: (1 − hLi(1+s))/s → −deriv hLi 1 as s → 0, s ≠ 0. -/\nlemma hLiExt_tendsto :\n Tendsto (fun s : ℂ => (1 - hLi (1 + s)) / s) (𝓝[≠] 0) (𝓝 (-deriv hLi 1)) := by\n have hd : HasDerivAt (fun s : ℂ => hLi (1 + s)) (deriv hLi 1) 0 := by\n have h1 : HasDerivAt hLi (deriv hLi 1) 1 := hLi_analyticAt_one.differentiableAt.hasDerivAt\n have h2 : HasDerivAt (fun s : ℂ => 1 + s) 1 0 := by\n simpa using (hasDerivAt_id (0 : ℂ)).const_add 1\n have h3 := h1.comp 0 h2\n rw [mul_one] at h3\n have h4 : (hLi ∘ fun s : ℂ => 1 + s) = fun s : ℂ => hLi (1 + s) := rfl\n rw [h4] at h3\n exact h3\n have hslope : Tendsto (fun s : ℂ => (hLi (1 + s) - hLi 1) / s) (𝓝[≠] 0)\n (𝓝 (deriv hLi 1)) := by\n have h := hasDerivAt_iff_tendsto_slope.mp hd\n simpa [slope_fun_def_field] using h\n have hev : (fun s : ℂ => -((hLi (1 + s) - hLi 1) / s)) =ᶠ[𝓝[≠] 0]\n (fun s => (1 - hLi (1 + s)) / s) := by\n filter_upwards [self_mem_nhdsWithin] with s hs\n rw [hLi_one]\n ring\n exact hslope.neg.congr' hev\n\n/-! ## 2. hLiExt: the analytic extension -/\n\n/-- hLiExt s := (1 − hLi(1+s))/s, extended by −deriv hLi 1 at 0 — the\nanalytic-at-0 form of 1/s + ζ′/ζ(1+s) (`hLiExt_eq_near_zero`). -/\ndef hLiExt : ℂ → ℂ := Function.update (fun s => (1 - hLi (1 + s)) / s) 0 (-deriv hLi 1)\n\nlemma hLiExt_zero : hLiExt 0 = -deriv hLi 1 := Function.update_self _ _ _\n\nlemma hLiExt_of_ne {s : ℂ} (hs : s ≠ 0) : hLiExt s = (1 - hLi (1 + s)) / s :=\n Function.update_of_ne hs _ _\n\n/-- hLiExt is analytic at 0 (removable singularity; the limit exists by\n`hLiExt_tendsto`). Mirrors `zetaA_analyticAt_one`. -/\nlemma hLiExt_analyticAt_zero : AnalyticAt ℂ hLiExt 0 := by\n have hT := hLiExt_tendsto\n rw [Metric.tendsto_nhdsWithin_nhds] at hT\n obtain ⟨δ, hδ0, hδ⟩ := hT 1 one_pos\n -- hLi is analytic on a ball around 1\n have hball : ∀ᶠ w in 𝓝 (1 : ℂ), AnalyticAt ℂ hLi w :=\n hLi_analyticAt_one.eventually_analyticAt\n rw [Metric.eventually_nhds_iff_ball] at hball\n obtain ⟨ε, hε0, hε⟩ := hball\n -- differentiability on a punctured ball around 0\n have hdiff : DifferentiableOn ℂ (fun s => (1 - hLi (1 + s)) / s)\n (Metric.ball 0 (min (δ / 2) ε) \\ {0}) := by\n intro s hs\n have hs0 : s ≠ 0 := hs.2\n have hs1 : (1 + s) ∈ Metric.ball 1 ε := by\n have hds : dist s 0 < ε := lt_of_lt_of_le hs.1 (min_le_right _ _)\n rw [Metric.mem_ball, dist_zero_right] at hds\n rw [Metric.mem_ball]\n have : (1 + s) - 1 = s := by ring\n rw [this]\n exact hds\n have ha : AnalyticAt ℂ hLi (1 + s) := hε (1 + s) hs1\n have hnum : DifferentiableAt ℂ (fun s : ℂ => 1 - hLi (1 + s)) s := by\n have hcomp : AnalyticAt ℂ hLi (1 + s) := ha\n have hpath : AnalyticAt ℂ (fun s : ℂ => 1 + s) s :=\n analyticAt_const.add analyticAt_id\n have h := hcomp.comp hpath\n have heq : (hLi ∘ fun s : ℂ => 1 + s) = fun s : ℂ => hLi (1 + s) := rfl\n rw [heq] at h\n exact analyticAt_const.sub h |>.differentiableAt\n exact hnum.div (differentiableAt_id) hs0 |>.differentiableWithinAt\n -- boundedness on the punctured ball\n have hbd : BddAbove ((fun s => ‖(1 - hLi (1 + s)) / s‖) ''\n (Metric.ball 0 (min (δ / 2) ε) \\ {0})) := by\n refine ⟨‖deriv hLi 1‖ + 1, ?_⟩\n rintro _ ⟨s, hs, rfl⟩\n have hs0 : s ≠ 0 := hs.2\n have hds : dist s 0 < δ := by\n have := hs.1\n rw [Metric.mem_ball] at this\n have h2 : dist s 0 < min (δ / 2) ε := this\n have h3 : min (δ / 2) ε ≤ δ / 2 := min_le_left _ _\n linarith [h2, h3, hδ0]\n have h1 := hδ (Set.mem_compl_singleton_iff.mpr hs0) hds\n rw [dist_eq_norm] at h1\n have h2 : ‖(1 - hLi (1 + s)) / s‖ ≤ ‖(1 - hLi (1 + s)) / s - (-deriv hLi 1)‖ +\n ‖(-deriv hLi 1 : ℂ)‖ := by\n nth_rewrite 1 [show (1 - hLi (1 + s)) / s =\n ((1 - hLi (1 + s)) / s - (-deriv hLi 1)) + (-deriv hLi 1) from by ring]\n exact norm_add_le _ _\n rw [norm_neg] at h2\n linarith [h1, h2]\n have h := differentiableOn_update_limUnder_of_bddAbove\n (Metric.ball_mem_nhds 0 (by positivity : (0 : ℝ) < min (δ / 2) ε)) hdiff hbd\n have hlim : limUnder (𝓝[≠] (0 : ℂ)) (fun s => (1 - hLi (1 + s)) / s) = -deriv hLi 1 :=\n hLiExt_tendsto.limUnder_eq\n rw [hlim] at h\n have han := h.analyticOnNhd Metric.isOpen_ball\n exact han 0 (Metric.mem_ball_self (by positivity : (0 : ℝ) < min (δ / 2) ε))\n\n/-! ## 3. The function identity and the coefficient reading -/\n\n/-- The exact global identity s·hLiExt s = 1 − hLi(1+s). -/\nlemma hLiExt_mul_id : (fun s : ℂ => s) * hLiExt = fun s => 1 - hLi (1 + s) := by\n funext s\n by_cases hs : s = 0\n · subst hs\n rw [hLiExt_zero, hLi_one]\n simp\n · rw [hLiExt_of_ne hs]\n show s * ((1 - hLi (1 + s)) / s) = 1 - hLi (1 + s)\n rw [mul_div_assoc', mul_div_cancel_left₀ _ hs]\n\n/-- The comp bridge: iterated derivatives of hLi(1+·) at 0 = those of hLi at 1. -/\nlemma iteratedDeriv_hLi_one_add (m : ℕ) :\n iteratedDeriv m (fun s : ℂ => hLi (1 + s)) 0 = iteratedDeriv m hLi 1 := by\n have e := congr_fun (iteratedDeriv_comp_sub_const m hLi (-1 : ℂ)) 0\n have e2 : (hLi ∘ (· - (-1 : ℂ))) = (fun s : ℂ => hLi (1 + s)) := by\n funext s\n simp [Function.comp_apply, sub_neg_eq_add, add_comm]\n rw [e2] at e\n simpa using e\n\n/-- **Piece (B)** (D-066 §2): the Taylor coefficients of hLiExt at 0 are\n−j!·lcoeff j — i.e. 1/s + ζ′/ζ(1+s) has j-th coefficient −c_j. -/\ntheorem iteratedDeriv_hLiExt (j : ℕ) :\n iteratedDeriv j hLiExt 0 = -(Nat.factorial j : ℂ) * lcoeff j := by\n have hcid : ContDiffAt ℂ (j + 1) (fun s : ℂ => s) 0 := contDiff_id.contDiffAt\n have hcE : ContDiffAt ℂ (j + 1) hLiExt 0 := hLiExt_analyticAt_zero.contDiffAt\n have h1 := iteratedDeriv_mul hcid hcE\n -- LHS via the function identity\n have hLHS : iteratedDeriv (j + 1) ((fun s : ℂ => s) * hLiExt) 0 =\n -iteratedDeriv (j + 1) hLi 1 := by\n rw [hLiExt_mul_id]\n have hconst : ContDiffAt ℂ (j + 1) (fun s : ℂ => (1 : ℂ)) 0 := contDiff_const.contDiffAt\n have hcompC : ContDiffAt ℂ (j + 1) (fun s : ℂ => hLi (1 + s)) 0 := by\n have h1a : AnalyticAt ℂ hLi (1 + (0 : ℂ)) := by simpa using hLi_analyticAt_one\n have h2a : AnalyticAt ℂ (fun s : ℂ => 1 + s) 0 := analyticAt_const.add analyticAt_id\n have h3 := h1a.comp h2a\n have heq : (hLi ∘ fun s : ℂ => 1 + s) = fun s : ℂ => hLi (1 + s) := rfl\n rw [heq] at h3\n exact h3.contDiffAt\n rw [show (fun s : ℂ => 1 - hLi (1 + s)) = (fun s => (1 : ℂ)) - (fun s => hLi (1 + s))\n from by funext s; simp [Pi.sub_apply]]\n rw [iteratedDeriv_sub hconst hcompC]\n have hconst' : iteratedDeriv (j + 1) (fun s : ℂ => (1 : ℂ)) 0 = 0 := by\n have hj : j + 1 ≠ 0 := by omega\n exact iteratedDeriv_const hj _\n rw [hconst', zero_sub, iteratedDeriv_hLi_one_add]\n -- RHS: the Leibniz sum collapses to the i = 1 term\n have hid : ∀ i : ℕ, iteratedDeriv i (fun s : ℂ => s) 0 = if i = 1 then 1 else 0 := by\n intro i\n rcases i with _ | _ | i\n · simp [iteratedDeriv_zero]\n · simp [iteratedDeriv_one, deriv_id'']\n · have h2 : iteratedDeriv (i + 2) (fun s : ℂ => s) = fun _ => (0 : ℂ) := by\n induction i with\n | zero =>\n funext s\n rw [iteratedDeriv_succ', iteratedDeriv_one, deriv_id'']\n simp\n | succ i ih =>\n rw [iteratedDeriv_succ', ih]\n simp\n rw [h2]\n simp\n have hsum : iteratedDeriv (j + 1) ((fun s : ℂ => s) * hLiExt) 0 =\n (j + 1 : ℂ) * iteratedDeriv j hLiExt 0 := by\n rw [h1]\n rw [Finset.sum_eq_single 1]\n · rw [hid 1, if_pos rfl]\n simp [Nat.choose_one_right]\n · intro i hi hi1\n rw [Finset.mem_range] at hi\n rw [hid i, if_neg hi1]\n simp\n · intro h1'\n rw [Finset.mem_range] at h1'\n omega\n -- combine\n rw [hsum] at hLHS\n -- (j+1)·iteratedDeriv j hLiExt 0 = −iteratedDeriv (j+1) hLi 1\n have hlc : iteratedDeriv (j + 1) hLi 1 = ((j + 1)! : ℂ) * lcoeff j := by\n rw [lcoeff]\n have hf : ((j + 1)! : ℂ) ≠ 0 := by simp [Nat.factorial_ne_zero]\n rw [show ((j + 1) ! : ℂ) = (Nat.factorial (j + 1) : ℂ) from rfl]\n field_simp [hf]\n rw [hlc] at hLHS\n have hj1 : ((j + 1 : ℕ) : ℂ) ≠ 0 := by\n simp [Nat.cast_ne_zero]\n have hjs : ((j + 1)! : ℂ) = (j + 1) * (j ! : ℂ) := by\n rw [Nat.factorial_succ]\n simp [Nat.cast_mul, Nat.factorial]\n rw [hjs] at hLHS\n -- (j+1)·X = −(j+1)·j!·lcoeff j ⟹ X = −j!·lcoeff j\n have hcancel : (j + 1 : ℂ) * iteratedDeriv j hLiExt 0 =\n (j + 1 : ℂ) * (-(Nat.factorial j : ℂ) * lcoeff j) := by\n rw [hLHS]\n ring\n exact mul_left_cancel₀ hj1 hcancel\n\n/-! ## 4. The reading as 1/s + ζ′/ζ(1+s) -/\n\n/-- On a punctured neighbourhood of 0, hLiExt s = 1/s + ζ′/ζ(1+s). -/\nlemma hLiExt_eq_near_zero :\n ∀ᶠ s in 𝓝[≠] (0 : ℂ),\n hLiExt s = 1 / s + deriv riemannZeta (1 + s) / riemannZeta (1 + s) := by\n -- ζ(1+s) ≠ 0 on a punctured nhd of 0 (transport of residue_one.eventually_ne)\n have hne1 : ∀ᶠ w in 𝓝[≠] (1 : ℂ), riemannZeta w ≠ 0 := by\n have h := riemannZeta_residue_one.eventually_ne (show (1 : ℂ) ≠ 0 by norm_num)\n filter_upwards [h] with w hw\n have h2 := hw\n simp only [ne_eq, mul_eq_zero] at h2\n push Not at h2\n exact h2.2\n have hmap : Tendsto (fun s : ℂ => 1 + s) (𝓝[≠] (0 : ℂ)) (𝓝[≠] (1 : ℂ)) := by\n rw [tendsto_nhdsWithin_iff]\n refine ⟨?_, ?_⟩\n · have hc : ContinuousAt (fun s : ℂ => 1 + s) 0 :=\n continuousAt_const.add continuousAt_id\n simpa using hc.tendsto\n · filter_upwards [self_mem_nhdsWithin] with s hs\n intro hcontra\n exact hs (by simpa using hcontra)\n have hne : ∀ᶠ s in 𝓝[≠] (0 : ℂ), riemannZeta (1 + s) ≠ 0 := hmap.eventually hne1\n filter_upwards [hne, self_mem_nhdsWithin] with s hs0 hs\n have hs1 : (1 : ℂ) + s ≠ 1 := by\n intro h\n exact hs (by linarith [h] |>.symm ▸ (by simp : (0:ℂ) = 0) |> fun x => x)\n sorry_replace\n sorry\n"},"extra_content":null}]