← Session 21 — Tier ii′ planning + launch: close SfBoundProp in Lean (D-064)
thinking (404 chars)
`h.differentiableOn.analyticOnNhd isOpen_ball` — so the method is `DifferentiableOn.analyticOnNhd (hd : DifferentiableOn ℂ f s) (ho : IsOpen s) : AnalyticOnNhd ℂ f s` ✓ exists (dot notation).
Now I have everything. Let me write LiResidue.lean Part 1 (zetaA, hLi, lcoeff, ResW1 + ResW1_eq_sum). I'll write it in the new file and iterate with `lake env lean NguyenRH1/LiResidue.lean` from the package dir.
All confirmed. Writing `LiResidue.lean` Part 1 (zetaA, hLi, lcoeff, ResW1, and the value theorem).
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, 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"
}
result 2026-08-21 21:00:46Z → 2026-08-21 21:00:46Z
{
"type": "create",
"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, 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",
"structuredPatch": [],
"originalFile": null
}
raw content_json (database row)
[{"type":"thinking","thinking":"`h.differentiableOn.analyticOnNhd isOpen_ball` — so the method is `DifferentiableOn.analyticOnNhd (hd : DifferentiableOn ℂ f s) (ho : IsOpen s) : AnalyticOnNhd ℂ f s` ✓ exists (dot notation).\n\nNow I have everything. Let me write LiResidue.lean Part 1 (zetaA, hLi, lcoeff, ResW1 + ResW1_eq_sum). I'll write it in the new file and iterate with `lake env lean NguyenRH1/LiResidue.lean` from the package dir.","signature":""},{"type":"text","text":"All confirmed. Writing `LiResidue.lean` Part 1 (zetaA, hLi, lcoeff, ResW1, and the value theorem)."},{"type":"tool_use","id":"Write_195","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, this file's core):\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)! (operational; no Laurent series\n needed at this stage).\n* `ResW1 n` — the residue at w = 1 of J(w) = k_n(w−1)·(−ζ′/ζ(w)),\n computed by the Leibniz identity (w−1)^{n+1}J = [wⁿ−(w−1)ⁿ]·hLi\n (D-064 §4 R1, verified algebraically in session 014):\n ResW1 n = Σ_{j=1}^n C(n,j)·lcoeff (j−1) =: `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\nlemma zetaA_tendsto : Tendsto (fun w => (w - 1) * riemannZeta w) (𝓝[≠] 1) (𝓝 1) :=\n riemannZeta_residue_one\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 := zetaA_tendsto\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 h1 : dist (z - 1) 0 = ‖z - 1‖ := by\n rw [dist_eq_norm]; simp [sub_zero]\n have hz1 : z ≠ 1 := hz.2\n have hzz : dist z 1 < δ := by\n have := hz.1\n rw [Metric.mem_ball, dist_comm] at this\n exact this\n have hlt := hδ (by rwa [dist_zero_right, h1] at *)\n have : ‖(z - 1) * riemannZeta z‖ ≤ ‖(1 : ℂ)‖ + 1 := by\n have := norm_sub_le_of_le hlt\n calc ‖(z - 1) * riemannZeta z‖\n ≤ ‖(z - 1) * riemannZeta z - 1‖ + ‖(1 : ℂ)‖ := by\n have := norm_sub_le ((z - 1) * riemannZeta z) 1\n linarith [this, hlt]\n _ ≤ 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 : ℝ) < 2)) hdiff hbd\n have hlim : limUnder (𝓝[≠] (1 : ℂ)) (fun w => (w - 1) * riemannZeta w) = 1 :=\n zetaA_tendsto.limUnder_eq\n rw [hlim] at h\n have hopen : IsOpen (Metric.ball (1 : ℂ) 2) := Metric.isOpen_ball\n have han := h.analyticOnNhd hopen\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 everywhere except possibly at 1 — and in fact also\nat 1; we record the off-1 version for quotient computations. -/\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 := 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 − (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 a punctured neighborhood of 1, 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/-- The punctured-neighborhood form, for later contour work. -/\nlemma hLi_eq_near_one :\n ∀ᶠ w in 𝓝[≠] (1 : ℂ), hLi w = (w - 1) * (-(deriv riemannZeta w) / riemannZeta w) := by\n have hzero : ∀ᶠ w in 𝓝[≠] (1 : ℂ), riemannZeta w ≠ 0 := by\n have h1 : (1 : ℂ) ∈ {s : ℂ | 1 ≤ s.re} := by simp\n filter_upwards [eventually_mem_nhdsWithin] with w hw\n have hwre : 1 ≤ 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 −ζ′/ζ at 1 (operational definition) -/\n\n/-- The k-th Laurent coefficient of −ζ′/ζ at s = 1:\n−ζ′/ζ(1+u) = u⁻¹ + Σ_{k≥0} lcoeff k · u^k (identification proved in\ntier ii′-2/3; here lcoeff is DEFINED via the analytic hLi). -/\ndef lcoeff (k : ℕ) : ℂ := iteratedDeriv (k + 1) hLi 1 / (k + 1) !\n\nlemma lcoeff_eq (k : ℕ) :\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−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 := iteratedDeriv_comp_sub_const i (fun w : ℂ => w ^ n) (1 : ℂ)\n have e2 : iteratedDeriv i (fun w : ℂ => (w - 1) ^ n) 1 =\n iteratedDeriv i (fun w : ℂ => 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 · rw [if_pos hin]\n have : (0 : ℂ) ^ (n - i) = 0 := by\n apply zero_pow\n omega\n rw [this, 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 on a punctured\nneighborhood, by `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 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 ≠ n := by omega\n rw [A_iter n i (by omega), if_pos (by omega)]\n · rfl\n · rw [Finset.mem_range] at *\n omega\n rw [hsum]\n have hfinal : (∑ i ∈ Finset.range n,\n n.choose i * (n.descFactorial i : ℂ) * iteratedDeriv (n - i) hLi 1) / n ! =\n ∑ j ∈ Finset.Icc 1 n, (n.choose j : ℂ) * lcoeff (j - 1) := by\n have hrewrite : ∀ i ∈ Finset.range n,\n n.choose i * (n.descFactorial i : ℂ) * iteratedDeriv (n - i) hLi 1 / n ! =\n (n.choose (n - i) : ℂ) * lcoeff (n - i - 1) := by\n intro i hi\n rw [Finset.mem_range] at hi\n have hcd : (n.choose i : ℂ) * (n.descFactorial i : ℂ) =\n n ! * n.choose i / (n - i) ! := by\n have h1 := Nat.choose_mul_factorial_mul_factorial (show i ≤ n by omega)\n have h2 := Nat.factorial_mul_descFactorial (show i ≤ n by omega)\n have : (n.choose i : ℂ) * (n.descFactorial i : ℂ) * ((i ! : ℂ) * ((n - i) ! : ℂ)) =\n (n ! : ℂ) * (n.choose i : ℂ) := by\n push_cast [h1, h2]\n ring\n have hfact : ((i ! : ℂ) * ((n - i) ! : ℂ)) ≠ 0 := by\n simp [Nat.factorial_ne_zero]\n have hthis := this\n field_simp at hthis ⊢\n have h3 : (n.choose i : ℂ) * (n.descFactorial i : ℂ) * ((n - i) ! : ℂ) =\n (n ! : ℂ) * (n.choose i : ℂ) / 1 := by\n have h4 := hthis\n rw [mul_comm ((i ! : ℂ)) ((n - i) ! : ℂ)] at h4\n have h5 : (n.choose i : ℂ) * (n.descFactorial i : ℂ) * ((n - i) ! : ℂ) * (i ! : ℂ) =\n (n ! : ℂ) * (n.choose i : ℂ) := by\n rw [mul_comm ((n - i) ! : ℂ) (i ! : ℂ)] at h4\n calc (n.choose i : ℂ) * (n.descFactorial i : ℂ) * ((n - i) ! : ℂ) * (i ! : ℂ)\n = (n.choose i : ℂ) * (n.descFactorial i : ℂ) * (((n - i) ! : ℂ) * (i ! : ℂ)) := by ring\n _ = (n ! : ℂ) * (n.choose i : ℂ) := by\n have := h4\n ring_nf at this ⊢\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 ⊢\n calc (n.choose i : ℂ) * (n.descFactorial i : ℂ)\n = ((n ! : ℂ) * (n.choose i : ℂ) / 1) / ((n - i) ! : ℂ) := by\n rw [← h3]\n field_simp\n ring\n _ = (n ! : ℂ) * (n.choose i : ℂ) / ((n - i) ! : ℂ) := by ring\n rw [hcd]\n have hni : n - i ≥ 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) ! : ℂ) ≠ 0 := by simp [Nat.factorial_ne_zero]\n field_simp\n rw [Nat.choose_symm (by omega : i ≤ n)]\n ring\n rw [Finset.sum_div]\n rw [Finset.sum_congr rfl hrewrite]\n have hmap : ∑ i ∈ Finset.range n, (n.choose (n - 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 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 ≤ n by omega)]\n simp [this]\n ring\n exact hmap\n rw [hfinal]\n\nend NguyenRH1\n"},"extra_content":null}]