← Session 22 — ii′-1: liCoeff pairing fix + residue machinery
thinking (7075 chars)
Clean. Now Section 4: the analyticity of DinfC on dpsiDomain + the cast bridge + the identity principle. Let me write it.
```lean
/-! ## 4. Analyticity and the identity with Complex.digamma -/
/-- The series converges uniformly on dpsiDomain (M-test with Σ 1/(m+1)²). -/
lemma dpsiTermC_hasSumUniformlyOn :
HasSumUniformlyOn dpsiTermC (fun s => ∑' m : ℕ, dpsiTermC s m) dpsiDomain := by
apply HasSumUniformlyOn.of_norm_le_summable (summable_div_add_one_sq 1)
intro m s hs
-- ‖dpsiTermC s m‖ ≤ 1/(m+1)² for s ∈ dpsiDomain
have hsm : s + m + 1 ≠ 0 := dpsiTermC_pole_free hs m
have hre : 0 < s.re := dpsiDomain_re_pos hs
rw [dpsiTermC_eq m hsm]
rw [norm_div]
have hden : ((m : ℝ) + 1) * ((m : ℝ) + 1) ≤ ‖((m : ℂ) + 1) * (s + ↑m + 1)‖ := by
... same as in summable
have hs1 : ‖s‖ < 1 := by
have h := hs
rw [dpsiDomain, Metric.mem_ball, dist_eq_norm] at h
calc ‖s‖ ≤ ‖s - (1:ℂ)/2‖ + ‖((1:ℂ)/2)‖ := norm_sub_le _ _
_ < 1/2 + 1/2 := by ... ‖(1:ℂ)/2‖ = 1/2
_ = 1 := by ring
...
```
Hmm — the norm of (1:ℂ)/2: ‖(1:ℂ)/2‖ = 1/2 — `by simp`? — norm_div, norm_one, norm_two... Let me include: have h12 : ‖((1:ℂ)/2)‖ = 1/2 := by rw [norm_div, norm_one]; norm_num — hmm ‖(2:ℂ)‖ = 2: `Complex.norm_two`? or norm_num... there's `norm_two : ‖(2:ℂ)‖ = 2`? probably `Complex.norm_two`? hmm. Actually — h4's goal — ‖s‖/(‖m+1‖·‖s+m+1‖) ≤ 1/(m+1)² — since ‖s‖ < 1 and the denominator ≥ (m+1)²: ‖s‖/D ≤ 1/D·... — hmm need care: ‖s‖/D ≤ 1/(m+1)² with D ≥ (m+1)² and ‖s‖ ≤ 1: ‖s‖/D ≤ ‖s‖/(m+1)² ≤ 1/(m+1)² ✓ two steps.
Then the differentiability: TendstoLocallyUniformlyOn.differentiableOn:
```lean
lemma DinfC_analyticOn : AnalyticOnNhd ℂ DinfC dpsiDomain := by
have hunif := dpsiTermC_hasSumUniformlyOn
have htend : TendstoLocallyUniformlyOn
(fun t : Finset ℕ => fun s => ∑ m ∈ t, dpsiTermC s m)
(fun s => ∑' m : ℕ, dpsiTermC s m) atTop dpsiDomain :=
hasSumUniformlyOn_iff_tendstoUniformlyOn.mp hunif -- hmm — that's TendstoUniformlyOn — need the Locally version
...
```
hasSumUniformlyOn_iff_tendstoUniformlyOn.mp hunif : TendstoUniformlyOn (partial sums) (tsum-fn) atTop dpsiDomain — then to TendstoLocallyUniformlyOn: `TendstoUniformlyOn.tendstoLocallyUniformlyOn`? — there might be a lemma — or: since dpsiDomain is open, TendstoUniformlyOn on it implies TendstoLocallyUniformlyOn — hmm — TendstoLocallyUniformlyOn means: every point has a nhd (within s) where uniform — from uniform-on-all-of-s: the whole s is such a nhd (s ∈ 𝓝[s] x ✓ self_mem_nhdsWithin) — there's probably `TendstoUniformlyOn.tendstoLocallyUniformlyOn` — let me assume/find.
Then TendstoLocallyUniformlyOn.differentiableOn htend (hF : ∀ᶠ t, DifferentiableOn ℂ (partial t) dpsiDomain): the partial sums are differentiable on dpsiDomain (each term differentiable: 1/(↑m+1) const + −1/(s+↑m+1) differentiable (s+↑m+1 ≠ 0 on the domain ✓ pole_free)) ✓ → DifferentiableOn ℂ (tsum-fn) dpsiDomain — then DinfC = −γ − 1/s + tsum-fn: DifferentiableOn (−γ − 1/s part: 1/s differentiable on dpsiDomain — 0 ∉ domain: s ≠ 0 from re > 0 ✓) — then `.analyticOnNhd dpsiDomain_isOpen`? — DifferentiableOn.analyticOnNhd (h : DifferentiableOn ℂ f s) (hs : IsOpen s) ✓.
The digamma side:
```lean
lemma digamma_analyticOn : AnalyticOnNhd ℂ Complex.digamma dpsiDomain := by
intro s hs
have hsG : Complex.Gamma s ≠ 0 := by
apply Complex.Gamma_ne_zero
intro m
intro hmeq -- s = −↑m
have hre : 0 < s.re := dpsiDomain_re_pos hs
rw [hmeq] at hre
simp at hre -- (−↑m).re = −↑m: 0 < −↑m — contradiction with ↑m ≥ 0
have hm : (0 : ℝ) ≤ (m : ℝ) := Nat.cast_nonneg m
linarith
have hdif : DifferentiableAt ℂ Complex.Gamma s := by
apply Complex.differentiableAt_Gamma
intro m hmeq
have hre : 0 < s.re := dpsiDomain_re_pos hs
rw [hmeq] at hre
simp at hre
have hm : (0 : ℝ) ≤ (m : ℝ) := Nat.cast_nonneg m
linarith
-- digamma = deriv Gamma / Gamma — analytic at s via the quotient
have hGammaAn : AnalyticAt ℂ Complex.Gamma s := by
-- from differentiableAt on a nhd: DifferentiableOn on dpsiDomain then analyticOnNhd
...
```
Hmm — AnalyticAt ℂ Complex.Gamma s from DifferentiableAt — NOT directly (pointwise differentiability ≠ analyticity at the point without a nhd) — BUT Gamma is differentiable on the open dpsiDomain ∋ s — so AnalyticOnNhd ℂ Gamma dpsiDomain via DifferentiableOn.analyticOnNhd — then AnalyticAt at s (AnalyticOnNhd.mem — `AnalyticOnNhd` def: ∀ x ∈ s, AnalyticAt f x — so from DifferentiableOn ℂ Gamma dpsiDomain: intro each point — differentiableAt_Gamma ✓ each point of dpsiDomain). So:
```lean
have hGammaAn : AnalyticOnNhd ℂ Complex.Gamma dpsiDomain := by
apply DifferentiableOn.analyticOnNhd _ dpsiDomain_isOpen
intro z hz
exact (Complex.differentiableAt_Gamma z (fun m => by
intro hmeq
have hre : 0 < z.re := dpsiDomain_re_pos hz
rw [hmeq] at hre
simp at hre
have hm : (0 : ℝ) ≤ (m : ℝ) := Nat.cast_nonneg m
linarith)).differentiableWithinAt
-- digamma = logDeriv Gamma = deriv Gamma / Gamma
have hdig : Complex.digamma = fun s => deriv Complex.Gamma s / Complex.Gamma s := by
funext s
rw [Complex.digamma_def, logDeriv_apply]
rw [hdig]
intro s hs
... AnalyticAt.div (hGammaAn.deriv s hs) (hGammaAn s hs) (the Gamma s ≠ 0)
```
Wait — the order: I need AnalyticOnNhd ℂ (fun s => deriv Gamma s / Gamma s) dpsiDomain — pointwise: (hGammaAn.deriv s hs).div (hGammaAn s hs) (Gamma s ≠ 0) — AnalyticAt.div (hf : AnalyticAt f x) (hg : AnalyticAt g x) (hg0 : g x ≠ 0) : AnalyticAt (f / g) x ✓ (used in LiResidue: hda.div ha hne ✓ — note the / is Pi.div — the lambda fun s => deriv Gamma s / Gamma s — defeq to deriv Gamma / Gamma ✓).
And AnalyticOnNhd.deriv : AnalyticOnNhd ℂ f s → AnalyticOnNhd ℂ (deriv f) s ✓ I believe exists.
Hmm — DifferentiableOn.analyticOnNhd's argument order: from LiResidue line 77: `h.analyticOnNhd Metric.isOpen_ball` where h : DifferentiableOn — so DifferentiableOn.analyticOnNhd (hs : IsOpen s) as the argument ✓ — `DifferentiableOn.analyticOnNhd (h) (hs)`? — the usage `h.analyticOnNhd Metric.isOpen_ball` — method-dot with the IsOpen arg ✓ so my `DifferentiableOn.analyticOnNhd _ dpsiDomain_isOpen` — hmm the _ is the DifferentiableOn which I `apply` — wait I wrote `apply DifferentiableOn.analyticOnNhd _ dpsiDomain_isOpen` — the _ is the DifferentiableOn hypothesis — apply leaves it as a goal: DifferentiableOn ℂ Gamma dpsiDomain — then intro z hz — DifferentiableOn's intro form: DifferentiableOn f s = ∀ x ∈ s, DifferentiableWithinAt f s x — `intro z hz` on that goal ✓ then `.differentiableWithinAt` of the differentiableAt ✓.
Let me also double check `Complex.Gamma_ne_zero` — from digamma_apply_add_one's proof (Digamma.lean:59): `Gamma_ne_zero hs` with hs : ∀ m : ℕ, s ≠ -m — inside namespace Complex — so `Complex.Gamma_ne_zero (hs : ∀ m : ℕ, s ≠ -↑m)? : Gamma s ≠ 0` ✓.
Then the identity principle + the cast bridge + the iterated values... Let me write Section 4 up to the identity principle now. Also need `TendstoUniformlyOn.tendstoLocallyUniformlyOn` — check name.
Clean. Checking the last name for Section 4, then writing the analyticity + identity principle.
tool: Bash ok
input
{
"command": "cd \"D:/Python/Quantum/zeta-23-lean/.lake/packages/mathlib\" && grep -rn \"TendstoUniformlyOn.tendstoLocallyUniformlyOn\\|theorem.*tendstoLocallyUniformlyOn_of\\|DifferentiableOn.analyticOnNhd\\|AnalyticOnNhd.deriv \\|theorem.*analyticOnNhd.*deriv\" Mathlib/Analysis/Complex/LocallyUniformLimit.lean Mathlib/Analysis/Calculus/ -r --include=\"*.lean\" 2>/dev/null | head -6; grep -rn \"theorem DifferentiableOn.analyticOnNhd\\|lemma DifferentiableOn.analyticOnNhd\" Mathlib/ -r --include=\"*.lean\" | head -2",
"description": "Check uniform-to-local and analyticOnNhd.deriv names"
}
result 2026-08-22 07:41:45Z → 2026-08-23 18:53:54Z
@hasSum_coe_mul_geometric_of_norm_lt_one : ∀ {𝕜 : Type u_1} [inst : NormedDivisionRing 𝕜] {r : 𝕜},
‖r‖ < 1 → HasSum (fun n => ↑n * r ^ n) (r / (1 - r) ^ 2)
HasSum.tsum_eq
(hasSum_coe_mul_geometric_of_norm_lt_one
(of_eq_true
(Eq.trans
(Eq.trans
(congrFun'
raw content_json (database row)
[{"type":"thinking","thinking":"Clean. Now Section 4: the analyticity of DinfC on dpsiDomain + the cast bridge + the identity principle. Let me write it.\n\n```lean\n/-! ## 4. Analyticity and the identity with Complex.digamma -/\n\n/-- The series converges uniformly on dpsiDomain (M-test with Σ 1/(m+1)²). -/\nlemma dpsiTermC_hasSumUniformlyOn :\n HasSumUniformlyOn dpsiTermC (fun s => ∑' m : ℕ, dpsiTermC s m) dpsiDomain := by\n apply HasSumUniformlyOn.of_norm_le_summable (summable_div_add_one_sq 1)\n intro m s hs\n -- ‖dpsiTermC s m‖ ≤ 1/(m+1)² for s ∈ dpsiDomain\n have hsm : s + m + 1 ≠ 0 := dpsiTermC_pole_free hs m\n have hre : 0 < s.re := dpsiDomain_re_pos hs\n rw [dpsiTermC_eq m hsm]\n rw [norm_div]\n have hden : ((m : ℝ) + 1) * ((m : ℝ) + 1) ≤ ‖((m : ℂ) + 1) * (s + ↑m + 1)‖ := by\n ... same as in summable\n have hs1 : ‖s‖ < 1 := by\n have h := hs\n rw [dpsiDomain, Metric.mem_ball, dist_eq_norm] at h\n calc ‖s‖ ≤ ‖s - (1:ℂ)/2‖ + ‖((1:ℂ)/2)‖ := norm_sub_le _ _\n _ < 1/2 + 1/2 := by ... ‖(1:ℂ)/2‖ = 1/2\n _ = 1 := by ring\n ...\n```\n\nHmm — the norm of (1:ℂ)/2: ‖(1:ℂ)/2‖ = 1/2 — `by simp`? — norm_div, norm_one, norm_two... Let me include: have h12 : ‖((1:ℂ)/2)‖ = 1/2 := by rw [norm_div, norm_one]; norm_num — hmm ‖(2:ℂ)‖ = 2: `Complex.norm_two`? or norm_num... there's `norm_two : ‖(2:ℂ)‖ = 2`? probably `Complex.norm_two`? hmm. Actually — h4's goal — ‖s‖/(‖m+1‖·‖s+m+1‖) ≤ 1/(m+1)² — since ‖s‖ < 1 and the denominator ≥ (m+1)²: ‖s‖/D ≤ 1/D·... — hmm need care: ‖s‖/D ≤ 1/(m+1)² with D ≥ (m+1)² and ‖s‖ ≤ 1: ‖s‖/D ≤ ‖s‖/(m+1)² ≤ 1/(m+1)² ✓ two steps.\n\nThen the differentiability: TendstoLocallyUniformlyOn.differentiableOn:\n```lean\nlemma DinfC_analyticOn : AnalyticOnNhd ℂ DinfC dpsiDomain := by\n have hunif := dpsiTermC_hasSumUniformlyOn\n have htend : TendstoLocallyUniformlyOn\n (fun t : Finset ℕ => fun s => ∑ m ∈ t, dpsiTermC s m)\n (fun s => ∑' m : ℕ, dpsiTermC s m) atTop dpsiDomain :=\n hasSumUniformlyOn_iff_tendstoUniformlyOn.mp hunif -- hmm — that's TendstoUniformlyOn — need the Locally version\n ...\n```\nhasSumUniformlyOn_iff_tendstoUniformlyOn.mp hunif : TendstoUniformlyOn (partial sums) (tsum-fn) atTop dpsiDomain — then to TendstoLocallyUniformlyOn: `TendstoUniformlyOn.tendstoLocallyUniformlyOn`? — there might be a lemma — or: since dpsiDomain is open, TendstoUniformlyOn on it implies TendstoLocallyUniformlyOn — hmm — TendstoLocallyUniformlyOn means: every point has a nhd (within s) where uniform — from uniform-on-all-of-s: the whole s is such a nhd (s ∈ 𝓝[s] x ✓ self_mem_nhdsWithin) — there's probably `TendstoUniformlyOn.tendstoLocallyUniformlyOn` — let me assume/find.\nThen TendstoLocallyUniformlyOn.differentiableOn htend (hF : ∀ᶠ t, DifferentiableOn ℂ (partial t) dpsiDomain): the partial sums are differentiable on dpsiDomain (each term differentiable: 1/(↑m+1) const + −1/(s+↑m+1) differentiable (s+↑m+1 ≠ 0 on the domain ✓ pole_free)) ✓ → DifferentiableOn ℂ (tsum-fn) dpsiDomain — then DinfC = −γ − 1/s + tsum-fn: DifferentiableOn (−γ − 1/s part: 1/s differentiable on dpsiDomain — 0 ∉ domain: s ≠ 0 from re > 0 ✓) — then `.analyticOnNhd dpsiDomain_isOpen`? — DifferentiableOn.analyticOnNhd (h : DifferentiableOn ℂ f s) (hs : IsOpen s) ✓.\n\nThe digamma side:\n```lean\nlemma digamma_analyticOn : AnalyticOnNhd ℂ Complex.digamma dpsiDomain := by\n intro s hs\n have hsG : Complex.Gamma s ≠ 0 := by\n apply Complex.Gamma_ne_zero\n intro m\n intro hmeq -- s = −↑m\n have hre : 0 < s.re := dpsiDomain_re_pos hs\n rw [hmeq] at hre\n simp at hre -- (−↑m).re = −↑m: 0 < −↑m — contradiction with ↑m ≥ 0\n have hm : (0 : ℝ) ≤ (m : ℝ) := Nat.cast_nonneg m\n linarith\n have hdif : DifferentiableAt ℂ Complex.Gamma s := by\n apply Complex.differentiableAt_Gamma\n intro m hmeq\n have hre : 0 < s.re := dpsiDomain_re_pos hs\n rw [hmeq] at hre\n simp at hre\n have hm : (0 : ℝ) ≤ (m : ℝ) := Nat.cast_nonneg m\n linarith\n -- digamma = deriv Gamma / Gamma — analytic at s via the quotient\n have hGammaAn : AnalyticAt ℂ Complex.Gamma s := by\n -- from differentiableAt on a nhd: DifferentiableOn on dpsiDomain then analyticOnNhd\n ...\n```\nHmm — AnalyticAt ℂ Complex.Gamma s from DifferentiableAt — NOT directly (pointwise differentiability ≠ analyticity at the point without a nhd) — BUT Gamma is differentiable on the open dpsiDomain ∋ s — so AnalyticOnNhd ℂ Gamma dpsiDomain via DifferentiableOn.analyticOnNhd — then AnalyticAt at s (AnalyticOnNhd.mem — `AnalyticOnNhd` def: ∀ x ∈ s, AnalyticAt f x — so from DifferentiableOn ℂ Gamma dpsiDomain: intro each point — differentiableAt_Gamma ✓ each point of dpsiDomain). So:\n```lean\n have hGammaAn : AnalyticOnNhd ℂ Complex.Gamma dpsiDomain := by\n apply DifferentiableOn.analyticOnNhd _ dpsiDomain_isOpen\n intro z hz\n exact (Complex.differentiableAt_Gamma z (fun m => by\n intro hmeq\n have hre : 0 < z.re := dpsiDomain_re_pos hz\n rw [hmeq] at hre\n simp at hre\n have hm : (0 : ℝ) ≤ (m : ℝ) := Nat.cast_nonneg m\n linarith)).differentiableWithinAt\n -- digamma = logDeriv Gamma = deriv Gamma / Gamma\n have hdig : Complex.digamma = fun s => deriv Complex.Gamma s / Complex.Gamma s := by\n funext s\n rw [Complex.digamma_def, logDeriv_apply]\n rw [hdig]\n intro s hs\n ... AnalyticAt.div (hGammaAn.deriv s hs) (hGammaAn s hs) (the Gamma s ≠ 0)\n```\nWait — the order: I need AnalyticOnNhd ℂ (fun s => deriv Gamma s / Gamma s) dpsiDomain — pointwise: (hGammaAn.deriv s hs).div (hGammaAn s hs) (Gamma s ≠ 0) — AnalyticAt.div (hf : AnalyticAt f x) (hg : AnalyticAt g x) (hg0 : g x ≠ 0) : AnalyticAt (f / g) x ✓ (used in LiResidue: hda.div ha hne ✓ — note the / is Pi.div — the lambda fun s => deriv Gamma s / Gamma s — defeq to deriv Gamma / Gamma ✓).\n\nAnd AnalyticOnNhd.deriv : AnalyticOnNhd ℂ f s → AnalyticOnNhd ℂ (deriv f) s ✓ I believe exists.\n\nHmm — DifferentiableOn.analyticOnNhd's argument order: from LiResidue line 77: `h.analyticOnNhd Metric.isOpen_ball` where h : DifferentiableOn — so DifferentiableOn.analyticOnNhd (hs : IsOpen s) as the argument ✓ — `DifferentiableOn.analyticOnNhd (h) (hs)`? — the usage `h.analyticOnNhd Metric.isOpen_ball` — method-dot with the IsOpen arg ✓ so my `DifferentiableOn.analyticOnNhd _ dpsiDomain_isOpen` — hmm the _ is the DifferentiableOn which I `apply` — wait I wrote `apply DifferentiableOn.analyticOnNhd _ dpsiDomain_isOpen` — the _ is the DifferentiableOn hypothesis — apply leaves it as a goal: DifferentiableOn ℂ Gamma dpsiDomain — then intro z hz — DifferentiableOn's intro form: DifferentiableOn f s = ∀ x ∈ s, DifferentiableWithinAt f s x — `intro z hz` on that goal ✓ then `.differentiableWithinAt` of the differentiableAt ✓.\n\nLet me also double check `Complex.Gamma_ne_zero` — from digamma_apply_add_one's proof (Digamma.lean:59): `Gamma_ne_zero hs` with hs : ∀ m : ℕ, s ≠ -m — inside namespace Complex — so `Complex.Gamma_ne_zero (hs : ∀ m : ℕ, s ≠ -↑m)? : Gamma s ≠ 0` ✓.\n\nThen the identity principle + the cast bridge + the iterated values... Let me write Section 4 up to the identity principle now. Also need `TendstoUniformlyOn.tendstoLocallyUniformlyOn` — check name.","signature":""},{"type":"text","text":"Clean. Checking the last name for Section 4, then writing the analyticity + identity principle."},{"type":"tool_use","id":"Bash_355","name":"Bash","input":{"command":"cd \"D:/Python/Quantum/zeta-23-lean/.lake/packages/mathlib\" && grep -rn \"TendstoUniformlyOn.tendstoLocallyUniformlyOn\\|theorem.*tendstoLocallyUniformlyOn_of\\|DifferentiableOn.analyticOnNhd\\|AnalyticOnNhd.deriv \\|theorem.*analyticOnNhd.*deriv\" Mathlib/Analysis/Complex/LocallyUniformLimit.lean Mathlib/Analysis/Calculus/ -r --include=\"*.lean\" 2>/dev/null | head -6; grep -rn \"theorem DifferentiableOn.analyticOnNhd\\|lemma DifferentiableOn.analyticOnNhd\" Mathlib/ -r --include=\"*.lean\" | head -2","description":"Check uniform-to-local and analyticOnNhd.deriv names"},"extra_content":null}]