← Session 21 — Tier ii′ planning + launch: close SfBoundProp in Lean (D-064)
thinking (7349 chars)
I wrote a first draft but I left a `sorry` in `hLi_eq_near_one` and some proofs are likely broken (hcd's algebra got convoluted, hsum's structure is off, hmap's reindexing is shaky). Let me compile and fix iteratively. Also I should fix hLi_eq_near_one's sorry: the zero-free punctured neighborhood of 1 — ζ(w) ≠ 0 for w near 1 with... the simple argument: ζ has a pole at 1, so |ζ| → ∞, hence ζ ≠ 0 in a punctured nhd: from riemannZeta_residue_one: (s−1)ζ(s) → 1, so (s−1)ζ(s) ≠ 0 in a punctured nhd, hence ζ(s) ≠ 0 there. That's cleaner than the re ≥ 1 approach:
```
lemma hLi_eq_near_one :
∀ᶠ w in 𝓝[≠] (1 : ℂ), hLi w = (w - 1) * (-(deriv riemannZeta w) / riemannZeta w) := by
have hT := riemannZeta_residue_one
have hne : ∀ᶠ w in 𝓝[≠] (1 : ℂ), (w - 1) * riemannZeta w ≠ 0 := by
have := hT.eventually_ne (show (1 : ℂ) ≠ 0 by norm_num)
exact this
filter_upwards [hne, eventually_mem_nhdsWithin] with w hw hw1
have hz : riemannZeta w ≠ 0 := by
have h2 := hw
simp only [ne_eq, mul_eq_zero] at h2
push_neg at h2
exact h2.2
exact hLi_eq_of_ne hw1 hz
```
`Tendsto.eventually_ne : Tendsto f l (𝓝 a) → a ≠ b → ∀ᶠ x in l, f x ≠ b` ✓ exists.
Also fix hcd — the coefficient algebra got tangled. Let me simplify: the identity needed:
(n.choose i : ℂ) * (n.descFactorial i : ℂ) / n ! = (n.choose i : ℂ) / ((n - i) ! : ℂ)·... wait — actually what I need: C(n,i)·descFac(i)/n!·h^{(n−i)} = C(n,i)·lcoeff(n−i−1) with lcoeff(n−i−1) = h^{(n−i)}/(n−i)!. So need C(n,i)·descFac(n,i)/n! = C(n,i)/(n−i)! ⟺ descFac(n,i)/n! = 1/(n−i)! ⟺ descFac(n,i)·... ⟺ n!/(n−i)! — i.e. descFac(n,i) = n!/(n−i)! — via factorial_mul_descFactorial: (n−i)!·descFac(n,i) = n! ⟹ descFac(n,i) = n!/(n−i)! ✓ (division in ℂ of the cast equality ✓ clean).
So the clean version:
```
have hdesc : (n.descFactorial i : ℂ) = (n ! : ℂ) / ((n - i) ! : ℂ) := by
have h2 := Nat.factorial_mul_descFactorial (show i ≤ n by omega)
have hcast : ((n - i) ! : ℂ) * (n.descFactorial i : ℂ) = (n ! : ℂ) := by exact_mod_cast h2
rw [eq_div_iff_mul_eq (by simp [Nat.factorial_ne_zero])]
rw [mul_comm]
exact hcast
```
`eq_div_iff_mul_eq : a = b / c ↔ a * c = b` (c ≠ 0) — check name: `eq_div_iff_mul_eq (hc : c ≠ 0) : a = b / c ↔ a * c = b` ✓.
Then term rewriting:
C(n,i)·descFac(n,i)·h^{(n−i)}/n! = C(n,i)·(n!/(n−i)!)·h^{(n−i)}/n! = C(n,i)·h^{(n−i)}/(n−i)! = C(n,i)·lcoeff(n−i−1).
And C(n,i) = C(n,n−i) (Nat.choose_symm hi).
The sum reindexing: ∑_{i ∈ range n} f(n−i) where f(k) = C(n,k)·lcoeff(k−1)... i ↦ n−i maps range n = {0,...,n−1} to {1,...,n} = Icc 1 n: `Finset.sum_range_reflect`? — sum_range_reflect : ∑ i ∈ range n, f i = ∑ i ∈ range n, f (n − 1 − i). Hmm that maps to n−1−i ∈ {0,...,n−1}. My target is Icc 1 n. Alternative: sum over range (n+1) with the zero terms? Or use `Finset.sum_bij`. Simplest: convert the target sum to range form: ∑ j ∈ Icc 1 n, g j = ∑ i ∈ range n, g (i + 1): `Finset.sum_Icc_eq_sum_range`? there's `Finset.sum_Icc_eq_sum_range : ∑ i ∈ Icc m n, f i = ∑ i ∈ range (n + 1 - m), f (i + m)` ✓ I believe. So ∑ j ∈ Icc 1 n, g j = ∑ i ∈ range n, g (i+1). Then:
∑ i ∈ range n, C(n,i)·descFac·h^{(n−i)}/n! = ∑ i ∈ range n, C(n,i)·lcoeff(n−i−1)·... vs ∑ i ∈ range n, g(i+1) = ∑ i ∈ range n, C(n,i+1)·lcoeff(i). Via sum_range_reflect: ∑ i ∈ range n, a(i) = ∑ i ∈ range n, a(n−1−i): with a(i) = C(n,i)·lcoeff(n−i−1): a(n−1−i) = C(n,n−1−i)·lcoeff(n−(n−1−i)−1) = C(n,i+1)·lcoeff(i)·... C(n,n−1−i) = C(n,i+1) (choose_symm: n−(n−1−i) = i+1 ✓). ✓
Let me restructure hfinal cleanly:
```
have hterm : ∀ i ∈ Finset.range n,
(n.choose i : ℂ) * (n.descFactorial i : ℂ) * iteratedDeriv (n - i) hLi 1 / n ! =
(n.choose i : ℂ) * lcoeff (n - i - 1) := by
intro i hi
rw [Finset.mem_range] at hi
have hdesc : (n.descFactorial i : ℂ) = (n ! : ℂ) / ((n - i) ! : ℂ) := by
have h2 := Nat.factorial_mul_descFactorial (show i ≤ n by omega)
have hcast : ((n - i) ! : ℂ) * (n.descFactorial i : ℂ) = (n ! : ℂ) := by exact_mod_cast h2
rw [eq_div_iff_mul_eq (by simp [Nat.factorial_ne_zero])]
rw [mul_comm]
exact hcast
rw [hdesc]
have hni : 1 ≤ n - i := by omega
have hlc : lcoeff (n - i - 1) = iteratedDeriv (n - i) hLi 1 / ((n - i) ! : ℂ) := by
rw [hLi_iteratedDeriv_div_factorial (j := n - i) hni]
rw [hlc]
field_simp
ring
```
field_simp + ring for: C·(n!/(n−i)!)·h/n! = C·(h/(n−i)!) — with h = iteratedDeriv — field_simp [n! ≠ 0, (n−i)! ≠ 0] then ring ✓.
Then:
```
rw [Finset.sum_div]
rw [Finset.sum_congr rfl hterm]
-- now: ∑ i ∈ range n, C(n,i)·lcoeff(n−i−1) = ∑ j ∈ Icc 1 n, C(n,j)·lcoeff(j−1)
have hre : ∑ i ∈ Finset.range n, (n.choose i : ℂ) * lcoeff (n - i - 1) =
∑ j ∈ Finset.Icc 1 n, (n.choose j : ℂ) * lcoeff (j - 1) := by
rw [Finset.sum_range_reflect]
-- now ∑ i ∈ range n, C(n, n−1−i)·lcoeff(n−(n−1−i)−1) = C(n,n−1−i)·lcoeff(i)
rw [Finset.sum_Icc_eq_sum_range]
apply Finset.sum_congr rfl
intro i hi
rw [Finset.mem_range] at hi
have e1 : n - 1 - i + 1 = n - i := by omega
-- target after rewrites: C(n, n−1−i)·lcoeff(n−1−i−...)... let me compute in code
...
```
Hmm the reindexing needs care. Finset.sum_range_reflect : ∑ i ∈ range n, f i = ∑ i ∈ range n, f (n - 1 - i). So ∑_{i<n} a(i) = ∑_{i<n} a(n−1−i): with a(k) = C(n,k)·lcoeff(n−k−1): a(n−1−i) = C(n,n−1−i)·lcoeff(n−(n−1−i)−1) = C(n,n−1−i)·lcoeff(i). C(n,n−1−i) = C(n,n−(n−1−i)) = C(n,i+1) — Nat.choose_symm : n.choose (n − k) = n.choose k for k ≤ n: n.choose (n−1−i) = n.choose (n − (n−1−i)) = n.choose (i+1)? — choose_symm (h : k ≤ n) : n.choose (n - k) = n.choose k — so n.choose (n−1−i) = n.choose (i+1) iff (n−1−i) = n − (i+1) ✓ and k := i+1 ≤ n ✓. So a(n−1−i) = C(n,i+1)·lcoeff(i). And the target (after sum_Icc_eq_sum_range): ∑_{i<n} C(n,i+1)·lcoeff((i+1)−1) = ∑_{i<n} C(n,i+1)·lcoeff(i) ✓ MATCHES.
OK — let me rewrite the file with all fixes. Also fix `hsum`'s broken structure (I had a malformed Finset.sum_subset application). The sum over range (n+1) → range n: the i = n term vanishes because A^{(n)}(1) = 0:
```
have hsum : (∑ i ∈ Finset.range (n + 1),
n.choose i * iteratedDeriv i (fun w : ℂ => w ^ n - (w - 1) ^ n) 1 *
iteratedDeriv (n - i) hLi 1) =
∑ i ∈ Finset.range n,
n.choose i * (n.descFactorial i : ℂ) * iteratedDeriv (n - i) hLi 1 := by
rw [Finset.sum_range_succ]
simp [A_iter n n le_rfl]
apply Finset.sum_congr rfl
intro i hi
rw [Finset.mem_range] at hi
rw [A_iter n i (by omega), if_pos hi]
```
Finset.sum_range_succ : ∑ i ∈ range (n+1), f i = ∑ i ∈ range n, f i + f n ✓. f n = C(n,n)·0·... = 0: A_iter n n (le_refl) : iteratedDeriv n A 1 = if n < n then ... else 0 = 0: if_neg (lt_irrefl n): simp [A_iter n n le_rfl] should simplify f n to 0 (A_iter gives if n < n then _ else 0 = 0 ✓).
Also `iteratedDeriv_sub` needs ContDiffAt — provided hA separately: in A_iter I used hf/hg locally ✓.
The `iteratedDeriv_mul` result: Σ i ∈ range (n+1), n.choose i * iteratedDeriv i A 1 * iteratedDeriv (n−i) hLi 1 — from the signature: `iteratedDeriv n (f * g) x = ∑ i ∈ .range (n + 1), n.choose i * iteratedDeriv i f x * iteratedDeriv (n - i) g x` — note: n.choose i is ℕ — cast to ℂ? The lemma as displayed: `n.choose i * iteratedDeriv i f x * iteratedDeriv (n - i) g x` — for 𝕜 → 𝔸 with 𝔸 an algebra over 𝕜 — the choose is a natural scalar mult — for ℂ→ℂ it should elaborate as (n.choose i : ℂ) cast or nsmul. Fine.
Let me now rewrite the whole file cleanly.
The draft needs repair — rewriting with the cleaned-up coefficient algebra, the proper zero-free argument, and fixed reindexing.
tool: Write ok
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiResidue.lean",
"content": "/-\nNguyenRH1/LiResidue.lean \u2014 tier ii\u2032 sub-stage ii\u2032-1b (D-064 \u00a74 R1):\nthe w = 1 residue of the Lagarias-kernel integrand, computed exactly.\n\nContents (Part 1):\n* `zetaA w = (w\u22121)\u00b7\u03b6(w)` extended by 1 at w = 1 \u2014 analytic at 1 with\n value 1 (removable singularity; Mathlib `riemannZeta_residue_one` +\n `differentiableOn_update_limUnder_of_bddAbove`).\n* `hLi w = 1 \u2212 (w\u22121)\u00b7(zetaA\u2032/zetaA)(w)` \u2014 analytic at 1, hLi 1 = 1;\n agrees with (w\u22121)\u00b7(\u2212\u03b6\u2032/\u03b6)(w) on a punctured neighborhood of 1\n (`hLi_eq_near_one`).\n* `lcoeff k` \u2014 the Laurent coefficients of \u2212\u03b6\u2032/\u03b6 at 1, DEFINED as\n iteratedDeriv (k+1) hLi 1 / (k+1)!.\n* `ResW1 n` \u2014 the residue at w = 1 of J(w) = k_n(w\u22121)\u00b7(\u2212\u03b6\u2032/\u03b6(w)),\n packaged as (1/n!)\u00b7(d/dw)\u207f[(w\u207f\u2212(w\u22121)\u207f)\u00b7hLi] at w = 1 (D-064 \u00a74 R1:\n (w\u22121)^{n+1}J = [w\u207f\u2212(w\u22121)\u207f]\u00b7hLi on a punctured neighborhood, by\n `hLi_eq_near_one`). Value: `ResW1_eq_sum`.\n\nArchive references: D-036, D-037, D-064 (R1), journal-014/015.\n-/\nimport Mathlib\nimport Zeta23.Statement\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. The regularized factor zetaA = (w\u22121)\u03b6(w) at w = 1 -/\n\n/-- `zetaA w = (w\u22121)\u00b7\u03b6(w)` with the removable singularity at w = 1 filled\nby the residue value 1. Analytic at 1 (`zetaA_analyticAt_one`), value\n`zetaA 1 = 1`. -/\ndef zetaA : \u2102 \u2192 \u2102 := Function.update (fun w => (w - 1) * riemannZeta w) 1 1\n\nlemma zetaA_apply {w : \u2102} (hw : w \u2260 1) : zetaA w = (w - 1) * riemannZeta w :=\n Function.update_of_ne hw _ _\n\nlemma zetaA_one : zetaA 1 = 1 := Function.update_self _ _ _\n\n/-- The regularized factor is analytic at w = 1 (removable singularity). -/\nlemma zetaA_analyticAt_one : AnalyticAt \u2102 zetaA 1 := by\n have hdiff : DifferentiableOn \u2102 (fun w => (w - 1) * riemannZeta w)\n (Metric.ball 1 2 \\ {1}) := by\n intro w hw\n have hw1 : w \u2260 1 := hw.2\n exact ((differentiableAt_id.sub (differentiableAt_const 1)).mul\n (differentiableAt_riemannZeta hw1)).differentiableWithinAt\n have hbd : BddAbove (Complex.norm \u2218 (fun w => (w - 1) * riemannZeta w)) ''\n (Metric.ball 1 2 \\ {1}) := by\n have hT := riemannZeta_residue_one\n rw [Metric.tendsto_nhdsWithin_nhds] at hT\n obtain \u27e8\u03b4, h\u03b40, h\u03b4\u27e9 := hT 1 one_pos\n refine \u27e82, ?_\u27e9\n rintro _ \u27e8z, hz, rfl\u27e9\n have hz1 : z \u2260 1 := hz.2\n have hlt := h\u03b4 (by\n rw [dist_eq_norm, sub_zero]\n exact hz.1)\n have h1 : \u2016(z - 1) * riemannZeta z - 1\u2016 < 1 := by\n have := hlt\n rwa [dist_eq_norm] at this\n have := norm_sub_le ((z - 1) * riemannZeta z) 1\n simp only [Complex.norm_eq_abs] at *\n have h2 : \u2016(z - 1) * riemannZeta z\u2016 \u2264 \u2016(z - 1) * riemannZeta z - 1\u2016 + \u2016(1 : \u2102)\u2016 :=\n norm_sub_le ((z - 1) * riemannZeta z) 1\n rw [norm_one] at h2\n linarith [h1]\n have h := differentiableOn_update_limUnder_of_bddAbove\n (Metric.ball_mem_nhds 1 (by norm_num : (0 : \u211d) < 2)) hdiff hbd\n have hlim : limUnder (\ud835\udcdd[\u2260] (1 : \u2102)) (fun w => (w - 1) * riemannZeta w) = 1 :=\n riemannZeta_residue_one.limUnder_eq\n rw [hlim] at h\n have han := h.analyticOnNhd Metric.isOpen_ball\n exact han.analyticAt (Metric.ball_mem_nhds 1 (by norm_num : (0 : \u211d) < 2))\n\n/-- zetaA is nonzero on a neighborhood of 1 (value 1 there). -/\nlemma zetaA_ne_zero_near_one : \u2200\u1da0 w in \ud835\udcdd (1 : \u2102), zetaA w \u2260 0 :=\n (zetaA_analyticAt_one.continuousAt).eventually_ne (by rw [zetaA_one]; norm_num)\n\n/-- zetaA is analytic at any w \u2260 1 (agrees with (w\u22121)\u03b6 there). -/\nlemma zetaA_analyticAt_of_ne {w : \u2102} (hw : w \u2260 1) : AnalyticAt \u2102 zetaA w := by\n have h : (fun w => (w - 1) * riemannZeta w) =\u1da0[\ud835\udcdd w] zetaA := by\n filter_upwards [eventually_ne_nhds hw] with z hz using (zetaA_apply hz).symm\n have ha : AnalyticAt \u2102 (fun w => (w - 1) * riemannZeta w) w :=\n (analyticAt_id.sub analyticAt_const).mul\n (differentiableAt_riemannZeta hw).analyticAt\n exact ha.congr h\n\n/-! ## 2. hLi w = 1 \u2212 (w\u22121)\u00b7(zetaA\u2032/zetaA)(w): analytic at 1, value 1 -/\n\n/-- hLi(w) = 1 \u2212 (w\u22121)\u00b7(zetaA\u2032/zetaA)(w) \u2014 the analytic-at-1 form of\n(w\u22121)(\u2212\u03b6\u2032/\u03b6)(w) (`hLi_eq_near_one`). hLi 1 = 1. -/\ndef hLi (w : \u2102) : \u2102 := 1 - (w - 1) * (deriv zetaA w / zetaA w)\n\nlemma hLi_one : hLi 1 = 1 := by simp [hLi]\n\nlemma hLi_analyticAt_one : AnalyticAt \u2102 hLi 1 := by\n have ha := zetaA_analyticAt_one\n have hda : AnalyticAt \u2102 (deriv zetaA) 1 := ha.deriv\n have hne : zetaA 1 \u2260 0 := by rw [zetaA_one]; norm_num\n exact ((analyticAt_const.sub analyticAt_id).mul\n (hda.div ha hne)).const_sub 1\n\n/-- On the punctured plane minus zeros of \u03b6, hLi = (w\u22121)\u00b7(\u2212\u03b6\u2032/\u03b6). -/\nlemma hLi_eq_of_ne {w : \u2102} (hw1 : w \u2260 1) (hw0 : riemannZeta w \u2260 0) :\n hLi w = (w - 1) * (-(deriv riemannZeta w) / riemannZeta w) := by\n have hA : zetaA w = (w - 1) * riemannZeta w := zetaA_apply hw1\n have hdA : deriv zetaA w = riemannZeta w + (w - 1) * deriv riemannZeta w := by\n have h1 : deriv (fun z => (z - 1) * riemannZeta z) w =\n deriv (fun z => z - 1) w * riemannZeta w +\n (w - 1) * deriv riemannZeta w :=\n deriv_mul ((differentiableAt_id.sub (differentiableAt_const 1)))\n (differentiableAt_riemannZeta hw1)\n have h2 : deriv (fun z => z - 1) w = 1 := by\n simp [deriv_sub, deriv_id'']\n have h3 : (fun z => (z - 1) * riemannZeta z) =\u1da0[\ud835\udcdd w] zetaA := by\n filter_upwards [eventually_ne_nhds hw1] with z hz using (zetaA_apply hz).symm\n rw [h3.deriv_eq, h1, h2, one_mul]\n rw [hLi, hdA, hA]\n have hw1' : w - 1 \u2260 0 := sub_ne_zero.mpr hw1\n field_simp [hw0, hw1']\n ring\n\n/-- On a punctured neighborhood of 1, hLi = (w\u22121)\u00b7(\u2212\u03b6\u2032/\u03b6). -/\nlemma hLi_eq_near_one :\n \u2200\u1da0 w in \ud835\udcdd[\u2260] (1 : \u2102), hLi w = (w - 1) * (-(deriv riemannZeta w) / riemannZeta w) := by\n have hne : \u2200\u1da0 w in \ud835\udcdd[\u2260] (1 : \u2102), (w - 1) * riemannZeta w \u2260 0 :=\n riemannZeta_residue_one.eventually_ne (show (1 : \u2102) \u2260 0 by norm_num)\n filter_upwards [hne, eventually_mem_nhdsWithin] with w hw hw1\n have hz : riemannZeta w \u2260 0 := by\n have h2 := hw\n simp only [ne_eq, mul_eq_zero] at h2\n push_neg at h2\n exact h2.2\n exact hLi_eq_of_ne hw1 hz\n\n/-! ## 3. The Laurent coefficients of \u2212\u03b6\u2032/\u03b6 at 1 (operational definition) -/\n\n/-- The k-th Laurent coefficient of \u2212\u03b6\u2032/\u03b6 at s = 1, DEFINED as\niteratedDeriv (k+1) hLi 1 / (k+1)! (the power-series coefficient of the\nanalytic hLi; the identification with \u2212\u03b6\u2032/\u03b6's Laurent expansion is\n`hLi_eq_near_one`). -/\ndef lcoeff (k : \u2115) : \u2102 := iteratedDeriv (k + 1) hLi 1 / (k + 1) !\n\n/-- hLi's Taylor coefficients: iteratedDeriv j hLi 1 / j ! = lcoeff (j\u22121). -/\nlemma hLi_iteratedDeriv_div_factorial {j : \u2115} (hj : 1 \u2264 j) :\n iteratedDeriv j hLi 1 / j ! = lcoeff (j - 1) := by\n rw [lcoeff]\n have : j = (j - 1) + 1 := by omega\n rw [this]\n\n/-! ## 4. The A-polynomial derivative: A(w) = w\u207f \u2212 (w\u22121)\u207f -/\n\n/-- Iterated derivatives of A(w) = w\u207f \u2212 (w\u22121)\u207f at 1:\nA^{(i)}(1) = n.descFactorial i for i < n, and A^{(n)}(1) = 0. -/\nlemma A_iter (n i : \u2115) (hi : i \u2264 n) :\n iteratedDeriv i (fun w => w ^ n - (w - 1) ^ n) (1 : \u2102) =\n if i < n then n.descFactorial i else 0 := by\n have hf : ContDiffAt \u2102 i (fun w : \u2102 => w ^ n) 1 :=\n (contDiff_id.pow n).contDiffAt\n have hg : ContDiffAt \u2102 i (fun w : \u2102 => (w - 1) ^ n) 1 :=\n ((contDiff_id.sub contDiff_const).pow n).contDiffAt\n rw [iteratedDeriv_sub hf hg]\n have h1 : iteratedDeriv i (fun w : \u2102 => w ^ n) 1 = n.descFactorial i := by\n rw [iteratedDeriv_pow]\n simp\n have h2 : iteratedDeriv i (fun w : \u2102 => (w - 1) ^ n) 1 =\n n.descFactorial i * (0 : \u2102) ^ (n - i) := by\n have e := congr_fun (iteratedDeriv_comp_sub_const i (fun w : \u2102 => w ^ n) (1 : \u2102)) 1\n rw [iteratedDeriv_pow] at e\n simpa using e\n rw [h1, h2]\n by_cases hin : i < n\n \u00b7 rw [if_pos hin]\n have hz : (0 : \u2102) ^ (n - i) = 0 := zero_pow (by omega)\n rw [hz, mul_zero, sub_zero]\n \u00b7 rw [if_neg hin]\n have hin' : i = n := le_antisymm hi (by omega)\n subst hin'\n simp [Nat.descFactorial_self]\n\n/-! ## 5. The residue at w = 1: ResW1 n = \u03a3_{j=1}^n C(n,j)\u00b7lcoeff (j\u22121) -/\n\n/-- The residue at w = 1 of the Lagarias-kernel integrand\nJ(w) = k_n(w\u22121)\u00b7(\u2212\u03b6\u2032/\u03b6(w)), packaged as (1/n!)\u00b7(d/dw)\u207f[(w\u207f\u2212(w\u22121)\u207f)hLi]\nat w = 1 (D-064 \u00a74 R1: (w\u22121)^{n+1}J = [w\u207f\u2212(w\u22121)\u207f]\u00b7hLi punctured near 1,\nby `hLi_eq_near_one`). -/\ndef ResW1 (n : \u2115) : \u2102 :=\n iteratedDeriv n (fun w => (w ^ n - (w - 1) ^ n) * hLi w) (1 : \u2102) / n !\n\n/-- The w = 1 residue value: ResW1 n = \u03a3_{j=1}^n C(n,j)\u00b7lcoeff (j\u22121). -/\ntheorem ResW1_eq_sum (n : \u2115) :\n ResW1 n = \u2211 j \u2208 Finset.Icc 1 n, (n.choose j : \u2102) * lcoeff (j - 1) := by\n have hA : ContDiffAt \u2102 n (fun w : \u2102 => w ^ n - (w - 1) ^ n) 1 :=\n ((contDiff_id.pow n).sub ((contDiff_id.sub contDiff_const).pow n)).contDiffAt\n have hh : ContDiffAt \u2102 n hLi 1 := hLi_analyticAt_one.contDiffAt\n have hmul := iteratedDeriv_mul hA hh\n rw [ResW1, hmul]\n have hsum : (\u2211 i \u2208 Finset.range (n + 1),\n n.choose i * iteratedDeriv i (fun w : \u2102 => w ^ n - (w - 1) ^ n) 1 *\n iteratedDeriv (n - i) hLi 1) =\n \u2211 i \u2208 Finset.range n,\n n.choose i * (n.descFactorial i : \u2102) * iteratedDeriv (n - i) hLi 1 := by\n rw [Finset.sum_range_succ]\n simp [A_iter n n le_rfl]\n apply Finset.sum_congr rfl\n intro i hi\n rw [Finset.mem_range] at hi\n rw [A_iter n i (by omega), if_pos hi]\n rw [hsum]\n have hterm : \u2200 i \u2208 Finset.range n,\n n.choose i * (n.descFactorial i : \u2102) * iteratedDeriv (n - i) hLi 1 / n ! =\n (n.choose i : \u2102) * lcoeff (n - i - 1) := by\n intro i hi\n rw [Finset.mem_range] at hi\n have hdesc : (n.descFactorial i : \u2102) = (n ! : \u2102) / ((n - i) ! : \u2102) := by\n have h2 := Nat.factorial_mul_descFactorial (show i \u2264 n by omega)\n have hcast : ((n - i) ! : \u2102) * (n.descFactorial i : \u2102) = (n ! : \u2102) := by\n exact_mod_cast h2\n rw [eq_div_iff_mul_eq (by simp [Nat.factorial_ne_zero])]\n rw [mul_comm]\n exact hcast\n rw [hdesc]\n have hlc : lcoeff (n - i - 1) = iteratedDeriv (n - i) hLi 1 / ((n - i) ! : \u2102) := by\n rw [hLi_iteratedDeriv_div_factorial (j := n - i) (by omega)]\n rw [hlc]\n field_simp\n ring\n rw [Finset.sum_div]\n rw [Finset.sum_congr rfl hterm]\n have hre : (\u2211 i \u2208 Finset.range n, (n.choose i : \u2102) * lcoeff (n - i - 1)) =\n \u2211 j \u2208 Finset.Icc 1 n, (n.choose j : \u2102) * lcoeff (j - 1) := by\n rw [Finset.sum_range_reflect]\n rw [Finset.sum_Icc_eq_sum_range]\n apply Finset.sum_congr rfl\n intro i hi\n rw [Finset.mem_range] at hi\n have e1 : n - 1 - i + 1 = n - i := by omega\n have e2 : n - (n - 1 - i) = i + 1 := by omega\n have e3 : n.choose (n - 1 - i) = n.choose (i + 1) := by\n rw [show n - 1 - i = n - (i + 1) by omega]\n exact Nat.choose_symm (by omega)\n have e4 : n - (n - 1 - i) - 1 = i := by omega\n rw [e1, e3]\n have : n - (i + 1) - 1 = i := by omega\n rw [this]\n exact hre\n\nend NguyenRH1\n"
}
result 2026-08-21 21:03:56Z → 2026-08-21 21:03:56Z
{
"type": "update",
"filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiResidue.lean",
"content": "/-\nNguyenRH1/LiResidue.lean \u2014 tier ii\u2032 sub-stage ii\u2032-1b (D-064 \u00a74 R1):\nthe w = 1 residue of the Lagarias-kernel integrand, computed exactly.\n\nContents (Part 1):\n* `zetaA w = (w\u22121)\u00b7\u03b6(w)` extended by 1 at w = 1 \u2014 analytic at 1 with\n value 1 (removable singularity; Mathlib `riemannZeta_residue_one` +\n `differentiableOn_update_limUnder_of_bddAbove`).\n* `hLi w = 1 \u2212 (w\u22121)\u00b7(zetaA\u2032/zetaA)(w)` \u2014 analytic at 1, hLi 1 = 1;\n agrees with (w\u22121)\u00b7(\u2212\u03b6\u2032/\u03b6)(w) on a punctured neighborhood of 1\n (`hLi_eq_near_one`).\n* `lcoeff k` \u2014 the Laurent coefficients of \u2212\u03b6\u2032/\u03b6 at 1, DEFINED as\n iteratedDeriv (k+1) hLi 1 / (k+1)!.\n* `ResW1 n` \u2014 the residue at w = 1 of J(w) = k_n(w\u22121)\u00b7(\u2212\u03b6\u2032/\u03b6(w)),\n packaged as (1/n!)\u00b7(d/dw)\u207f[(w\u207f\u2212(w\u22121)\u207f)\u00b7hLi] at w = 1 (D-064 \u00a74 R1:\n (w\u22121)^{n+1}J = [w\u207f\u2212(w\u22121)\u207f]\u00b7hLi on a punctured neighborhood, by\n `hLi_eq_near_one`). Value: `ResW1_eq_sum`.\n\nArchive references: D-036, D-037, D-064 (R1), journal-014/015.\n-/\nimport Mathlib\nimport Zeta23.Statement\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. The regularized factor zetaA = (w\u22121)\u03b6(w) at w = 1 -/\n\n/-- `zetaA w = (w\u22121)\u00b7\u03b6(w)` with the removable singularity at w = 1 filled\nby the residue value 1. Analytic at 1 (`zetaA_analyticAt_one`), value\n`zetaA 1 = 1`. -/\ndef zetaA : \u2102 \u2192 \u2102 := Function.update (fun w => (w - 1) * riemannZeta w) 1 1\n\nlemma zetaA_apply {w : \u2102} (hw : w \u2260 1) : zetaA w = (w - 1) * riemannZeta w :=\n Function.update_of_ne hw _ _\n\nlemma zetaA_one : zetaA 1 = 1 := Function.update_self _ _ _\n\n/-- The regularized factor is analytic at w = 1 (removable singularity). -/\nlemma zetaA_analyticAt_one : AnalyticAt \u2102 zetaA 1 := by\n have hdiff : DifferentiableOn \u2102 (fun w => (w - 1) * riemannZeta w)\n (Metric.ball 1 2 \\ {1}) := by\n intro w hw\n have hw1 : w \u2260 1 := hw.2\n exact ((differentiableAt_id.sub (differentiableAt_const 1)).mul\n (differentiableAt_riemannZeta hw1)).differentiableWithinAt\n have hbd : BddAbove (Complex.norm \u2218 (fun w => (w - 1) * riemannZeta w)) ''\n (Metric.ball 1 2 \\ {1}) := by\n have hT := riemannZeta_residue_one\n rw [Metric.tendsto_nhdsWithin_nhds] at hT\n obtain \u27e8\u03b4, h\u03b40, h\u03b4\u27e9 := hT 1 one_pos\n refine \u27e82, ?_\u27e9\n rintro _ \u27e8z, hz, rfl\u27e9\n have hz1 : z \u2260 1 := hz.2\n have hlt := h\u03b4 (by\n rw [dist_eq_norm, sub_zero]\n exact hz.1)\n have h1 : \u2016(z - 1) * riemannZeta z - 1\u2016 < 1 := by\n have := hlt\n rwa [dist_eq_norm] at this\n have := norm_sub_le ((z - 1) * riemannZeta z) 1\n simp only [Complex.norm_eq_abs] at *\n have h2 : \u2016(z - 1) * riemannZeta z\u2016 \u2264 \u2016(z - 1) * riemannZeta z - 1\u2016 + \u2016(1 : \u2102)\u2016 :=\n norm_sub_le ((z - 1) * riemannZeta z) 1\n rw [norm_one] at h2\n linarith [h1]\n have h := differentiableOn_update_limUnder_of_bddAbove\n (Metric.ball_mem_nhds 1 (by norm_num : (0 : \u211d) < 2)) hdiff hbd\n have hlim : limUnder (\ud835\udcdd[\u2260] (1 : \u2102)) (fun w => (w - 1) * riemannZeta w) = 1 :=\n riemannZeta_residue_one.limUnder_eq\n rw [hlim] at h\n have han := h.analyticOnNhd Metric.isOpen_ball\n exact han.analyticAt (Metric.ball_mem_nhds 1 (by norm_num : (0 : \u211d) < 2))\n\n/-- zetaA is nonzero on a neighborhood of 1 (value 1 there). -/\nlemma zetaA_ne_zero_near_one : \u2200\u1da0 w in \ud835\udcdd (1 : \u2102), zetaA w \u2260 0 :=\n (zetaA_analyticAt_one.continuousAt).eventually_ne (by rw [zetaA_one]; norm_num)\n\n/-- zetaA is analytic at any w \u2260 1 (agrees with (w\u22121)\u03b6 there). -/\nlemma zetaA_analyticAt_of_ne {w : \u2102} (hw : w \u2260 1) : AnalyticAt \u2102 zetaA w := by\n have h : (fun w => (w - 1) * riemannZeta w) =\u1da0[\ud835\udcdd w] zetaA := by\n filter_upwards [eventually_ne_nhds hw] with z hz using (zetaA_apply hz).symm\n have ha : AnalyticAt \u2102 (fun w => (w - 1) * riemannZeta w) w :=\n (analyticAt_id.sub analyticAt_const).mul\n (differentiableAt_riemannZeta hw).analyticAt\n exact ha.congr h\n\n/-! ## 2. hLi w = 1 \u2212 (w\u22121)\u00b7(zetaA\u2032/zetaA)(w): analytic at 1, value 1 -/\n\n/-- hLi(w) = 1 \u2212 (w\u22121)\u00b7(zetaA\u2032/zetaA)(w) \u2014 the analytic-at-1 form of\n(w\u22121)(\u2212\u03b6\u2032/\u03b6)(w) (`hLi_eq_near_one`). hLi 1 = 1. -/\ndef hLi (w : \u2102) : \u2102 := 1 - (w - 1) * (deriv zetaA w / zetaA w)\n\nlemma hLi_one : hLi 1 = 1 := by simp [hLi]\n\nlemma hLi_analyticAt_one : AnalyticAt \u2102 hLi 1 := by\n have ha := zetaA_analyticAt_one\n have hda : AnalyticAt \u2102 (deriv zetaA) 1 := ha.deriv\n have hne : zetaA 1 \u2260 0 := by rw [zetaA_one]; norm_num\n exact ((analyticAt_const.sub analyticAt_id).mul\n (hda.div ha hne)).const_sub 1\n\n/-- On the punctured plane minus zeros of \u03b6, hLi = (w\u22121)\u00b7(\u2212\u03b6\u2032/\u03b6). -/\nlemma hLi_eq_of_ne {w : \u2102} (hw1 : w \u2260 1) (hw0 : riemannZeta w \u2260 0) :\n hLi w = (w - 1) * (-(deriv riemannZeta w) / riemannZeta w) := by\n have hA : zetaA w = (w - 1) * riemannZeta w := zetaA_apply hw1\n have hdA : deriv zetaA w = riemannZeta w + (w - 1) * deriv riemannZeta w := by\n have h1 : deriv (fun z => (z - 1) * riemannZeta z) w =\n deriv (fun z => z - 1) w * riemannZeta w +\n (w - 1) * deriv riemannZeta w :=\n deriv_mul ((differentiableAt_id.sub (differentiableAt_const 1)))\n (differentiableAt_riemannZeta hw1)\n have h2 : deriv (fun z => z - 1) w = 1 := by\n simp [deriv_sub, deriv_id'']\n have h3 : (fun z => (z - 1) * riemannZeta z) =\u1da0[\ud835\udcdd w] zetaA := by\n filter_upwards [eventually_ne_nhds hw1] with z hz using (zetaA_apply hz).symm\n rw [h3.deriv_eq, h1, h2, one_mul]\n rw [hLi, hdA, hA]\n have hw1' : w - 1 \u2260 0 := sub_ne_zero.mpr hw1\n field_simp [hw0, hw1']\n ring\n\n/-- On a punctured neighborhood of 1, hLi = (w\u22121)\u00b7(\u2212\u03b6\u2032/\u03b6). -/\nlemma hLi_eq_near_one :\n \u2200\u1da0 w in \ud835\udcdd[\u2260] (1 : \u2102), hLi w = (w - 1) * (-(deriv riemannZeta w) / riemannZeta w) := by\n have hne : \u2200\u1da0 w in \ud835\udcdd[\u2260] (1 : \u2102), (w - 1) * riemannZeta w \u2260 0 :=\n riemannZeta_residue_one.eventually_ne (show (1 : \u2102) \u2260 0 by norm_num)\n filter_upwards [hne, eventually_mem_nhdsWithin] with w hw hw1\n have hz : riemannZeta w \u2260 0 := by\n have h2 := hw\n simp only [ne_eq, mul_eq_zero] at h2\n push_neg at h2\n exact h2.2\n exact hLi_eq_of_ne hw1 hz\n\n/-! ## 3. The Laurent coefficients of \u2212\u03b6\u2032/\u03b6 at 1 (operational definition) -/\n\n/-- The k-th Laurent coefficient of \u2212\u03b6\u2032/\u03b6 at s = 1, DEFINED as\niteratedDeriv (k+1) hLi 1 / (k+1)! (the power-series coefficient of the\nanalytic hLi; the identification with \u2212\u03b6\u2032/\u03b6's Laurent expansion is\n`hLi_eq_near_one`). -/\ndef lcoeff (k : \u2115) : \u2102 := iteratedDeriv (k + 1) hLi 1 / (k + 1) !\n\n/-- hLi's Taylor coefficients: iteratedDeriv j hLi 1 / j ! = lcoeff (j\u22121). -/\nlemma hLi_iteratedDeriv_div_factorial {j : \u2115} (hj : 1 \u2264 j) :\n iteratedDeriv j hLi 1 / j ! = lcoeff (j - 1) := by\n rw [lcoeff]\n have : j = (j - 1) + 1 := by omega\n rw [this]\n\n/-! ## 4. The A-polynomial derivative: A(w) = w\u207f \u2212 (w\u22121)\u207f -/\n\n/-- Iterated derivatives of A(w) = w\u207f \u2212 (w\u22121)\u207f at 1:\nA^{(i)}(1) = n.descFactorial i for i < n, and A^{(n)}(1) = 0. -/\nlemma A_iter (n i : \u2115) (hi : i \u2264 n) :\n iteratedDeriv i (fun w => w ^ n - (w - 1) ^ n) (1 : \u2102) =\n if i < n then n.descFactorial i else 0 := by\n have hf : ContDiffAt \u2102 i (fun w : \u2102 => w ^ n) 1 :=\n (contDiff_id.pow n).contDiffAt\n have hg : ContDiffAt \u2102 i (fun w : \u2102 => (w - 1) ^ n) 1 :=\n ((contDiff_id.sub contDiff_const).pow n).contDiffAt\n rw [iteratedDeriv_sub hf hg]\n have h1 : iteratedDeriv i (fun w : \u2102 => w ^ n) 1 = n.descFactorial i := by\n rw [iteratedDeriv_pow]\n simp\n have h2 : iteratedDeriv i (fun w : \u2102 => (w - 1) ^ n) 1 =\n n.descFactorial i * (0 : \u2102) ^ (n - i) := by\n have e := congr_fun (iteratedDeriv_comp_sub_const i (fun w : \u2102 => w ^ n) (1 : \u2102)) 1\n rw [iteratedDeriv_pow] at e\n simpa using e\n rw [h1, h2]\n by_cases hin : i < n\n \u00b7 rw [if_pos hin]\n have hz : (0 : \u2102) ^ (n - i) = 0 := zero_pow (by omega)\n rw [hz, mul_zero, sub_zero]\n \u00b7 rw [if_neg hin]\n have hin' : i = n := le_antisymm hi (by omega)\n subst hin'\n simp [Nat.descFactorial_self]\n\n/-! ## 5. The residue at w = 1: ResW1 n = \u03a3_{j=1}^n C(n,j)\u00b7lcoeff (j\u22121) -/\n\n/-- The residue at w = 1 of the Lagarias-kernel integrand\nJ(w) = k_n(w\u22121)\u00b7(\u2212\u03b6\u2032/\u03b6(w)), packaged as (1/n!)\u00b7(d/dw)\u207f[(w\u207f\u2212(w\u22121)\u207f)hLi]\nat w = 1 (D-064 \u00a74 R1: (w\u22121)^{n+1}J = [w\u207f\u2212(w\u22121)\u207f]\u00b7hLi punctured near 1,\nby `hLi_eq_near_one`). -/\ndef ResW1 (n : \u2115) : \u2102 :=\n iteratedDeriv n (fun w => (w ^ n - (w - 1) ^ n) * hLi w) (1 : \u2102) / n !\n\n/-- The w = 1 residue value: ResW1 n = \u03a3_{j=1}^n C(n,j)\u00b7lcoeff (j\u22121). -/\ntheorem ResW1_eq_sum (n : \u2115) :\n ResW1 n = \u2211 j \u2208 Finset.Icc 1 n, (n.choose j : \u2102) * lcoeff (j - 1) := by\n have hA : ContDiffAt \u2102 n (fun w : \u2102 => w ^ n - (w - 1) ^ n) 1 :=\n ((contDiff_id.pow n).sub ((contDiff_id.sub contDiff_const).pow n)).contDiffAt\n have hh : ContDiffAt \u2102 n hLi 1 := hLi_analyticAt_one.contDiffAt\n have hmul := iteratedDeriv_mul hA hh\n rw [ResW1, hmul]\n have hsum : (\u2211 i \u2208 Finset.range (n + 1),\n n.choose i * iteratedDeriv i (fun w : \u2102 => w ^ n - (w - 1) ^ n) 1 *\n iteratedDeriv (n - i) hLi 1) =\n \u2211 i \u2208 Finset.range n,\n n.choose i * (n.descFactorial i : \u2102) * iteratedDeriv (n - i) hLi 1 := by\n rw [Finset.sum_range_succ]\n simp [A_iter n n le_rfl]\n apply Finset.sum_congr rfl\n intro i hi\n rw [Finset.mem_range] at hi\n rw [A_iter n i (by omega), if_pos hi]\n rw [hsum]\n have hterm : \u2200 i \u2208 Finset.range n,\n n.choose i * (n.descFactorial i : \u2102) * iteratedDeriv (n - i) hLi 1 / n ! =\n (n.choose i : \u2102) * lcoeff (n - i - 1) := by\n intro i hi\n rw [Finset.mem_range] at hi\n have hdesc : (n.descFactorial i : \u2102) = (n ! : \u2102) / ((n - i) ! : \u2102) := by\n have h2 := Nat.factorial_mul_descFactorial (show i \u2264 n by omega)\n have hcast : ((n - i) ! : \u2102) * (n.descFactorial i : \u2102) = (n ! : \u2102) := by\n exact_mod_cast h2\n rw [eq_div_iff_mul_eq (by simp [Nat.factorial_ne_zero])]\n rw [mul_comm]\n exact hcast\n rw [hdesc]\n have hlc : lcoeff (n - i - 1) = iteratedDeriv (n - i) hLi 1 / ((n - i) ! : \u2102) := by\n rw [hLi_iteratedDeriv_div_factorial (j := n - i) (by omega)]\n rw [hlc]\n field_simp\n ring\n rw [Finset.sum_div]\n rw [Finset.sum_congr rfl hterm]\n have hre : (\u2211 i \u2208 Finset.range n, (n.choose i : \u2102) * lcoeff (n - i - 1)) =\n \u2211 j \u2208 Finset.Icc 1 n, (n.choose j : \u2102) * lcoeff (j - 1) := by\n rw [Finset.sum_range_reflect]\n rw [Finset.sum_Icc_eq_sum_range]\n apply Finset.sum_congr rfl\n intro i hi\n rw [Finset.mem_range] at hi\n have e1 : n - 1 - i + 1 = n - i := by omega\n have e2 : n - (n - 1 - i) = i + 1 := by omega\n have e3 : n.choose (n - 1 - i) = n.choose (i + 1) := by\n rw [show n - 1 - i = n - (i + 1) by omega]\n exact Nat.choose_symm (by omega)\n have e4 : n - (n - 1 - i) - 1 = i := by omega\n rw [e1, e3]\n have : n - (i + 1) - 1 = i := by omega\n rw [this]\n exact hre\n\nend NguyenRH1\n",
"structuredPatch": [
{
"oldStart": 2,
"oldLines": 7,
"newStart": 2,
"newLines": 7,
"lines": [
" NguyenRH1/LiResidue.lean \u2014 tier ii\u2032 sub-stage ii\u2032-1b (D-064 \u00a74 R1):",
" the w = 1 residue of the Lagarias-kernel integrand, computed exactly.",
" ",
"-Contents (Part 1, this file's core):",
"+Contents (Part 1):",
" * `zetaA w = (w\u22121)\u00b7\u03b6(w)` extended by 1 at w = 1 \u2014 analytic at 1 with",
" value 1 (removable singularity; Mathlib `riemannZeta_residue_one` +",
" `differentiableOn_update_limUnder_of_bddAbove`)."
]
},
{
"oldStart": 10,
"oldLines": 12,
"newStart": 10,
"newLines": 11,
"lines": [
" agrees with (w\u22121)\u00b7(\u2212\u03b6\u2032/\u03b6)(w) on a punctured neighborhood of 1",
" (`hLi_eq_near_one`).",
" * `lcoeff k` \u2014 the Laurent coefficients of \u2212\u03b6\u2032/\u03b6 at 1, DEFINED as",
"- iteratedDeriv (k+1) hLi 1 / (k+1)! (operational; no Laurent series",
"- needed at this stage).",
"+ iteratedDeriv (k+1) hLi 1 / (k+1)!.",
" * `ResW1 n` \u2014 the residue at w = 1 of J(w) = k_n(w\u22121)\u00b7(\u2212\u03b6\u2032/\u03b6(w)),",
"- computed by the Leibniz identity (w\u22121)^{n+1}J = [w\u207f\u2212(w\u22121)\u207f]\u00b7hLi",
"- (D-064 \u00a74 R1, verified algebraically in session 014):",
"- ResW1 n = \u03a3_{j=1}^n C(n,j)\u00b7lcoeff (j\u22121) =: `ResW1_eq_sum`.",
"+ packaged as (1/n!)\u00b7(d/dw)\u207f[(w\u207f\u2212(w\u22121)\u207f)\u00b7hLi] at w = 1 (D-064 \u00a74 R1:",
"+ (w\u22121)^{n+1}J = [w\u207f\u2212(w\u22121)\u207f]\u00b7hLi on a punctured neighborhood, by",
"+ `hLi_eq_near_one`). Value: `ResW1_eq_sum`.",
" ",
" Archive references: D-036, D-037, D-064 (R1), journal-014/015.",
" -/"
]
},
{
"oldStart": 40,
"oldLines": 63,
"newStart": 39,
"newLines": 52,
"lines": [
" ",
" lemma zetaA_one : zetaA 1 = 1 := Function.update_self _ _ _",
" ",
"-lemma zetaA_tendsto : Tendsto (fun w => (w - 1) * riemannZeta w) (\ud835\udcdd[\u2260] 1) (\ud835\udcdd 1) :=",
"- riemannZeta_residue_one",
"-",
" /-- The regularized factor is analytic at w = 1 (removable singularity). -/",
" lemma zetaA_analyticAt_one : AnalyticAt \u2102 zetaA 1 := by",
" have hdiff : DifferentiableOn \u2102 (fun w => (w - 1) * riemannZeta w)",
" (Metric.ball 1 2 \\ {1}) := by",
" intro w hw",
" have hw1 : w \u2260 1 := hw.2",
"- exact (differentiableAt_id.sub (differentiableAt_const 1)).mul",
"- (differentiableAt_riemannZeta hw1) |>.differentiableWithinAt",
"+ exact ((differentiableAt_id.sub (differentiableAt_const 1)).mul",
"+ (differentiableAt_riemannZeta hw1)).differentiableWithinAt",
" have hbd : BddAbove (Complex.norm \u2218 (fun w => (w - 1) * riemannZeta w)) ''",
" (Metric.ball 1 2 \\ {1}) := by",
"- have hT := zetaA_tendsto",
"+ have hT := riemannZeta_residue_one",
" rw [Metric.tendsto_nhdsWithin_nhds] at hT",
" obtain \u27e8\u03b4, h\u03b40, h\u03b4\u27e9 := hT 1 one_pos",
" refine \u27e82, ?_\u27e9",
" rintro _ \u27e8z, hz, rfl\u27e9",
"- have h1 : dist (z - 1) 0 = \u2016z - 1\u2016 := by",
"- rw [dist_eq_norm]; simp [sub_zero]",
" have hz1 : z \u2260 1 := hz.2",
"- have hzz : dist z 1 < \u03b4 := by",
"- have := hz.1",
"- rw [Metric.mem_ball, dist_comm] at this",
"- exact this",
"- have hlt := h\u03b4 (by rwa [dist_zero_right, h1] at *)",
"- have : \u2016(z - 1) * riemannZeta z\u2016 \u2264 \u2016(1 : \u2102)\u2016 + 1 := by",
"- have := norm_sub_le_of_le hlt",
"- calc \u2016(z - 1) * riemannZeta z\u2016",
"- \u2264 \u2016(z - 1) * riemannZeta z - 1\u2016 + \u2016(1 : \u2102)\u2016 := by",
"- have := norm_sub_le ((z - 1) * riemannZeta z) 1",
"- linarith [this, hlt]",
"- _ \u2264 2 := by",
"- have h2 := hlt",
"- rw [norm_one]",
"- linarith [h2]",
"- exact this",
"+ have hlt := h\u03b4 (by",
"+ rw [dist_eq_norm, sub_zero]",
"+ exact hz.1)",
"+ have h1 : \u2016(z - 1) * riemannZeta z - 1\u2016 < 1 := by",
"+ have := hlt",
"+ rwa [dist_eq_norm] at this",
"+ have := norm_sub_le ((z - 1) * riemannZeta z) 1",
"+ simp only [Complex.norm_eq_abs] at *",
"+ have h2 : \u2016(z - 1) * riemannZeta z\u2016 \u2264 \u2016(z - 1) * riemannZeta z - 1\u2016 + \u2016(1 : \u2102)\u2016 :=",
"+ norm_sub_le ((z - 1) * riemannZeta z) 1",
"+ rw [norm_one] at h2",
"+ linarith [h1]",
" have h := differentiableOn_update_limUnder_of_bddAbove",
" (Metric.ball_mem_nhds 1 (by norm_num : (0 : \u211d) < 2)) hdiff hbd",
" have hlim : limUnder (\ud835\udcdd[\u2260] (1 : \u2102)) (fun w => (w - 1) * riemannZeta w) = 1 :=",
"- zetaA_tendsto.limUnder_eq",
"+ riemannZeta_residue_one.limUnder_eq",
" rw [hlim] at h",
"- have hopen : IsOpen (Metric.ball (1 : \u2102) 2) := Metric.isOpen_ball",
"- have han := h.analyticOnNhd hopen",
"+ have han := h.analyticOnNhd Metric.isOpen_ball",
" exact han.analyticAt (Metric.ball_mem_nhds 1 (by norm_num : (0 : \u211d) < 2))",
" ",
" /-- zetaA is nonzero on a neighborhood of 1 (value 1 there). -/",
" lemma zetaA_ne_zero_near_one : \u2200\u1da0 w in \ud835\udcdd (1 : \u2102), zetaA w \u2260 0 :=",
" (zetaA_analyticAt_one.continuousAt).eventually_ne (by rw [zetaA_one]; norm_num)",
" ",
"-/-- zetaA is analytic everywhere except possibly at 1 \u2014 and in fact also",
"-at 1; we record the off-1 version for quotient computations. -/",
"+/-- zetaA is analytic at any w \u2260 1 (agrees with (w\u22121)\u03b6 there). -/",
" lemma zetaA_analyticAt_of_ne {w : \u2102} (hw : w \u2260 1) : AnalyticAt \u2102 zetaA w := by",
" have h : (fun w => (w - 1) * riemannZeta w) =\u1da0[\ud835\udcdd w] zetaA := by",
" filter_upwards [eventually_ne_nhds hw] with z hz using (zetaA_apply hz).symm",
"- have ha : AnalyticAt \u2102 (fun w => (w - 1) * riemannZeta w) w := by",
"- exact (analyticAt_id.sub analyticAt_const).mul",
"+ have ha : AnalyticAt \u2102 (fun w => (w - 1) * riemannZeta w) w :=",
"+ (analyticAt_id.sub analyticAt_const).mul",
" (differentiableAt_riemannZeta hw).analyticAt",
" exact ha.congr h",
" "
]
},
{
"oldStart": 112,
"oldLines": 10,
"newStart": 100,
"newLines": 10,
"lines": [
" have ha := zetaA_analyticAt_one",
" have hda : AnalyticAt \u2102 (deriv zetaA) 1 := ha.deriv",
" have hne : zetaA 1 \u2260 0 := by rw [zetaA_one]; norm_num",
"- exact (analyticAt_const.sub analyticAt_id).mul",
"- (hda.div ha hne) |>.const_sub 1",
"+ exact ((analyticAt_const.sub analyticAt_id).mul",
"+ (hda.div ha hne)).const_sub 1",
" ",
"-/-- On a punctured neighborhood of 1, hLi = (w\u22121)\u00b7(\u2212\u03b6\u2032/\u03b6). -/",
"+/-- On the punctured plane minus zeros of \u03b6, hLi = (w\u22121)\u00b7(\u2212\u03b6\u2032/\u03b6). -/",
" lemma hLi_eq_of_ne {w : \u2102} (hw1 : w \u2260 1) (hw0 : riemannZeta w \u2260 0) :",
" hLi w = (w - 1) * (-(deriv riemannZeta w) / riemannZeta w) := by",
" have hA : zetaA w = (w - 1) * riemannZeta w := zetaA_apply hw1"
]
},
{
"oldStart": 135,
"oldLines": 30,
"newStart": 123,
"newLines": 28,
"lines": [
" field_simp [hw0, hw1']",
" ring",
" ",
"-/-- The punctured-neighborhood form, for later contour work. -/",
"+/-- On a punctured neighborhood of 1, hLi = (w\u22121)\u00b7(\u2212\u03b6\u2032/\u03b6). -/",
" lemma hLi_eq_near_one :",
" \u2200\u1da0 w in \ud835\udcdd[\u2260] (1 : \u2102), hLi w = (w - 1) * (-(deriv riemannZeta w) / riemannZeta w) := by",
"- have hzero : \u2200\u1da0 w in \ud835\udcdd[\u2260] (1 : \u2102), riemannZeta w \u2260 0 := by",
"- have h1 : (1 : \u2102) \u2208 {s : \u2102 | 1 \u2264 s.re} := by simp",
"- filter_upwards [eventually_mem_nhdsWithin] with w hw",
"- have hwre : 1 \u2264 w.re := by",
"- have := hw.2",
"- sorry",
"- exact riemannZeta_ne_zero_of_one_le_re hwre",
"- filter_upwards [hzero, eventually_mem_nhdsWithin] with w hw0 hw1",
"- exact hLi_eq_of_ne hw1 hw0",
"+ have hne : \u2200\u1da0 w in \ud835\udcdd[\u2260] (1 : \u2102), (w - 1) * riemannZeta w \u2260 0 :=",
"+ riemannZeta_residue_one.eventually_ne (show (1 : \u2102) \u2260 0 by norm_num)",
"+ filter_upwards [hne, eventually_mem_nhdsWithin] with w hw hw1",
"+ have hz : riemannZeta w \u2260 0 := by",
"+ have h2 := hw",
"+ simp only [ne_eq, mul_eq_zero] at h2",
"+ push_neg at h2",
"+ exact h2.2",
"+ exact hLi_eq_of_ne hw1 hz",
" ",
" /-! ## 3. The Laurent coefficients of \u2212\u03b6\u2032/\u03b6 at 1 (operational definition) -/",
" ",
"-/-- The k-th Laurent coefficient of \u2212\u03b6\u2032/\u03b6 at s = 1:",
"-\u2212\u03b6\u2032/\u03b6(1+u) = u\u207b\u00b9 + \u03a3_{k\u22650} lcoeff k \u00b7 u^k (identification proved in",
"-tier ii\u2032-2/3; here lcoeff is DEFINED via the analytic hLi). -/",
"+/-- The k-th Laurent coefficient of \u2212\u03b6\u2032/\u03b6 at s = 1, DEFINED as",
"+iteratedDeriv (k+1) hLi 1 / (k+1)! (the power-series coefficient of the",
"+analytic hLi; the identification with \u2212\u03b6\u2032/\u03b6's Laurent expansion is",
"+`hLi_eq_near_one`). -/",
" def lcoeff (k : \u2115) : \u2102 := iteratedDeriv (k + 1) hLi 1 / (k + 1) !",
" ",
"-lemma lcoeff_eq (k : \u2115) :",
"- lcoeff k = iteratedDeriv (k + 1) hLi 1 / (k + 1) ! := rfl",
"-",
"-/-- hLi's Taylor coefficient form: iteratedDeriv j hLi 1 / j ! = lcoeff (j\u22121). -/",
"+/-- hLi's Taylor coefficients: iteratedDeriv j hLi 1 / j ! = lcoeff (j\u22121). -/",
" lemma hLi_iteratedDeriv_div_factorial {j : \u2115} (hj : 1 \u2264 j) :",
" iteratedDeriv j hLi 1 / j ! = lcoeff (j - 1) := by",
" rw [lcoeff]"
]
},
{
"oldStart": 182,
"oldLines": 20,
"newStart": 168,
"newLines": 14,
"lines": [
" simp",
" have h2 : iteratedDeriv i (fun w : \u2102 => (w - 1) ^ n) 1 =",
" n.descFactorial i * (0 : \u2102) ^ (n - i) := by",
"- have e := iteratedDeriv_comp_sub_const i (fun w : \u2102 => w ^ n) (1 : \u2102)",
"- have e2 : iteratedDeriv i (fun w : \u2102 => (w - 1) ^ n) 1 =",
"- iteratedDeriv i (fun w : \u2102 => w ^ n) (1 - 1) := by",
"- have := congr_fun e 1",
"- convert this using 2",
"- rw [e2, iteratedDeriv_pow]",
"- simp",
"+ have e := congr_fun (iteratedDeriv_comp_sub_const i (fun w : \u2102 => w ^ n) (1 : \u2102)) 1",
"+ rw [iteratedDeriv_pow] at e",
"+ simpa using e",
" rw [h1, h2]",
" by_cases hin : i < n",
" \u00b7 rw [if_pos hin]",
"- have : (0 : \u2102) ^ (n - i) = 0 := by",
"- apply zero_pow",
"- omega",
"- rw [this, mul_zero, sub_zero]",
"+ have hz : (0 : \u2102) ^ (n - i) = 0 := zero_pow (by omega)",
"+ rw [hz, mul_zero, sub_zero]",
" \u00b7 rw [if_neg hin]",
" have hin' : i = n := le_antisymm hi (by omega)",
" subst hin'"
]
},
{
"oldStart": 205,
"oldLines": 8,
"newStart": 185,
"newLines": 8,
"lines": [
" ",
" /-- The residue at w = 1 of the Lagarias-kernel integrand",
" J(w) = k_n(w\u22121)\u00b7(\u2212\u03b6\u2032/\u03b6(w)), packaged as (1/n!)\u00b7(d/dw)\u207f[(w\u207f\u2212(w\u22121)\u207f)hLi]",
"-at w = 1 (D-064 \u00a74 R1: (w\u22121)^{n+1}J = [w\u207f\u2212(w\u22121)\u207f]\u00b7hLi on a punctured",
"-neighborhood, by `hLi_eq_near_one`). -/",
"+at w = 1 (D-064 \u00a74 R1: (w\u22121)^{n+1}J = [w\u207f\u2212(w\u22121)\u207f]\u00b7hLi punctured near 1,",
"+by `hLi_eq_near_one`). -/",
" def ResW1 (n : \u2115) : \u2102 :=",
" iteratedDeriv n (fun w => (w ^ n - (w - 1) ^ n) * hLi w) (1 : \u2102) / n !",
" "
]
},
{
"oldStart": 218,
"oldLines": 86,
"newStart": 198,
"newLines": 55,
"lines": [
" have hh : ContDiffAt \u2102 n hLi 1 := hLi_analyticAt_one.contDiffAt",
" have hmul := iteratedDeriv_mul hA hh",
" rw [ResW1, hmul]",
"- have hsum : \u2211 i \u2208 Finset.range (n + 1),",
"+ have hsum : (\u2211 i \u2208 Finset.range (n + 1),",
" n.choose i * iteratedDeriv i (fun w : \u2102 => w ^ n - (w - 1) ^ n) 1 *",
"- iteratedDeriv (n - i) hLi 1 =",
"+ iteratedDeriv (n - i) hLi 1) =",
" \u2211 i \u2208 Finset.range n,",
" n.choose i * (n.descFactorial i : \u2102) * iteratedDeriv (n - i) hLi 1 := by",
"- apply Finset.sum_subset (Finset.range_le_iff.mpr (Nat.le_succ n))",
"+ rw [Finset.sum_range_succ]",
"+ simp [A_iter n n le_rfl]",
"+ apply Finset.sum_congr rfl",
" intro i hi",
" rw [Finset.mem_range] at hi",
"- have hi0 : i \u2260 n := by omega",
"- rw [A_iter n i (by omega), if_pos (by omega)]",
"- \u00b7 rfl",
"- \u00b7 rw [Finset.mem_range] at *",
"- omega",
"+ rw [A_iter n i (by omega), if_pos hi]",
" rw [hsum]",
"- have hfinal : (\u2211 i \u2208 Finset.range n,",
"- n.choose i * (n.descFactorial i : \u2102) * iteratedDeriv (n - i) hLi 1) / n ! =",
"+ have hterm : \u2200 i \u2208 Finset.range n,",
"+ n.choose i * (n.descFactorial i : \u2102) * iteratedDeriv (n - i) hLi 1 / n ! =",
"+ (n.choose i : \u2102) * lcoeff (n - i - 1) := by",
"+ intro i hi",
"+ rw [Finset.mem_range] at hi",
"+ have hdesc : (n.descFactorial i : \u2102) = (n ! : \u2102) / ((n - i) ! : \u2102) := by",
"+ have h2 := Nat.factorial_mul_descFactorial (show i \u2264 n by omega)",
"+ have hcast : ((n - i) ! : \u2102) * (n.descFactorial i : \u2102) = (n ! : \u2102) := by",
"+ exact_mod_cast h2",
"+ rw [eq_div_iff_mul_eq (by simp [Nat.factorial_ne_zero])]",
"+ rw [mul_comm]",
"+ exact hcast",
"+ rw [hdesc]",
"+ have hlc : lcoeff (n - i - 1) = iteratedDeriv (n - i) hLi 1 / ((n - i) ! : \u2102) := by",
"+ rw [hLi_iteratedDeriv_div_factorial (j := n - i) (by omega)]",
"+ rw [hlc]",
"+ field_simp",
"+ ring",
"+ rw [Finset.sum_div]",
"+ rw [Finset.sum_congr rfl hterm]",
"+ have hre : (\u2211 i \u2208 Finset.range n, (n.choose i : \u2102) * lcoeff (n - i - 1)) =",
" \u2211 j \u2208 Finset.Icc 1 n, (n.choose j : \u2102) * lcoeff (j - 1) := by",
"- have hrewrite : \u2200 i \u2208 Finset.range n,",
"- n.choose i * (n.descFactorial i : \u2102) * iteratedDeriv (n - i) hLi 1 / n ! =",
"- (n.choose (n - i) : \u2102) * lcoeff (n - i - 1) := by",
"- intro i hi",
"- rw [Finset.mem_range] at hi",
"- have hcd : (n.choose i : \u2102) * (n.descFactorial i : \u2102) =",
"- n ! * n.choose i / (n - i) ! := by",
"- have h1 := Nat.choose_mul_factorial_mul_factorial (show i \u2264 n by omega)",
"- have h2 := Nat.factorial_mul_descFactorial (show i \u2264 n by omega)",
"- have : (n.choose i : \u2102) * (n.descFactorial i : \u2102) * ((i ! : \u2102) * ((n - i) ! : \u2102)) =",
"- (n ! : \u2102) * (n.choose i : \u2102) := by",
"- push_cast [h1, h2]",
"- ring",
"- have hfact : ((i ! : \u2102) * ((n - i) ! : \u2102)) \u2260 0 := by",
"- simp [Nat.factorial_ne_zero]",
"- have hthis := this",
"- field_simp at hthis \u22a2",
"- have h3 : (n.choose i : \u2102) * (n.descFactorial i : \u2102) * ((n - i) ! : \u2102) =",
"- (n ! : \u2102) * (n.choose i : \u2102) / 1 := by",
"- have h4 := hthis",
"- rw [mul_comm ((i ! : \u2102)) ((n - i) ! : \u2102)] at h4",
"- have h5 : (n.choose i : \u2102) * (n.descFactorial i : \u2102) * ((n - i) ! : \u2102) * (i ! : \u2102) =",
"- (n ! : \u2102) * (n.choose i : \u2102) := by",
"- rw [mul_comm ((n - i) ! : \u2102) (i ! : \u2102)] at h4",
"- calc (n.choose i : \u2102) * (n.descFactorial i : \u2102) * ((n - i) ! : \u2102) * (i ! : \u2102)",
"- = (n.choose i : \u2102) * (n.descFactorial i : \u2102) * (((n - i) ! : \u2102) * (i ! : \u2102)) := by ring",
"- _ = (n ! : \u2102) * (n.choose i : \u2102) := by",
"- have := h4",
"- ring_nf at this \u22a2",
"- convert this using 1",
"- ring",
"- exact (div_eq_one_iff_eq (by simp [Nat.factorial_ne_zero])).mpr h5",
"- field_simp at h3 \u22a2",
"- calc (n.choose i : \u2102) * (n.descFactorial i : \u2102)",
"- = ((n ! : \u2102) * (n.choose i : \u2102) / 1) / ((n - i) ! : \u2102) := by",
"- rw [\u2190 h3]",
"- field_simp",
"- ring",
"- _ = (n ! : \u2102) * (n.choose i : \u2102) / ((n - i) ! : \u2102) := by ring",
"- rw [hcd]",
"- have hni : n - i \u2265 1 := by omega",
"- rw [hLi_iteratedDeriv_div_factorial (j := n - i) (by omega)]",
"- rw [show n - i - 1 = n - i - 1 from rfl]",
"- have hcoe : ((n - i) ! : \u2102) \u2260 0 := by simp [Nat.factorial_ne_zero]",
"- field_simp",
"- rw [Nat.choose_symm (by omega : i \u2264 n)]",
"- ring",
"- rw [Finset.sum_div]",
"- rw [Finset.sum_congr rfl hrewrite]",
"- have hmap : \u2211 i \u2208 Finset.range n, (n.choose (n - i) : \u2102) * lcoeff (n - i - 1) =",
"- \u2211 j \u2208 Finset.Icc 1 n, (n.choose j : \u2102) * lcoeff (j - 1) := by",
"- rw [Finset.sum_range_reflect]",
"- apply Finset.sum_congr rfl",
"- intro i hi",
"- rw [Finset.mem_range] at hi",
"- have : n - 1 - i + 1 = n - i := by omega",
"- rw [this]",
"- have : n - (n - i) = i := by omega",
"- rw [Nat.choose_symm (show n - i \u2264 n by omega)]",
"- simp [this]",
"- ring",
"- exact hmap",
"- rw [hfinal]",
"+ rw [Finset.sum_range_reflect]",
"+ rw [Finset.sum_Icc_eq_sum_range]",
"+ apply Finset.sum_congr rfl",
"+ intro i hi",
"+ rw [Finset.mem_range] at hi",
"+ have e1 : n - 1 - i + 1 = n - i := by omega",
"+ have e2 : n - (n - 1 - i) = i + 1 := by omega",
"+ have e3 : n.choose (n - 1 - i) = n.choose (i + 1) := by",
"+ rw [show n - 1 - i = n - (i + 1) by omega]",
"+ exact Nat.choose_symm (by omega)",
"+ have e4 : n - (n - 1 - i) - 1 = i := by omega",
"+ rw [e1, e3]",
"+ have : n - (i + 1) - 1 = i := by omega",
"+ rw [this]",
"+ exact hre",
" ",
" end NguyenRH1",
" "
]
}
],
"originalFile": "/-\nNguyenRH1/LiResidue.lean \u2014 tier ii\u2032 sub-stage ii\u2032-1b (D-064 \u00a74 R1):\nthe w = 1 residue of the Lagarias-kernel integrand, computed exactly.\n\nContents (Part 1, this file's core):\n* `zetaA w = (w\u22121)\u00b7\u03b6(w)` extended by 1 at w = 1 \u2014 analytic at 1 with\n value 1 (removable singularity; Mathlib `riemannZeta_residue_one` +\n `differentiableOn_update_limUnder_of_bddAbove`).\n* `hLi w = 1 \u2212 (w\u22121)\u00b7(zetaA\u2032/zetaA)(w)` \u2014 analytic at 1, hLi 1 = 1;\n agrees with (w\u22121)\u00b7(\u2212\u03b6\u2032/\u03b6)(w) on a punctured neighborhood of 1\n (`hLi_eq_near_one`).\n* `lcoeff k` \u2014 the Laurent coefficients of \u2212\u03b6\u2032/\u03b6 at 1, DEFINED as\n iteratedDeriv (k+1) hLi 1 / (k+1)! (operational; no Laurent series\n needed at this stage).\n* `ResW1 n` \u2014 the residue at w = 1 of J(w) = k_n(w\u22121)\u00b7(\u2212\u03b6\u2032/\u03b6(w)),\n computed by the Leibniz identity (w\u22121)^{n+1}J = [w\u207f\u2212(w\u22121)\u207f]\u00b7hLi\n (D-064 \u00a74 R1, verified algebraically in session 014):\n ResW1 n = \u03a3_{j=1}^n C(n,j)\u00b7lcoeff (j\u22121) =: `ResW1_eq_sum`.\n\nArchive references: D-036, D-037, D-064 (R1), journal-014/015.\n-/\nimport Mathlib\nimport Zeta23.Statement\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. The regularized factor zetaA = (w\u22121)\u03b6(w) at w = 1 -/\n\n/-- `zetaA w = (w\u22121)\u00b7\u03b6(w)` with the removable singularity at w = 1 filled\nby the residue value 1. Analytic at 1 (`zetaA_analyticAt_one`), value\n`zetaA 1 = 1`. -/\ndef zetaA : \u2102 \u2192 \u2102 := Function.update (fun w => (w - 1) * riemannZeta w) 1 1\n\nlemma zetaA_apply {w : \u2102} (hw : w \u2260 1) : zetaA w = (w - 1) * riemannZeta w :=\n Function.update_of_ne hw _ _\n\nlemma zetaA_one : zetaA 1 = 1 := Function.update_self _ _ _\n\nlemma zetaA_tendsto : Tendsto (fun w => (w - 1) * riemannZeta w) (\ud835\udcdd[\u2260] 1) (\ud835\udcdd 1) :=\n riemannZeta_residue_one\n\n/-- The regularized factor is analytic at w = 1 (removable singularity). -/\nlemma zetaA_analyticAt_one : AnalyticAt \u2102 zetaA 1 := by\n have hdiff : DifferentiableOn \u2102 (fun w => (w - 1) * riemannZeta w)\n (Metric.ball 1 2 \\ {1}) := by\n intro w hw\n have hw1 : w \u2260 1 := hw.2\n exact (differentiableAt_id.sub (differentiableAt_const 1)).mul\n (differentiableAt_riemannZeta hw1) |>.differentiableWithinAt\n have hbd : BddAbove (Complex.norm \u2218 (fun w => (w - 1) * riemannZeta w)) ''\n (Metric.ball 1 2 \\ {1}) := by\n have hT := zetaA_tendsto\n rw [Metric.tendsto_nhdsWithin_nhds] at hT\n obtain \u27e8\u03b4, h\u03b40, h\u03b4\u27e9 := hT 1 one_pos\n refine \u27e82, ?_\u27e9\n rintro _ \u27e8z, hz, rfl\u27e9\n have h1 : dist (z - 1) 0 = \u2016z - 1\u2016 := by\n rw [dist_eq_norm]; simp [sub_zero]\n have hz1 : z \u2260 1 := hz.2\n have hzz : dist z 1 < \u03b4 := by\n have := hz.1\n rw [Metric.mem_ball, dist_comm] at this\n exact this\n have hlt := h\u03b4 (by rwa [dist_zero_right, h1] at *)\n have : \u2016(z - 1) * riemannZeta z\u2016 \u2264 \u2016(1 : \u2102)\u2016 + 1 := by\n have := norm_sub_le_of_le hlt\n calc \u2016(z - 1) * riemannZeta z\u2016\n \u2264 \u2016(z - 1) * riemannZeta z - 1\u2016 + \u2016(1 : \u2102)\u2016 := by\n have := norm_sub_le ((z - 1) * riemannZeta z) 1\n linarith [this, hlt]\n _ \u2264 2 := by\n have h2 := hlt\n rw [norm_one]\n linarith [h2]\n exact this\n have h := differentiableOn_update_limUnder_of_bddAbove\n (Metric.ball_mem_nhds 1 (by norm_num : (0 : \u211d) < 2)) hdiff hbd\n have hlim : limUnder (\ud835\udcdd[\u2260] (1 : \u2102)) (fun w => (w - 1) * riemannZeta w) = 1 :=\n zetaA_tendsto.limUnder_eq\n rw [hlim] at h\n have hopen : IsOpen (Metric.ball (1 : \u2102) 2) := Metric.isOpen_ball\n have han := h.analyticOnNhd hopen\n exact han.analyticAt (Metric.ball_mem_nhds 1 (by norm_num : (0 : \u211d) < 2))\n\n/-- zetaA is nonzero on a neighborhood of 1 (value 1 there). -/\nlemma zetaA_ne_zero_near_one : \u2200\u1da0 w in \ud835\udcdd (1 : \u2102), zetaA w \u2260 0 :=\n (zetaA_analyticAt_one.continuousAt).eventually_ne (by rw [zetaA_one]; norm_num)\n\n/-- zetaA is analytic everywhere except possibly at 1 \u2014 and in fact also\nat 1; we record the off-1 version for quotient computations. -/\nlemma zetaA_analyticAt_of_ne {w : \u2102} (hw : w \u2260 1) : AnalyticAt \u2102 zetaA w := by\n have h : (fun w => (w - 1) * riemannZeta w) =\u1da0[\ud835\udcdd w] zetaA := by\n filter_upwards [eventually_ne_nhds hw] with z hz using (zetaA_apply hz).symm\n have ha : AnalyticAt \u2102 (fun w => (w - 1) * riemannZeta w) w := by\n exact (analyticAt_id.sub analyticAt_const).mul\n (differentiableAt_riemannZeta hw).analyticAt\n exact ha.congr h\n\n/-! ## 2. hLi w = 1 \u2212 (w\u22121)\u00b7(zetaA\u2032/zetaA)(w): analytic at 1, value 1 -/\n\n/-- hLi(w) = 1 \u2212 (w\u22121)\u00b7(zetaA\u2032/zetaA)(w) \u2014 the analytic-at-1 form of\n(w\u22121)(\u2212\u03b6\u2032/\u03b6)(w) (`hLi_eq_near_one`). hLi 1 = 1. -/\ndef hLi (w : \u2102) : \u2102 := 1 - (w - 1) * (deriv zetaA w / zetaA w)\n\nlemma hLi_one : hLi 1 = 1 := by simp [hLi]\n\nlemma hLi_analyticAt_one : AnalyticAt \u2102 hLi 1 := by\n have ha := zetaA_analyticAt_one\n have hda : AnalyticAt \u2102 (deriv zetaA) 1 := ha.deriv\n have hne : zetaA 1 \u2260 0 := by rw [zetaA_one]; norm_num\n exact (analyticAt_const.sub analyticAt_id).mul\n (hda.div ha hne) |>.const_sub 1\n\n/-- On a punctured neighborhood of 1, hLi = (w\u22121)\u00b7(\u2212\u03b6\u2032/\u03b6). -/\nlemma hLi_eq_of_ne {w : \u2102} (hw1 : w \u2260 1) (hw0 : riemannZeta w \u2260 0) :\n hLi w = (w - 1) * (-(deriv riemannZeta w) / riemannZeta w) := by\n have hA : zetaA w = (w - 1) * riemannZeta w := zetaA_apply hw1\n have hdA : deriv zetaA w = riemannZeta w + (w - 1) * deriv riemannZeta w := by\n have h1 : deriv (fun z => (z - 1) * riemannZeta z) w =\n deriv (fun z => z - 1) w * riemannZeta w +\n (w - 1) * deriv riemannZeta w :=\n deriv_mul ((differentiableAt_id.sub (differentiableAt_const 1)))\n (differentiableAt_riemannZeta hw1)\n have h2 : deriv (fun z => z - 1) w = 1 := by\n simp [deriv_sub, deriv_id'']\n have h3 : (fun z => (z - 1) * riemannZeta z) =\u1da0[\ud835\udcdd w] zetaA := by\n filter_upwards [eventually_ne_nhds hw1] with z hz using (zetaA_apply hz).symm\n rw [h3.deriv_eq, h1, h2, one_mul]\n rw [hLi, hdA, hA]\n have hw1' : w - 1 \u2260 0 := sub_ne_zero.mpr hw1\n field_simp [hw0, hw1']\n ring\n\n/-- The punctured-neighborhood form, for later contour work. -/\nlemma hLi_eq_near_one :\n \u2200\u1da0 w in \ud835\udcdd[\u2260] (1 : \u2102), hLi w = (w - 1) * (-(deriv riemannZeta w) / riemannZeta w) := by\n have hzero : \u2200\u1da0 w in \ud835\udcdd[\u2260] (1 : \u2102), riemannZeta w \u2260 0 := by\n have h1 : (1 : \u2102) \u2208 {s : \u2102 | 1 \u2264 s.re} := by simp\n filter_upwards [eventually_mem_nhdsWithin] with w hw\n have hwre : 1 \u2264 w.re := by\n have := hw.2\n sorry\n exact riemannZeta_ne_zero_of_one_le_re hwre\n filter_upwards [hzero, eventually_mem_nhdsWithin] with w hw0 hw1\n exact hLi_eq_of_ne hw1 hw0\n\n/-! ## 3. The Laurent coefficients of \u2212\u03b6\u2032/\u03b6 at 1 (operational definition) -/\n\n/-- The k-th Laurent coefficient of \u2212\u03b6\u2032/\u03b6 at s = 1:\n\u2212\u03b6\u2032/\u03b6(1+u) = u\u207b\u00b9 + \u03a3_{k\u22650} lcoeff k \u00b7 u^k (identification proved in\ntier ii\u2032-2/3; here lcoeff is DEFINED via the analytic hLi). -/\ndef lcoeff (k : \u2115) : \u2102 := iteratedDeriv (k + 1) hLi 1 / (k + 1) !\n\nlemma lcoeff_eq (k : \u2115) :\n lcoeff k = iteratedDeriv (k + 1) hLi 1 / (k + 1) ! := rfl\n\n/-- hLi's Taylor coefficient form: iteratedDeriv j hLi 1 / j ! = lcoeff (j\u22121). -/\nlemma hLi_iteratedDeriv_div_factorial {j : \u2115} (hj : 1 \u2264 j) :\n iteratedDeriv j hLi 1 / j ! = lcoeff (j - 1) := by\n rw [lcoeff]\n have : j = (j - 1) + 1 := by omega\n rw [this]\n\n/-! ## 4. The A-polynomial derivative: A(w) = w\u207f \u2212 (w\u22121)\u207f -/\n\n/-- Iterated derivatives of A(w) = w\u207f \u2212 (w\u22121)\u207f at 1:\nA^{(i)}(1) = n.descFactorial i for i < n, and A^{(n)}(1) = 0. -/\nlemma A_iter (n i : \u2115) (hi : i \u2264 n) :\n iteratedDeriv i (fun w => w ^ n - (w - 1) ^ n) (1 : \u2102) =\n if i < n then n.descFactorial i else 0 := by\n have hf : ContDiffAt \u2102 i (fun w : \u2102 => w ^ n) 1 :=\n (contDiff_id.pow n).contDiffAt\n have hg : ContDiffAt \u2102 i (fun w : \u2102 => (w - 1) ^ n) 1 :=\n ((contDiff_id.sub contDiff_const).pow n).contDiffAt\n rw [iteratedDeriv_sub hf hg]\n have h1 : iteratedDeriv i (fun w : \u2102 => w ^ n) 1 = n.descFactorial i := by\n rw [iteratedDeriv_pow]\n simp\n have h2 : iteratedDeriv i (fun w : \u2102 => (w - 1) ^ n) 1 =\n n.descFactorial i * (0 : \u2102) ^ (n - i) := by\n have e := iteratedDeriv_comp_sub_const i (fun w : \u2102 => w ^ n) (1 : \u2102)\n have e2 : iteratedDeriv i (fun w : \u2102 => (w - 1) ^ n) 1 =\n iteratedDeriv i (fun w : \u2102 => w ^ n) (1 - 1) := by\n have := congr_fun e 1\n convert this using 2\n rw [e2, iteratedDeriv_pow]\n simp\n rw [h1, h2]\n by_cases hin : i < n\n \u00b7 rw [if_pos hin]\n have : (0 : \u2102) ^ (n - i) = 0 := by\n apply zero_pow\n omega\n rw [this, mul_zero, sub_zero]\n \u00b7 rw [if_neg hin]\n have hin' : i = n := le_antisymm hi (by omega)\n subst hin'\n simp [Nat.descFactorial_self]\n\n/-! ## 5. The residue at w = 1: ResW1 n = \u03a3_{j=1}^n C(n,j)\u00b7lcoeff (j\u22121) -/\n\n/-- The residue at w = 1 of the Lagarias-kernel integrand\nJ(w) = k_n(w\u22121)\u00b7(\u2212\u03b6\u2032/\u03b6(w)), packaged as (1/n!)\u00b7(d/dw)\u207f[(w\u207f\u2212(w\u22121)\u207f)hLi]\nat w = 1 (D-064 \u00a74 R1: (w\u22121)^{n+1}J = [w\u207f\u2212(w\u22121)\u207f]\u00b7hLi on a punctured\nneighborhood, by `hLi_eq_near_one`). -/\ndef ResW1 (n : \u2115) : \u2102 :=\n iteratedDeriv n (fun w => (w ^ n - (w - 1) ^ n) * hLi w) (1 : \u2102) / n !\n\n/-- The w = 1 residue value: ResW1 n = \u03a3_{j=1}^n C(n,j)\u00b7lcoeff (j\u22121). -/\ntheorem ResW1_eq_sum (n : \u2115) :\n ResW1 n = \u2211 j \u2208 Finset.Icc 1 n, (n.choose j : \u2102) * lcoeff (j - 1) := by\n have hA : ContDiffAt \u2102 n (fun w : \u2102 => w ^ n - (w - 1) ^ n) 1 :=\n ((contDiff_id.pow n).sub ((contDiff_id.sub contDiff_const).pow n)).contDiffAt\n have hh : ContDiffAt \u2102 n hLi 1 := hLi_analyticAt_one.contDiffAt\n have hmul := iteratedDeriv_mul hA hh\n rw [ResW1, hmul]\n have hsum : \u2211 i \u2208 Finset.range (n + 1),\n n.choose i * iteratedDeriv i (fun w : \u2102 => w ^ n - (w - 1) ^ n) 1 *\n iteratedDeriv (n - i) hLi 1 =\n \u2211 i \u2208 Finset.range n,\n n.choose i * (n.descFactorial i : \u2102) * iteratedDeriv (n - i) hLi 1 := by\n apply Finset.sum_subset (Finset.range_le_iff.mpr (Nat.le_succ n))\n intro i hi\n rw [Finset.mem_range] at hi\n have hi0 : i \u2260 n := by omega\n rw [A_iter n i (by omega), if_pos (by omega)]\n \u00b7 rfl\n \u00b7 rw [Finset.mem_range] at *\n omega\n rw [hsum]\n have hfinal : (\u2211 i \u2208 Finset.range n,\n n.choose i * (n.descFactorial i : \u2102) * iteratedDeriv (n - i) hLi 1) / n ! =\n \u2211 j \u2208 Finset.Icc 1 n, (n.choose j : \u2102) * lcoeff (j - 1) := by\n have hrewrite : \u2200 i \u2208 Finset.range n,\n n.choose i * (n.descFactorial i : \u2102) * iteratedDeriv (n - i) hLi 1 / n ! =\n (n.choose (n - i) : \u2102) * lcoeff (n - i - 1) := by\n intro i hi\n rw [Finset.mem_range] at hi\n have hcd : (n.choose i : \u2102) * (n.descFactorial i : \u2102) =\n n ! * n.choose i / (n - i) ! := by\n have h1 := Nat.choose_mul_factorial_mul_factorial (show i \u2264 n by omega)\n have h2 := Nat.factorial_mul_descFactorial (show i \u2264 n by omega)\n have : (n.choose i : \u2102) * (n.descFactorial i : \u2102) * ((i ! : \u2102) * ((n - i) ! : \u2102)) =\n (n ! : \u2102) * (n.choose i : \u2102) := by\n push_cast [h1, h2]\n ring\n have hfact : ((i ! : \u2102) * ((n - i) ! : \u2102)) \u2260 0 := by\n simp [Nat.factorial_ne_zero]\n have hthis := this\n field_simp at hthis \u22a2\n have h3 : (n.choose i : \u2102) * (n.descFactorial i : \u2102) * ((n - i) ! : \u2102) =\n (n ! : \u2102) * (n.choose i : \u2102) / 1 := by\n have h4 := hthis\n rw [mul_comm ((i ! : \u2102)) ((n - i) ! : \u2102)] at h4\n have h5 : (n.choose i : \u2102) * (n.descFactorial i : \u2102) * ((n - i) ! : \u2102) * (i ! : \u2102) =\n (n ! : \u2102) * (n.choose i : \u2102) := by\n rw [mul_comm ((n - i) ! : \u2102) (i ! : \u2102)] at h4\n calc (n.choose i : \u2102) * (n.descFactorial i : \u2102) * ((n - i) ! : \u2102) * (i ! : \u2102)\n = (n.choose i : \u2102) * (n.descFactorial i : \u2102) * (((n - i) ! : \u2102) * (i ! : \u2102)) := by ring\n _ = (n ! : \u2102) * (n.choose i : \u2102) := by\n have := h4\n ring_nf at this \u22a2\n convert this using 1\n ring\n exact (div_eq_one_iff_eq (by simp [Nat.factorial_ne_zero])).mpr h5\n field_simp at h3 \u22a2\n calc (n.choose i : \u2102) * (n.descFactorial i : \u2102)\n = ((n ! : \u2102) * (n.choose i : \u2102) / 1) / ((n - i) ! : \u2102) := by\n rw [\u2190 h3]\n field_simp\n ring\n _ = (n ! : \u2102) * (n.choose i : \u2102) / ((n - i) ! : \u2102) := by ring\n rw [hcd]\n have hni : n - i \u2265 1 := by omega\n rw [hLi_iteratedDeriv_div_factorial (j := n - i) (by omega)]\n rw [show n - i - 1 = n - i - 1 from rfl]\n have hcoe : ((n - i) ! : \u2102) \u2260 0 := by simp [Nat.factorial_ne_zero]\n field_simp\n rw [Nat.choose_symm (by omega : i \u2264 n)]\n ring\n rw [Finset.sum_div]\n rw [Finset.sum_congr rfl hrewrite]\n have hmap : \u2211 i \u2208 Finset.range n, (n.choose (n - i) : \u2102) * lcoeff (n - i - 1) =\n \u2211 j \u2208 Finset.Icc 1 n, (n.choose j : \u2102) * lcoeff (j - 1) := by\n rw [Finset.sum_range_reflect]\n apply Finset.sum_congr rfl\n intro i hi\n rw [Finset.mem_range] at hi\n have : n - 1 - i + 1 = n - i := by omega\n rw [this]\n have : n - (n - i) = i := by omega\n rw [Nat.choose_symm (show n - i \u2264 n by omega)]\n simp [this]\n ring\n exact hmap\n rw [hfinal]\n\nend NguyenRH1\n",
"autoRead": false
}
raw content_json (database row)
[{"type":"thinking","thinking":"I wrote a first draft but I left a `sorry` in `hLi_eq_near_one` and some proofs are likely broken (hcd's algebra got convoluted, hsum's structure is off, hmap's reindexing is shaky). Let me compile and fix iteratively. Also I should fix hLi_eq_near_one's sorry: the zero-free punctured neighborhood of 1 — ζ(w) ≠ 0 for w near 1 with... the simple argument: ζ has a pole at 1, so |ζ| → ∞, hence ζ ≠ 0 in a punctured nhd: from riemannZeta_residue_one: (s−1)ζ(s) → 1, so (s−1)ζ(s) ≠ 0 in a punctured nhd, hence ζ(s) ≠ 0 there. That's cleaner than the re ≥ 1 approach:\n\n```\nlemma hLi_eq_near_one :\n ∀ᶠ w in 𝓝[≠] (1 : ℂ), hLi w = (w - 1) * (-(deriv riemannZeta w) / riemannZeta w) := by\n have hT := riemannZeta_residue_one\n have hne : ∀ᶠ w in 𝓝[≠] (1 : ℂ), (w - 1) * riemannZeta w ≠ 0 := by\n have := hT.eventually_ne (show (1 : ℂ) ≠ 0 by norm_num)\n exact this\n filter_upwards [hne, eventually_mem_nhdsWithin] with w hw hw1\n have hz : riemannZeta w ≠ 0 := by\n have h2 := hw\n simp only [ne_eq, mul_eq_zero] at h2\n push_neg at h2\n exact h2.2\n exact hLi_eq_of_ne hw1 hz\n```\n`Tendsto.eventually_ne : Tendsto f l (𝓝 a) → a ≠ b → ∀ᶠ x in l, f x ≠ b` ✓ exists.\n\nAlso fix hcd — the coefficient algebra got tangled. Let me simplify: the identity needed:\n(n.choose i : ℂ) * (n.descFactorial i : ℂ) / n ! = (n.choose i : ℂ) / ((n - i) ! : ℂ)·... wait — actually what I need: C(n,i)·descFac(i)/n!·h^{(n−i)} = C(n,i)·lcoeff(n−i−1) with lcoeff(n−i−1) = h^{(n−i)}/(n−i)!. So need C(n,i)·descFac(n,i)/n! = C(n,i)/(n−i)! ⟺ descFac(n,i)/n! = 1/(n−i)! ⟺ descFac(n,i)·... ⟺ n!/(n−i)! — i.e. descFac(n,i) = n!/(n−i)! — via factorial_mul_descFactorial: (n−i)!·descFac(n,i) = n! ⟹ descFac(n,i) = n!/(n−i)! ✓ (division in ℂ of the cast equality ✓ clean).\n\nSo the clean version:\n```\nhave hdesc : (n.descFactorial i : ℂ) = (n ! : ℂ) / ((n - i) ! : ℂ) := by\n have h2 := Nat.factorial_mul_descFactorial (show i ≤ n by omega)\n have hcast : ((n - i) ! : ℂ) * (n.descFactorial i : ℂ) = (n ! : ℂ) := by exact_mod_cast h2\n rw [eq_div_iff_mul_eq (by simp [Nat.factorial_ne_zero])]\n rw [mul_comm]\n exact hcast\n```\n`eq_div_iff_mul_eq : a = b / c ↔ a * c = b` (c ≠ 0) — check name: `eq_div_iff_mul_eq (hc : c ≠ 0) : a = b / c ↔ a * c = b` ✓.\n\nThen term rewriting:\nC(n,i)·descFac(n,i)·h^{(n−i)}/n! = C(n,i)·(n!/(n−i)!)·h^{(n−i)}/n! = C(n,i)·h^{(n−i)}/(n−i)! = C(n,i)·lcoeff(n−i−1).\nAnd C(n,i) = C(n,n−i) (Nat.choose_symm hi).\n\nThe sum reindexing: ∑_{i ∈ range n} f(n−i) where f(k) = C(n,k)·lcoeff(k−1)... i ↦ n−i maps range n = {0,...,n−1} to {1,...,n} = Icc 1 n: `Finset.sum_range_reflect`? — sum_range_reflect : ∑ i ∈ range n, f i = ∑ i ∈ range n, f (n − 1 − i). Hmm that maps to n−1−i ∈ {0,...,n−1}. My target is Icc 1 n. Alternative: sum over range (n+1) with the zero terms? Or use `Finset.sum_bij`. Simplest: convert the target sum to range form: ∑ j ∈ Icc 1 n, g j = ∑ i ∈ range n, g (i + 1): `Finset.sum_Icc_eq_sum_range`? there's `Finset.sum_Icc_eq_sum_range : ∑ i ∈ Icc m n, f i = ∑ i ∈ range (n + 1 - m), f (i + m)` ✓ I believe. So ∑ j ∈ Icc 1 n, g j = ∑ i ∈ range n, g (i+1). Then:\n∑ i ∈ range n, C(n,i)·descFac·h^{(n−i)}/n! = ∑ i ∈ range n, C(n,i)·lcoeff(n−i−1)·... vs ∑ i ∈ range n, g(i+1) = ∑ i ∈ range n, C(n,i+1)·lcoeff(i). Via sum_range_reflect: ∑ i ∈ range n, a(i) = ∑ i ∈ range n, a(n−1−i): with a(i) = C(n,i)·lcoeff(n−i−1): a(n−1−i) = C(n,n−1−i)·lcoeff(n−(n−1−i)−1) = C(n,i+1)·lcoeff(i)·... C(n,n−1−i) = C(n,i+1) (choose_symm: n−(n−1−i) = i+1 ✓). ✓ \n\nLet me restructure hfinal cleanly:\n```\nhave hterm : ∀ i ∈ Finset.range n,\n (n.choose i : ℂ) * (n.descFactorial i : ℂ) * iteratedDeriv (n - i) hLi 1 / n ! =\n (n.choose i : ℂ) * lcoeff (n - i - 1) := by\n intro i hi\n rw [Finset.mem_range] at hi\n have hdesc : (n.descFactorial i : ℂ) = (n ! : ℂ) / ((n - i) ! : ℂ) := by\n have h2 := Nat.factorial_mul_descFactorial (show i ≤ n by omega)\n have hcast : ((n - i) ! : ℂ) * (n.descFactorial i : ℂ) = (n ! : ℂ) := by exact_mod_cast h2\n rw [eq_div_iff_mul_eq (by simp [Nat.factorial_ne_zero])]\n rw [mul_comm]\n exact hcast\n rw [hdesc]\n have hni : 1 ≤ n - i := by omega\n have hlc : lcoeff (n - i - 1) = iteratedDeriv (n - i) hLi 1 / ((n - i) ! : ℂ) := by\n rw [hLi_iteratedDeriv_div_factorial (j := n - i) hni]\n rw [hlc]\n field_simp\n ring\n```\nfield_simp + ring for: C·(n!/(n−i)!)·h/n! = C·(h/(n−i)!) — with h = iteratedDeriv — field_simp [n! ≠ 0, (n−i)! ≠ 0] then ring ✓.\n\nThen:\n```\nrw [Finset.sum_div]\nrw [Finset.sum_congr rfl hterm]\n-- now: ∑ i ∈ range n, C(n,i)·lcoeff(n−i−1) = ∑ j ∈ Icc 1 n, C(n,j)·lcoeff(j−1)\nhave hre : ∑ i ∈ Finset.range n, (n.choose i : ℂ) * lcoeff (n - i - 1) =\n ∑ j ∈ Finset.Icc 1 n, (n.choose j : ℂ) * lcoeff (j - 1) := by\n rw [Finset.sum_range_reflect]\n -- now ∑ i ∈ range n, C(n, n−1−i)·lcoeff(n−(n−1−i)−1) = C(n,n−1−i)·lcoeff(i)\n rw [Finset.sum_Icc_eq_sum_range]\n apply Finset.sum_congr rfl\n intro i hi\n rw [Finset.mem_range] at hi\n have e1 : n - 1 - i + 1 = n - i := by omega\n -- target after rewrites: C(n, n−1−i)·lcoeff(n−1−i−...)... let me compute in code\n ...\n```\nHmm the reindexing needs care. Finset.sum_range_reflect : ∑ i ∈ range n, f i = ∑ i ∈ range n, f (n - 1 - i). So ∑_{i<n} a(i) = ∑_{i<n} a(n−1−i): with a(k) = C(n,k)·lcoeff(n−k−1): a(n−1−i) = C(n,n−1−i)·lcoeff(n−(n−1−i)−1) = C(n,n−1−i)·lcoeff(i). C(n,n−1−i) = C(n,n−(n−1−i)) = C(n,i+1) — Nat.choose_symm : n.choose (n − k) = n.choose k for k ≤ n: n.choose (n−1−i) = n.choose (n − (n−1−i)) = n.choose (i+1)? — choose_symm (h : k ≤ n) : n.choose (n - k) = n.choose k — so n.choose (n−1−i) = n.choose (i+1) iff (n−1−i) = n − (i+1) ✓ and k := i+1 ≤ n ✓. So a(n−1−i) = C(n,i+1)·lcoeff(i). And the target (after sum_Icc_eq_sum_range): ∑_{i<n} C(n,i+1)·lcoeff((i+1)−1) = ∑_{i<n} C(n,i+1)·lcoeff(i) ✓ MATCHES.\n\nOK — let me rewrite the file with all fixes. Also fix `hsum`'s broken structure (I had a malformed Finset.sum_subset application). The sum over range (n+1) → range n: the i = n term vanishes because A^{(n)}(1) = 0:\n```\nhave hsum : (∑ i ∈ Finset.range (n + 1),\n n.choose i * iteratedDeriv i (fun w : ℂ => w ^ n - (w - 1) ^ n) 1 *\n iteratedDeriv (n - i) hLi 1) =\n ∑ i ∈ Finset.range n,\n n.choose i * (n.descFactorial i : ℂ) * iteratedDeriv (n - i) hLi 1 := by\n rw [Finset.sum_range_succ]\n simp [A_iter n n le_rfl]\n apply Finset.sum_congr rfl\n intro i hi\n rw [Finset.mem_range] at hi\n rw [A_iter n i (by omega), if_pos hi]\n```\nFinset.sum_range_succ : ∑ i ∈ range (n+1), f i = ∑ i ∈ range n, f i + f n ✓. f n = C(n,n)·0·... = 0: A_iter n n (le_refl) : iteratedDeriv n A 1 = if n < n then ... else 0 = 0: if_neg (lt_irrefl n): simp [A_iter n n le_rfl] should simplify f n to 0 (A_iter gives if n < n then _ else 0 = 0 ✓).\n\nAlso `iteratedDeriv_sub` needs ContDiffAt — provided hA separately: in A_iter I used hf/hg locally ✓.\n\nThe `iteratedDeriv_mul` result: Σ i ∈ range (n+1), n.choose i * iteratedDeriv i A 1 * iteratedDeriv (n−i) hLi 1 — from the signature: `iteratedDeriv n (f * g) x = ∑ i ∈ .range (n + 1), n.choose i * iteratedDeriv i f x * iteratedDeriv (n - i) g x` — note: n.choose i is ℕ — cast to ℂ? The lemma as displayed: `n.choose i * iteratedDeriv i f x * iteratedDeriv (n - i) g x` — for 𝕜 → 𝔸 with 𝔸 an algebra over 𝕜 — the choose is a natural scalar mult — for ℂ→ℂ it should elaborate as (n.choose i : ℂ) cast or nsmul. Fine.\n\nLet me now rewrite the whole file cleanly.","signature":""},{"type":"text","text":"The draft needs repair — rewriting with the cleaned-up coefficient algebra, the proper zero-free argument, and fixed reindexing."},{"type":"tool_use","id":"Write_196","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiResidue.lean","content":"/-\nNguyenRH1/LiResidue.lean — tier ii′ sub-stage ii′-1b (D-064 §4 R1):\nthe w = 1 residue of the Lagarias-kernel integrand, computed exactly.\n\nContents (Part 1):\n* `zetaA w = (w−1)·ζ(w)` extended by 1 at w = 1 — analytic at 1 with\n value 1 (removable singularity; Mathlib `riemannZeta_residue_one` +\n `differentiableOn_update_limUnder_of_bddAbove`).\n* `hLi w = 1 − (w−1)·(zetaA′/zetaA)(w)` — analytic at 1, hLi 1 = 1;\n agrees with (w−1)·(−ζ′/ζ)(w) on a punctured neighborhood of 1\n (`hLi_eq_near_one`).\n* `lcoeff k` — the Laurent coefficients of −ζ′/ζ at 1, DEFINED as\n iteratedDeriv (k+1) hLi 1 / (k+1)!.\n* `ResW1 n` — the residue at w = 1 of J(w) = k_n(w−1)·(−ζ′/ζ(w)),\n packaged as (1/n!)·(d/dw)ⁿ[(wⁿ−(w−1)ⁿ)·hLi] at w = 1 (D-064 §4 R1:\n (w−1)^{n+1}J = [wⁿ−(w−1)ⁿ]·hLi on a punctured neighborhood, by\n `hLi_eq_near_one`). Value: `ResW1_eq_sum`.\n\nArchive references: D-036, D-037, D-064 (R1), journal-014/015.\n-/\nimport Mathlib\nimport Zeta23.Statement\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. The regularized factor zetaA = (w−1)ζ(w) at w = 1 -/\n\n/-- `zetaA w = (w−1)·ζ(w)` with the removable singularity at w = 1 filled\nby the residue value 1. Analytic at 1 (`zetaA_analyticAt_one`), value\n`zetaA 1 = 1`. -/\ndef zetaA : ℂ → ℂ := Function.update (fun w => (w - 1) * riemannZeta w) 1 1\n\nlemma zetaA_apply {w : ℂ} (hw : w ≠ 1) : zetaA w = (w - 1) * riemannZeta w :=\n Function.update_of_ne hw _ _\n\nlemma zetaA_one : zetaA 1 = 1 := Function.update_self _ _ _\n\n/-- The regularized factor is analytic at w = 1 (removable singularity). -/\nlemma zetaA_analyticAt_one : AnalyticAt ℂ zetaA 1 := by\n have hdiff : DifferentiableOn ℂ (fun w => (w - 1) * riemannZeta w)\n (Metric.ball 1 2 \\ {1}) := by\n intro w hw\n have hw1 : w ≠ 1 := hw.2\n exact ((differentiableAt_id.sub (differentiableAt_const 1)).mul\n (differentiableAt_riemannZeta hw1)).differentiableWithinAt\n have hbd : BddAbove (Complex.norm ∘ (fun w => (w - 1) * riemannZeta w)) ''\n (Metric.ball 1 2 \\ {1}) := by\n have hT := riemannZeta_residue_one\n rw [Metric.tendsto_nhdsWithin_nhds] at hT\n obtain ⟨δ, hδ0, hδ⟩ := hT 1 one_pos\n refine ⟨2, ?_⟩\n rintro _ ⟨z, hz, rfl⟩\n have hz1 : z ≠ 1 := hz.2\n have hlt := hδ (by\n rw [dist_eq_norm, sub_zero]\n exact hz.1)\n have h1 : ‖(z - 1) * riemannZeta z - 1‖ < 1 := by\n have := hlt\n rwa [dist_eq_norm] at this\n have := norm_sub_le ((z - 1) * riemannZeta z) 1\n simp only [Complex.norm_eq_abs] at *\n have h2 : ‖(z - 1) * riemannZeta z‖ ≤ ‖(z - 1) * riemannZeta z - 1‖ + ‖(1 : ℂ)‖ :=\n norm_sub_le ((z - 1) * riemannZeta z) 1\n rw [norm_one] at h2\n linarith [h1]\n have h := differentiableOn_update_limUnder_of_bddAbove\n (Metric.ball_mem_nhds 1 (by norm_num : (0 : ℝ) < 2)) hdiff hbd\n have hlim : limUnder (𝓝[≠] (1 : ℂ)) (fun w => (w - 1) * riemannZeta w) = 1 :=\n riemannZeta_residue_one.limUnder_eq\n rw [hlim] at h\n have han := h.analyticOnNhd Metric.isOpen_ball\n exact han.analyticAt (Metric.ball_mem_nhds 1 (by norm_num : (0 : ℝ) < 2))\n\n/-- zetaA is nonzero on a neighborhood of 1 (value 1 there). -/\nlemma zetaA_ne_zero_near_one : ∀ᶠ w in 𝓝 (1 : ℂ), zetaA w ≠ 0 :=\n (zetaA_analyticAt_one.continuousAt).eventually_ne (by rw [zetaA_one]; norm_num)\n\n/-- zetaA is analytic at any w ≠ 1 (agrees with (w−1)ζ there). -/\nlemma zetaA_analyticAt_of_ne {w : ℂ} (hw : w ≠ 1) : AnalyticAt ℂ zetaA w := by\n have h : (fun w => (w - 1) * riemannZeta w) =ᶠ[𝓝 w] zetaA := by\n filter_upwards [eventually_ne_nhds hw] with z hz using (zetaA_apply hz).symm\n have ha : AnalyticAt ℂ (fun w => (w - 1) * riemannZeta w) w :=\n (analyticAt_id.sub analyticAt_const).mul\n (differentiableAt_riemannZeta hw).analyticAt\n exact ha.congr h\n\n/-! ## 2. hLi w = 1 − (w−1)·(zetaA′/zetaA)(w): analytic at 1, value 1 -/\n\n/-- hLi(w) = 1 − (w−1)·(zetaA′/zetaA)(w) — the analytic-at-1 form of\n(w−1)(−ζ′/ζ)(w) (`hLi_eq_near_one`). hLi 1 = 1. -/\ndef hLi (w : ℂ) : ℂ := 1 - (w - 1) * (deriv zetaA w / zetaA w)\n\nlemma hLi_one : hLi 1 = 1 := by simp [hLi]\n\nlemma hLi_analyticAt_one : AnalyticAt ℂ hLi 1 := by\n have ha := zetaA_analyticAt_one\n have hda : AnalyticAt ℂ (deriv zetaA) 1 := ha.deriv\n have hne : zetaA 1 ≠ 0 := by rw [zetaA_one]; norm_num\n exact ((analyticAt_const.sub analyticAt_id).mul\n (hda.div ha hne)).const_sub 1\n\n/-- On the punctured plane minus zeros of ζ, hLi = (w−1)·(−ζ′/ζ). -/\nlemma hLi_eq_of_ne {w : ℂ} (hw1 : w ≠ 1) (hw0 : riemannZeta w ≠ 0) :\n hLi w = (w - 1) * (-(deriv riemannZeta w) / riemannZeta w) := by\n have hA : zetaA w = (w - 1) * riemannZeta w := zetaA_apply hw1\n have hdA : deriv zetaA w = riemannZeta w + (w - 1) * deriv riemannZeta w := by\n have h1 : deriv (fun z => (z - 1) * riemannZeta z) w =\n deriv (fun z => z - 1) w * riemannZeta w +\n (w - 1) * deriv riemannZeta w :=\n deriv_mul ((differentiableAt_id.sub (differentiableAt_const 1)))\n (differentiableAt_riemannZeta hw1)\n have h2 : deriv (fun z => z - 1) w = 1 := by\n simp [deriv_sub, deriv_id'']\n have h3 : (fun z => (z - 1) * riemannZeta z) =ᶠ[𝓝 w] zetaA := by\n filter_upwards [eventually_ne_nhds hw1] with z hz using (zetaA_apply hz).symm\n rw [h3.deriv_eq, h1, h2, one_mul]\n rw [hLi, hdA, hA]\n have hw1' : w - 1 ≠ 0 := sub_ne_zero.mpr hw1\n field_simp [hw0, hw1']\n ring\n\n/-- On a punctured neighborhood of 1, hLi = (w−1)·(−ζ′/ζ). -/\nlemma hLi_eq_near_one :\n ∀ᶠ w in 𝓝[≠] (1 : ℂ), hLi w = (w - 1) * (-(deriv riemannZeta w) / riemannZeta w) := by\n have hne : ∀ᶠ w in 𝓝[≠] (1 : ℂ), (w - 1) * riemannZeta w ≠ 0 :=\n riemannZeta_residue_one.eventually_ne (show (1 : ℂ) ≠ 0 by norm_num)\n filter_upwards [hne, eventually_mem_nhdsWithin] with w hw hw1\n have hz : riemannZeta w ≠ 0 := by\n have h2 := hw\n simp only [ne_eq, mul_eq_zero] at h2\n push_neg at h2\n exact h2.2\n exact hLi_eq_of_ne hw1 hz\n\n/-! ## 3. The Laurent coefficients of −ζ′/ζ at 1 (operational definition) -/\n\n/-- The k-th Laurent coefficient of −ζ′/ζ at s = 1, DEFINED as\niteratedDeriv (k+1) hLi 1 / (k+1)! (the power-series coefficient of the\nanalytic hLi; the identification with −ζ′/ζ's Laurent expansion is\n`hLi_eq_near_one`). -/\ndef lcoeff (k : ℕ) : ℂ := iteratedDeriv (k + 1) hLi 1 / (k + 1) !\n\n/-- hLi's Taylor coefficients: iteratedDeriv j hLi 1 / j ! = lcoeff (j−1). -/\nlemma hLi_iteratedDeriv_div_factorial {j : ℕ} (hj : 1 ≤ j) :\n iteratedDeriv j hLi 1 / j ! = lcoeff (j - 1) := by\n rw [lcoeff]\n have : j = (j - 1) + 1 := by omega\n rw [this]\n\n/-! ## 4. The A-polynomial derivative: A(w) = wⁿ − (w−1)ⁿ -/\n\n/-- Iterated derivatives of A(w) = wⁿ − (w−1)ⁿ at 1:\nA^{(i)}(1) = n.descFactorial i for i < n, and A^{(n)}(1) = 0. -/\nlemma A_iter (n i : ℕ) (hi : i ≤ n) :\n iteratedDeriv i (fun w => w ^ n - (w - 1) ^ n) (1 : ℂ) =\n if i < n then n.descFactorial i else 0 := by\n have hf : ContDiffAt ℂ i (fun w : ℂ => w ^ n) 1 :=\n (contDiff_id.pow n).contDiffAt\n have hg : ContDiffAt ℂ i (fun w : ℂ => (w - 1) ^ n) 1 :=\n ((contDiff_id.sub contDiff_const).pow n).contDiffAt\n rw [iteratedDeriv_sub hf hg]\n have h1 : iteratedDeriv i (fun w : ℂ => w ^ n) 1 = n.descFactorial i := by\n rw [iteratedDeriv_pow]\n simp\n have h2 : iteratedDeriv i (fun w : ℂ => (w - 1) ^ n) 1 =\n n.descFactorial i * (0 : ℂ) ^ (n - i) := by\n have e := congr_fun (iteratedDeriv_comp_sub_const i (fun w : ℂ => w ^ n) (1 : ℂ)) 1\n rw [iteratedDeriv_pow] at e\n simpa using e\n rw [h1, h2]\n by_cases hin : i < n\n · rw [if_pos hin]\n have hz : (0 : ℂ) ^ (n - i) = 0 := zero_pow (by omega)\n rw [hz, mul_zero, sub_zero]\n · rw [if_neg hin]\n have hin' : i = n := le_antisymm hi (by omega)\n subst hin'\n simp [Nat.descFactorial_self]\n\n/-! ## 5. The residue at w = 1: ResW1 n = Σ_{j=1}^n C(n,j)·lcoeff (j−1) -/\n\n/-- The residue at w = 1 of the Lagarias-kernel integrand\nJ(w) = k_n(w−1)·(−ζ′/ζ(w)), packaged as (1/n!)·(d/dw)ⁿ[(wⁿ−(w−1)ⁿ)hLi]\nat w = 1 (D-064 §4 R1: (w−1)^{n+1}J = [wⁿ−(w−1)ⁿ]·hLi punctured near 1,\nby `hLi_eq_near_one`). -/\ndef ResW1 (n : ℕ) : ℂ :=\n iteratedDeriv n (fun w => (w ^ n - (w - 1) ^ n) * hLi w) (1 : ℂ) / n !\n\n/-- The w = 1 residue value: ResW1 n = Σ_{j=1}^n C(n,j)·lcoeff (j−1). -/\ntheorem ResW1_eq_sum (n : ℕ) :\n ResW1 n = ∑ j ∈ Finset.Icc 1 n, (n.choose j : ℂ) * lcoeff (j - 1) := by\n have hA : ContDiffAt ℂ n (fun w : ℂ => w ^ n - (w - 1) ^ n) 1 :=\n ((contDiff_id.pow n).sub ((contDiff_id.sub contDiff_const).pow n)).contDiffAt\n have hh : ContDiffAt ℂ n hLi 1 := hLi_analyticAt_one.contDiffAt\n have hmul := iteratedDeriv_mul hA hh\n rw [ResW1, hmul]\n have hsum : (∑ i ∈ Finset.range (n + 1),\n n.choose i * iteratedDeriv i (fun w : ℂ => w ^ n - (w - 1) ^ n) 1 *\n iteratedDeriv (n - i) hLi 1) =\n ∑ i ∈ Finset.range n,\n n.choose i * (n.descFactorial i : ℂ) * iteratedDeriv (n - i) hLi 1 := by\n rw [Finset.sum_range_succ]\n simp [A_iter n n le_rfl]\n apply Finset.sum_congr rfl\n intro i hi\n rw [Finset.mem_range] at hi\n rw [A_iter n i (by omega), if_pos hi]\n rw [hsum]\n have hterm : ∀ i ∈ Finset.range n,\n n.choose i * (n.descFactorial i : ℂ) * iteratedDeriv (n - i) hLi 1 / n ! =\n (n.choose i : ℂ) * lcoeff (n - i - 1) := by\n intro i hi\n rw [Finset.mem_range] at hi\n have hdesc : (n.descFactorial i : ℂ) = (n ! : ℂ) / ((n - i) ! : ℂ) := by\n have h2 := Nat.factorial_mul_descFactorial (show i ≤ n by omega)\n have hcast : ((n - i) ! : ℂ) * (n.descFactorial i : ℂ) = (n ! : ℂ) := by\n exact_mod_cast h2\n rw [eq_div_iff_mul_eq (by simp [Nat.factorial_ne_zero])]\n rw [mul_comm]\n exact hcast\n rw [hdesc]\n have hlc : lcoeff (n - i - 1) = iteratedDeriv (n - i) hLi 1 / ((n - i) ! : ℂ) := by\n rw [hLi_iteratedDeriv_div_factorial (j := n - i) (by omega)]\n rw [hlc]\n field_simp\n ring\n rw [Finset.sum_div]\n rw [Finset.sum_congr rfl hterm]\n have hre : (∑ i ∈ Finset.range n, (n.choose i : ℂ) * lcoeff (n - i - 1)) =\n ∑ j ∈ Finset.Icc 1 n, (n.choose j : ℂ) * lcoeff (j - 1) := by\n rw [Finset.sum_range_reflect]\n rw [Finset.sum_Icc_eq_sum_range]\n apply Finset.sum_congr rfl\n intro i hi\n rw [Finset.mem_range] at hi\n have e1 : n - 1 - i + 1 = n - i := by omega\n have e2 : n - (n - 1 - i) = i + 1 := by omega\n have e3 : n.choose (n - 1 - i) = n.choose (i + 1) := by\n rw [show n - 1 - i = n - (i + 1) by omega]\n exact Nat.choose_symm (by omega)\n have e4 : n - (n - 1 - i) - 1 = i := by omega\n rw [e1, e3]\n have : n - (i + 1) - 1 = i := by omega\n rw [this]\n exact hre\n\nend NguyenRH1\n"},"extra_content":null}]