← Session 22 — ii′-1: liCoeff pairing fix + residue machinery
thinking (2871 chars)
Committed (8e04c98). Now the remaining big pieces. Let me push on with Section 6 (the identity principle) since it's short, then Section 7 (iterated values via iteratedDerivWithin_tsum — the heavy one), Section 8 (reindexing), Section 9 (assembly).
Section 6: the identity principle.
```lean
/-! ## 6. The identity digamma = DinfC on the domain -/
lemma digamma_eq_DinfC_on : Set.EqOn Complex.digamma DinfC dpsiDomain := by
apply AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq digamma_analyticOn DinfC_analyticOn
dpsiDomain_convex.isPreconnected dpsiDomain_half
-- ∃ᶠ z in 𝓝[≠] ↑(1/2), digamma z = DinfC z
have hfreq : ∃ᶠ z in 𝓝[≠] (↑(1 / 2 : ℝ)), Complex.digamma z = DinfC z := by
rw [frequently_iff] -- check the name
intro U hU
-- U ∈ 𝓝[≠] ↑(1/2): extract a point of the real segment
rw [mem_nhdsWithin_iff_exists_mem_nhds_inter] at hU
obtain ⟨V, hV, hVU⟩ := hU
rw [Metric.mem_nhds_iff] at hV
obtain ⟨δ, hδ, hδV⟩ := hV
-- take the real point x = 1/2 + min (δ/2) (1/4)
refine ⟨↑((1 / 2 : ℝ) + min (δ / 2) (1 / 4)), hVU ?_, ?_⟩
· -- ∈ V ∩ {↑(1/2)}ᶜ
constructor
· apply hδV
rw [Metric.mem_ball, dist_eq_norm]
have e : (↑((1/2 : ℝ) + min (δ/2) (1/4)) : ℂ) - ↑(1/2 : ℝ) =
↑(min (δ/2) (1/4)) := by push_cast; ring
rw [e, RCLike.norm_ofReal]... wait Complex.norm_real + abs
have hpos : (0:ℝ) < min (δ/2) (1/4) := lt_min (by positivity) (by norm_num)
rw [abs_of_nonneg hpos.le] -- hmm — the norm of the cast = |·|
calc min (δ/2) (1/4) ≤ δ/2 := min_le_left _ _
_ < δ := by linarith [hδ]
· -- ≠ ↑(1/2)
intro hcontra
have : (↑((1/2 : ℝ) + min (δ/2) (1/4)) : ℂ) = ↑(1/2 : ℝ) := hcontra
have h2 : (1/2 : ℝ) + min (δ/2) (1/4) = 1/2 := by
exact_mod_cast this -- ofReal injective: ofReal_inj
have hpos : (0:ℝ) < min (δ/2) (1/4) := lt_min (by positivity) (by norm_num)
linarith
· -- the equality at that point
have hx : (1/2 : ℝ) + min (δ/2) (1/4) ∈ Set.Ioo 0 1 := by
constructor
· have hpos : (0:ℝ) < min (δ/2) (1/4) := lt_min (by positivity) (by norm_num)
linarith
· have : min (δ/2) (1/4) ≤ 1/4 := min_le_right _ _
linarith
exact digamma_eq_DinfC_ofReal hx
exact hfreq
```
Names to verify: `frequently_iff` — the exact: `Filter.frequently_iff : (∃ᶠ x in l, P x) ↔ ∀ U ∈ l, ∃ x ∈ U, P x`? — I think it's `frequently_iff` hmm or `Filter.frequently_iff_exists`... let me check. Also `mem_nhdsWithin_iff_exists_mem_nhds_inter` and `Metric.mem_nhds_iff`.
Also — the EqOn conclusion's usage: eqOn_of_preconnected_of_frequently_eq gives EqOn f g U — with f := digamma, g := DinfC — the hfg : ∃ᶠ z in 𝓝[≠] z₀, f z = g z — digamma z = DinfC z ✓ matches digamma_eq_DinfC_ofReal's conclusion ✓.
Let me check the filter lemma names.
Section 6 — the identity principle. Checking the filter lemma names first.
tool: Bash ok
input
{
"command": "cd \"D:/Python/Quantum/zeta-23-lean/.lake/packages/mathlib\" && grep -rn \"theorem frequently_iff \\|lemma frequently_iff \" Mathlib/Order/Filter/Basic.lean | head -3; grep -rn \"mem_nhdsWithin_iff_exists_mem_nhds_inter\" Mathlib/Topology/ -r --include=\"*.lean\" | head -2",
"description": "Check frequently_iff and mem_nhdsWithin names"
}
result 2026-08-22 08:23:42Z → 2026-08-23 10:53:11Z
NguyenRH1/LiDigammaLeft.lean:483:45: warning: Variable name `hdist` is not explicitly referenced.
Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
[apply] _hdist
Note: This linter can be disabled with `set_option linter.unusedVariables false`
NguyenRH1/LiDigammaLeft.lean:513:44: warning: Variable name `hdist` is not explicitly referenced.
Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
[apply] _hdist
Note: This linter can be disabled with `set_option linter.unusedVariables false`
NguyenRH1/LiDigammaLeft.lean:610:28: error: Type mismatch
hlogmono0 hm1 hm1
has type
1 + Real.log ↑1 ≤ 1 + Real.log ↑m
but is expected to have type
1 + Real.log (↑m - (↑j₀ + 1)) ≤ 1 + Real.log ↑m
NguyenRH1/LiDigammaLeft.lean:614:14: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
?m.768 j₀ + ∑ x ∈ (Finset.Ico j₀ m).erase j₀, ?m.768 x
in the target expression
∑ j ∈ Finset.Ico j₀ m, ‖(w + ↑j)⁻¹‖ = ‖(w + ↑j₀)⁻¹‖ + ∑ j ∈ Finset.Ico (j₀ + 1) m, ‖(w + ↑j)⁻¹‖
c : ℝ
hc : 0 < c
w : ℂ
hdist : ∀ (m : ℕ), c ≤ ‖w + ↑m‖
m : ℕ
j₀ : ℕ := ⌈-w.re⌉₊
hm : j₀ + 1 ≤ m
hj₀ : j₀ = ⌈-w.re⌉₊
hj₀m : j₀ ≤ m
hm1 : 1 ≤ m
hHarm : ∀ (K : ℕ), ∑ i ∈ Finset.range K, (↑i + 1)⁻¹ ≤ 1 + Real.log ↑K
hlogmono : ∀ {a b : ℕ}, 1 ≤ a → a ≤ b → 1 + Real.log ↑a ≤ 1 + Real.log ↑b
raw content_json (database row)
[{"type":"thinking","thinking":"Committed (8e04c98). Now the remaining big pieces. Let me push on with Section 6 (the identity principle) since it's short, then Section 7 (iterated values via iteratedDerivWithin_tsum — the heavy one), Section 8 (reindexing), Section 9 (assembly).\n\nSection 6: the identity principle.\n```lean\n/-! ## 6. The identity digamma = DinfC on the domain -/\n\nlemma digamma_eq_DinfC_on : Set.EqOn Complex.digamma DinfC dpsiDomain := by\n apply AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq digamma_analyticOn DinfC_analyticOn\n dpsiDomain_convex.isPreconnected dpsiDomain_half\n -- ∃ᶠ z in 𝓝[≠] ↑(1/2), digamma z = DinfC z\n have hfreq : ∃ᶠ z in 𝓝[≠] (↑(1 / 2 : ℝ)), Complex.digamma z = DinfC z := by\n rw [frequently_iff] -- check the name\n intro U hU\n -- U ∈ 𝓝[≠] ↑(1/2): extract a point of the real segment\n rw [mem_nhdsWithin_iff_exists_mem_nhds_inter] at hU\n obtain ⟨V, hV, hVU⟩ := hU\n rw [Metric.mem_nhds_iff] at hV\n obtain ⟨δ, hδ, hδV⟩ := hV\n -- take the real point x = 1/2 + min (δ/2) (1/4)\n refine ⟨↑((1 / 2 : ℝ) + min (δ / 2) (1 / 4)), hVU ?_, ?_⟩\n · -- ∈ V ∩ {↑(1/2)}ᶜ\n constructor\n · apply hδV\n rw [Metric.mem_ball, dist_eq_norm]\n have e : (↑((1/2 : ℝ) + min (δ/2) (1/4)) : ℂ) - ↑(1/2 : ℝ) =\n ↑(min (δ/2) (1/4)) := by push_cast; ring\n rw [e, RCLike.norm_ofReal]... wait Complex.norm_real + abs\n have hpos : (0:ℝ) < min (δ/2) (1/4) := lt_min (by positivity) (by norm_num)\n rw [abs_of_nonneg hpos.le] -- hmm — the norm of the cast = |·|\n calc min (δ/2) (1/4) ≤ δ/2 := min_le_left _ _\n _ < δ := by linarith [hδ]\n · -- ≠ ↑(1/2)\n intro hcontra\n have : (↑((1/2 : ℝ) + min (δ/2) (1/4)) : ℂ) = ↑(1/2 : ℝ) := hcontra\n have h2 : (1/2 : ℝ) + min (δ/2) (1/4) = 1/2 := by\n exact_mod_cast this -- ofReal injective: ofReal_inj\n have hpos : (0:ℝ) < min (δ/2) (1/4) := lt_min (by positivity) (by norm_num)\n linarith\n · -- the equality at that point\n have hx : (1/2 : ℝ) + min (δ/2) (1/4) ∈ Set.Ioo 0 1 := by\n constructor\n · have hpos : (0:ℝ) < min (δ/2) (1/4) := lt_min (by positivity) (by norm_num)\n linarith\n · have : min (δ/2) (1/4) ≤ 1/4 := min_le_right _ _\n linarith\n exact digamma_eq_DinfC_ofReal hx\n exact hfreq\n```\nNames to verify: `frequently_iff` — the exact: `Filter.frequently_iff : (∃ᶠ x in l, P x) ↔ ∀ U ∈ l, ∃ x ∈ U, P x`? — I think it's `frequently_iff` hmm or `Filter.frequently_iff_exists`... let me check. Also `mem_nhdsWithin_iff_exists_mem_nhds_inter` and `Metric.mem_nhds_iff`.\n\nAlso — the EqOn conclusion's usage: eqOn_of_preconnected_of_frequently_eq gives EqOn f g U — with f := digamma, g := DinfC — the hfg : ∃ᶠ z in 𝓝[≠] z₀, f z = g z — digamma z = DinfC z ✓ matches digamma_eq_DinfC_ofReal's conclusion ✓.\n\nLet me check the filter lemma names.","signature":""},{"type":"text","text":"Section 6 — the identity principle. Checking the filter lemma names first."},{"type":"tool_use","id":"Bash_405","name":"Bash","input":{"command":"cd \"D:/Python/Quantum/zeta-23-lean/.lake/packages/mathlib\" && grep -rn \"theorem frequently_iff \\|lemma frequently_iff \" Mathlib/Order/Filter/Basic.lean | head -3; grep -rn \"mem_nhdsWithin_iff_exists_mem_nhds_inter\" Mathlib/Topology/ -r --include=\"*.lean\" | head -2","description":"Check frequently_iff and mem_nhdsWithin names"},"extra_content":null}]