[{"type":"thinking","thinking":"All confirmed. Now write LiSeries.lean. Let me draft the full file carefully.\n\n```lean\n/-\nNguyenRH1/LiSeries.lean — tier ii′ sub-stage ii′-5e-iii (D-068 §3):\nthe zero-side partial-fraction series\n\n  seriesFun s := ∑' ρ : {ρ // IsNontrivialZero ρ}, (zeroMult ρ : ℂ)·(1/(s−ρ) + 1/ρ)\n\nand its three structural properties:\n(§1–2) ABSOLUTE SUMMABILITY at every s (`seriesSummable`): the tail bound\n  ‖1/(s−ρ) + 1/ρ‖ ≤ 2‖s‖/‖ρ‖² (‖ρ‖ ≥ 2‖s‖, ‖ρ‖ ≥ 2) feeds the ii′-1a\n  dominator chain (comparison 1 + ‖γ_ρ‖² ≤ (17/12)‖ρ‖² → Zeta23\n  `WeilEF.zero_sum_inv_sq`); the finite head is a finite subtype sum.\n(§3–4) ANALYTICITY off the zeros (`seriesFun_analyticOnNhd`): around any\n  s₀ that is not a nontrivial zero there is a ball avoiding the\n  nontrivial zeros (continuity of ζ where ζ s₀ ≠ 0; the order normal\n  form where ζ s₀ = 0, s₀ ≠ 1; the zetaA factorization at s₀ = 1), and\n  on that ball the series converges UNIFORMLY (Weierstrass M-test,\n  `HasSumUniformlyOn.of_norm_le_summable_eventually`) with analytic\n  partial sums.\n(§5) ISOLATION (`nontrivialZero_isolated`) and the reduced series\n  `seriesFunSub ρ₀` (the ρ₀-term zeroed out): analytic AT ρ₀\n  (`seriesFunSub_analyticAt`), so the polar subtraction\n  s ↦ seriesFun s − mult/(s−ρ₀) is analytic at ρ₀\n  (`seriesFun_sub_polar_analyticAt`) — the input 5e-iv needs for the\n  residue cancellation at the nontrivial zeros.\n\nArchive references: D-068 §3, journal-020/021 (the locally-uniform ⟹\nanalytic pattern), journal-015 (the ii′-1a dominator chain).\n-/\nimport Mathlib\nimport Zeta23.WeilEF.ZeroSummability\nimport Zeta23.Statement.SeamClosed\nimport NguyenRH1.LiSides\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n```\n\nWait — check LiSides namespace: decls like zeta_order_ne_top_of_ne are in NguyenRH1 namespace (used unqualified in LiDisc which is also NguyenRH1). ✓.\n\nNow §0:\n\n```lean\n/-! ## 0. The series -/\n\n/-- The zero-series summand: mult(ρ)·(1/(s−ρ) + 1/ρ) over the nontrivial\nzero subtype (the ii′-1a encoding; D-068 §3). -/\ndef seriesTerm (s : ℂ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ :=\n  (zeroMult ρ : ℂ) * (1 / (s - (ρ : ℂ)) + 1 / (ρ : ℂ))\n\n/-- The zero-side partial-fraction series. Summable at every s\n(`seriesSummable`), analytic off the nontrivial zeros\n(`seriesFun_analyticOnNhd`). -/\ndef seriesFun (s : ℂ) : ℂ := ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, seriesTerm s ρ\n```\n\n§1:\n\n```lean\n/-! ## 1. The norm comparison and the tail bound -/\n\n/-- For a nontrivial zero with 2 ≤ ‖ρ‖: 1 + ‖γ_ρ‖² ≤ (17/12)·‖ρ‖²\n(the γ-vs-‖·‖ comparison of the ii′-1a chain, with the constant for the\n‖ρ‖ ≥ 2 range: ‖γ‖² = im² + (1/2−re)² ≤ im² + 1/4 and im² ≥ ‖ρ‖² − 1 ≥ 3). -/\nlemma one_add_normSq_gammaOf_le (ρ : {ρ : ℂ // IsNontrivialZero ρ})\n    (hρ : (2 : ℝ) ≤ ‖(ρ : ℂ)‖) :\n    1 + Complex.normSq (gammaOf (ρ : ℂ)) ≤ 17 / 12 * ‖(ρ : ℂ)‖ ^ 2 := by\n  have hz := ρ.2\n  have hre0 : 0 < (ρ : ℂ).re := hz.2.1\n  have hre1 : (ρ : ℂ).re < 1 := hz.2.2\n  have hnorm : ‖(ρ : ℂ)‖ ^ 2 = (ρ : ℂ).re ^ 2 + (ρ : ℂ).im ^ 2 := by\n    rw [← Complex.normSq_eq_norm_sq, Complex.normSq_apply]\n    ring\n  have hgam : Complex.normSq (gammaOf (ρ : ℂ)) = (ρ : ℂ).im ^ 2 + (1 / 2 - (ρ : ℂ).re) ^ 2 := by\n    rw [Complex.normSq_apply, WeilEF.gammaOf_re, WeilEF.gammaOf_im]\n    ring\n  have hre2 : (ρ : ℂ).re ^ 2 ≤ 1 := by nlinarith [hre0, hre1]\n  have him2 : 3 ≤ (ρ : ℂ).im ^ 2 := by nlinarith [hρ, hnorm, hre2]  -- needs 4 ≤ ‖ρ‖²: from hρ: 2 ≤ ‖ρ‖: sq: 4 ≤ ‖ρ‖² — pow_le_pow_left₀ or nlinarith [hρ, norm_nonneg]\n  have hquarter : (1 / 2 - (ρ : ℂ).re) ^ 2 ≤ 1 / 4 := by nlinarith [hre0, hre1]\n  rw [hgam, hnorm]\n  nlinarith [him2, hquarter]\n```\n\nCheck nlinarith goals: him2: 3 ≤ im²: from ‖ρ‖² = re²+im², ‖ρ‖ ≥ 2 ⟹ ‖ρ‖² ≥ 4 (nlinarith: hρ : 2 ≤ ‖ρ‖, norm_nonneg ‖ρ‖ ≥ 0 ⟹ product (‖ρ‖−2)(‖ρ‖+2) ≥ 0 ⟹ ‖ρ‖² ≥ 4 ✓ nlinarith [hρ, norm_nonneg ‖(ρ:ℂ)‖]); re² ≤ 1 ⟹ im² = ‖ρ‖² − re² ≥ 4 − 1 = 3 ✓ nlinarith should manage with hnorm as an hypothesis (rw first? I rw [hgam, hnorm] at the END — the haves hnorm/hgam are used in nlinarith calls before the rewrite; hnorm is a hypothesis equation so nlinarith [hρ, hnorm, hre2]... but hnorm is in context already, no need to pass. Final goal after rw [hgam, hnorm]: 1 + (im² + (1/2−re)²) ≤ 17/12·(re²+im²). nlinarith [him2, hquarter, hre2...]: LHS ≤ 1 + im² + 1/4; want ≤ 17/12 re² + 17/12 im². From him2: im² ≥ 3. Hmm: 1 + im² + 1/4 ≤ 17/12(re²+im²) ⟺ 5/4 + im² ≤ 17/12 re² + 17/12 im² ⟸ 5/4 + im² ≤ 17/12 im² ⟺ 5/4 ≤ 5/12 im² ⟺ 3 ≤ im² ✓. nlinarith hint: needs (5/12)im² ≥ 5/4 from im² ≥ 3: linear ✓ and re² ≥ 0 (sq_nonneg) ✓. So `nlinarith [him2, hquarter, sq_nonneg (ρ:ℂ).re]`.\n\nhquarter: (1/2−re)² ≤ 1/4 ⟺ |1/2−re| ≤ 1/2 ⟺ 0 ≤ re ≤ 1: nlinarith [hre0, hre1]: (1/2−re)² − 1/4 = −re + re² = re(re−1) ≤ 0 since re > 0, re−1 < 0: product re(re−1) < 0: nlinarith product hint: it multiplies hre0·(hre1): re·(re − 1)... nlinarith proves (1/2−re)² ≤ 1/4 ⟺ re² − re + 1/4 ≤ 1/4 ⟺ re² ≤ re ⟺ re(re−1) ≤ 0: from hre0 (0 < re) and hre1 (re < 1): (re)·(1−re) > 0 ⟹ re − re² > 0: nlinarith multiplies hre0 and (1 − re > 0 from hre1) ✓ should find it.\n\nhre2: re² ≤ 1: re < 1, re > 0: re·re < 1·re·... nlinarith [hre0, hre1]: re² ≤ 1 ⟸ re² ≤ re (above) and re < 1: nlinarith finds via product (1−re)·re > 0 and re < 1... re² ≤ re < 1... wait need re² ≤ 1: re² ≤ re (from product) and re < 1 ⟹ re² < 1 ✓. nlinarith [hre0, hre1] ✓.\n\nThen:\n\n```lean\n/-- The key algebra: 1/(s−ρ) + 1/ρ = s/(ρ·(s−ρ)). -/\nlemma one_div_sub_add_one_div {s ρ : ℂ} (h0 : ρ ≠ 0) (h1 : s - ρ ≠ 0) :\n    1 / (s - ρ) + 1 / ρ = s / (ρ * (s - ρ)) := by\n  field_simp\n  ring\n```\n\nfield_simp with h0, h1 in context: goal 1/(s−ρ) + 1/ρ = s/(ρ·(s−ρ)): field_simp clears denominators: needs ρ*(s−ρ) ≠ 0 — mul_ne_zero h0 h1 might need to be in context; field_simp should find h0 h1 and maybe need the product: add `have := mul_ne_zero h0 h1`. After clearing: ρ + (s−ρ) = s? LHS·denom: 1/(s−ρ) = ρ·?/… let me trust field_simp + ring (banked gotcha: \"field_simp often closes goals (trailing ring errors)\").\n\n```lean\n/-- Tail bound: for 2 ≤ ‖ρ‖ and 2‖s‖ ≤ ‖ρ‖,\n‖seriesTerm s ρ‖ ≤ (17/6)·‖s‖·mult/(1+‖γ_ρ‖²). -/\nlemma seriesTerm_norm_le {s : ℂ} (ρ : {ρ : ℂ // IsNontrivialZero ρ})\n    (hρ2 : (2 : ℝ) ≤ ‖(ρ : ℂ)‖) (hsρ : 2 * ‖s‖ ≤ ‖(ρ : ℂ)‖) :\n    ‖seriesTerm s ρ‖ ≤\n      17 / 6 * ‖s‖ * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ)))) := by\n  have h0 : (ρ : ℂ) ≠ 0 := by\n    intro h; rw [h, norm_zero] at hρ2; linarith  -- norm_num at... 2 ≤ 0 false: linarith works: norm_zero: ‖0‖=0: hρ2 : 2 ≤ 0: linarith? norm_num closes: `norm_num at hρ2`. Use that.\n  have hρpos : (0 : ℝ) < ‖(ρ : ℂ)‖ := norm_pos_iff.mpr h0\n  have hsnorm : ‖s‖ ≤ ‖(ρ : ℂ)‖ / 2 := by linarith\n  have hsr : ‖s - (ρ : ℂ)‖ ≥ ‖(ρ : ℂ)‖ / 2 := by  -- use norm_sub_le reversed\n    have h := norm_sub_le_norm_sub... \n```\n\n‖s−ρ‖ ≥ ‖ρ‖ − ‖s‖ (norm_sub_norm_le? `norm_sub_le_norm_sub`? The reverse triangle: `norm_sub_le`? Mathlib: `norm_sub_le_norm_sub`? No: `abs_norm_sub_norm_le : |‖a‖ − ‖b‖| ≤ ‖a − b‖` — so ‖ρ‖ − ‖s‖ ≤ |‖ρ‖−‖s‖| ≤ ‖ρ − s‖ = ‖s − ρ‖ (norm_sub_rev). So:\n```lean\n  have hsr : ‖(ρ : ℂ)‖ / 2 ≤ ‖s - (ρ : ℂ)‖ := by\n    have h := abs_norm_sub_norm_le s (ρ : ℂ)  -- |‖s‖ − ‖ρ‖| ≤ ‖s − ρ‖\n    rw [abs_le] at h\n    have h2 := h.1  -- -(‖s‖−‖ρ‖) ≤ ‖s−ρ‖ i.e. ‖ρ‖−‖s‖ ≤ ‖s−ρ‖\n    linarith\n```\nThen s − ρ ≠ 0: norm_pos: ‖s−ρ‖ ≥ ‖ρ‖/2 > 0.\n\n```lean\n  have h1 : s - (ρ : ℂ) ≠ 0 := by\n    intro h; rw [h, norm_zero] at hsr; linarith\n  have hcomp := one_add_normSq_gammaOf_le ρ hρ2\n  have hg0 : (0 : ℝ) < 1 + Complex.normSq (gammaOf (ρ : ℂ)) := by\n    have := Complex.normSq_nonneg (gammaOf (ρ : ℂ)); linarith\n  have halg := one_div_sub_add_one_div h0 h1\n  rw [seriesTerm, halg, norm_mul, Complex.norm_natCast]  -- norm of (mult : ℂ) * (...): norm_mul gives ‖mult‖·‖s/(ρ(s−ρ))‖; Complex.norm_natCast: ‖(mult:ℂ)‖ = (mult:ℝ)... zeroMult ρ is ℕ; (zeroMult ρ : ℂ): norm_natCast: ‖(↑n : ℂ)‖ = ↑n? Complex.norm_natCast : ‖(n : ℂ)‖ = n. Hmm RCLike.norm_natCast was used in LiSkeleton: `RCLike.norm_natCast`. Both may exist. Use RCLike.norm_natCast like LiSkeleton.\n  rw [norm_div, norm_mul]\n  -- goal: (mult:ℝ) * (‖s‖ / (‖ρ‖ * ‖s−ρ‖)) ≤ 17/6 * ‖s‖ * (mult / (1+‖γ‖²))\n  have hmul0 : (0:ℝ) ≤ (zeroMult ρ : ℝ) := Nat.cast_nonneg _\n  -- ‖ρ‖·‖s−ρ‖ ≥ ‖ρ‖·(‖ρ‖/2) = ‖ρ‖²/2\n  have hden : ‖(ρ : ℂ)‖ ^ 2 / 2 ≤ ‖(ρ : ℂ)‖ * ‖s - (ρ : ℂ)‖ :=\n    by nlinarith [hsr, hρpos, norm_nonneg (s - (ρ:ℂ))]\n    -- mul_le_mul_of_nonneg_left hsr (le_of_lt hρpos) : ‖ρ‖·(‖ρ‖/2) ≤ ‖ρ‖·‖s−ρ‖; ring_nf\n  -- hence ‖s‖/(‖ρ‖‖s−ρ‖) ≤ ‖s‖/(‖ρ‖²/2) = 2‖s‖/‖ρ‖²\n  have hfrac : ‖s‖ / (‖(ρ : ℂ)‖ * ‖s - (ρ : ℂ)‖) ≤ 2 * ‖s‖ / ‖(ρ : ℂ)‖ ^ 2 := by\n    rw [div_le_div_iff₀ (by positivity...)] ...\n```\n\ndiv_le_div_iff₀ (ha : 0 < a) (hb : 0 < b): a/b ≤ c/d ⟺ ... signature: `div_le_div_iff₀ (hb : 0 < b) (hd : 0 < d) : a / b ≤ c / d ↔ a * d ≤ c * b`. Let me do: ‖s‖/D ≤ 2‖s‖/ρ² ⟺ ‖s‖·ρ² ≤ 2‖s‖·D (D = ‖ρ‖‖s−ρ‖ > 0): from D ≥ ρ²/2: 2‖s‖·D ≥ 2‖s‖·ρ²/2 = ‖s‖·ρ² ✓. positivity for ‖s‖ ≥ 0 fine.\n\nThen:\n```lean\n  calc (zeroMult ρ : ℝ) * (‖s‖ / (‖(ρ:ℂ)‖ * ‖s - (ρ:ℂ)‖))\n      ≤ (zeroMult ρ : ℝ) * (2 * ‖s‖ / ‖(ρ:ℂ)‖ ^ 2) := mul_le_mul_of_nonneg_left hfrac hmul0\n    _ = 2 * ‖s‖ * (zeroMult ρ : ℝ) / ‖(ρ:ℂ)‖ ^ 2 := by ring\n    _ ≤ 17 / 6 * ‖s‖ * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ:ℂ)))) := by\n        -- ⟺ 2·‖s‖·mult/ρ² ≤ (17/6)‖s‖·mult/(1+γ²)\n        -- ⟸ mult·‖s‖·(2/ρ² ≤ (17/6)/(1+γ²)) ⟸ 2/ρ² ≤ (17/6)/(1+γ²) ⟺ 2(1+γ²) ≤ (17/6)ρ² ⟸ 2·(17/12)ρ² = (17/6)ρ² ✓\n        rw [div_le_div_iff₀ (by positivity) hg0]  -- careful: LHS form A/ρ², RHS B/(1+γ²)\n        ...\n```\nLet me structure: \n```lean\n    have hinv : 2 * ‖s‖ * (zeroMult ρ : ℝ) / ‖(ρ:ℂ)‖ ^ 2\n        ≤ 17 / 6 * ‖s‖ * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ:ℂ)))) := by\n      rw [div_le_div_iff₀ (by positivity : (0:ℝ) < ‖(ρ:ℂ)‖ ^ 2) hg0]\n      -- goal: 2‖s‖mult·(1+γ²) ≤ (17/6‖s‖·mult)·ρ²  -- hmm RHS form: (17/6 * ‖s‖ * (mult/(1+γ²))) * ρ²... \n```\nCareful — after div_le_div_iff₀ with a = 2‖s‖mult, b = ρ², c = (17/6)‖s‖·mult... wait RHS is (17/6 * ‖s‖ * (mult/(1+γ²))) — that's not of the form c/d syntactically! It's a product containing a division. div_le_div_iff₀ won't apply. Restructure: show both sides as divisions: RHS = ((17/6)·‖s‖·mult)/(1+γ²) by ring (mul_div_assoc). So:\n\n```lean\n      have hR : 17 / 6 * ‖s‖ * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ:ℂ))))\n          = (17 / 6 * ‖s‖ * (zeroMult ρ : ℝ)) / (1 + Complex.normSq (gammaOf (ρ:ℂ))) := by ring\n      rw [hR, div_le_div_iff₀ (by positivity : (0:ℝ) < ‖(ρ:ℂ)‖ ^ 2) hg0]\n      -- goal: 2*‖s‖*mult * (1+γ²) ≤ (17/6*‖s‖*mult) * ρ²\n      have hkey : 2 * (1 + Complex.normSq (gammaOf (ρ:ℂ))) ≤ 17 / 6 * ‖(ρ:ℂ)‖ ^ 2 := by\n        linarith [hcomp]  -- hcomp: 1+γ² ≤ 17/12 ρ² ⟹ 2(1+γ²) ≤ 17/6 ρ² ✓\n      calc 2 * ‖s‖ * (zeroMult ρ:ℝ) * (1 + Complex.normSq (gammaOf (ρ:ℂ)))\n          = (‖s‖ * (zeroMult ρ:ℝ)) * (2 * (1 + Complex.normSq (gammaOf (ρ:ℂ)))) := by ring\n        _ ≤ (‖s‖ * (zeroMult ρ:ℝ)) * (17 / 6 * ‖(ρ:ℂ)‖ ^ 2) :=\n            mul_le_mul_of_nonneg_left hkey (by positivity)\n        _ = 17 / 6 * ‖s‖ * (zeroMult ρ:ℝ) * ‖(ρ:ℂ)‖ ^ 2 := by ring\n```\npositivity for ‖s‖·mult ≥ 0 ✓ (Nat.cast_nonneg & norm_nonneg — positivity handles).\n\nThen wrap the calc: LHS of goal is `‖(zeroMult ρ : ℂ)‖ * (‖s‖ / (‖ρ‖ * ‖s−ρ‖))` after the rewrites — hmm actually after `rw [seriesTerm, halg, norm_mul, RCLike.norm_natCast, norm_div, norm_mul]` the goal is `(↑(zeroMult ρ) : ℝ) * (‖s‖ / (‖ρ‖ * ‖s − ρ‖)) ≤ ...`. Note RCLike.norm_natCast gives ‖(n:ℂ)‖ = (n:ℝ)? RCLike.norm_natCast : ‖(n : R)‖ = n where the RHS is (n : ℝ)? For ℂ: ‖(n:ℂ)‖ = ↑n ✓. In liSummand_norm: `rw [liSummand_eq n ρ, norm_mul, RCLike.norm_natCast]` then `RCLike.norm_ofReal` — so RCLike.norm_natCast : ‖(↑n : 𝕜)‖ = ↑n (into ℝ) ✓.\n\nHmm — but wait, does `norm_natCast` match `(zeroMult ρ : ℂ)` where zeroMult ρ : ℕ? The cast is ℕ → ℂ: ‖((zeroMult ρ : ℕ) : ℂ)‖ = ((zeroMult ρ : ℕ) : ℝ) ✓.\n\nBut hold on: in my calc chain the goal after rw has LHS `(zeroMult ρ : ℝ) * (‖s‖ / (‖ρ‖ * ‖s − ρ‖))` — my calc starts with exactly that ✓. Actually `norm_div` on `‖s / (ρ * (s−ρ))‖` gives ‖s‖ / ‖ρ*(s−ρ)‖ then norm_mul gives ‖ρ‖·‖s−ρ‖ ✓.\n\n§2:\n\n```lean\n/-! ## 2. Summability -/\n\n/-- The subtype elements in a closed ball form a finite set (the ii′-1a\ncompact-finiteness pattern). -/\nlemma finite_subtype_norm_lt (R : ℝ) :\n    {ρ : {ρ : ℂ // IsNontrivialZero ρ} | ‖(ρ : ℂ)‖ < R}.Finite := by\n  have hcomp : IsCompact (Metric.closedBall (0 : ℂ) R) := isCompact_closedBall _ _\n  have hzeros : (Metric.closedBall (0 : ℂ) R) ∩ {ρ : ℂ | IsNontrivialZero ρ}\n      ⊆ (Metric.closedBall (0 : ℂ) R) ∩ riemannZetaZeros := by\n    intro z hz\n    exact ⟨hz.1, hz.2.1⟩\n  have hfin2 := (hcomp.inter_riemannZetaZeros_finite).subset hzeros\n  have himg : (Subtype.val '' {ρ : {ρ // IsNontrivialZero ρ} | ‖(ρ : ℂ)‖ < R}).Finite := by\n    apply hfin2.subset\n    rintro z ⟨ρ, hρ, rfl⟩\n    refine ⟨?_, ρ.2⟩\n    simp only [Metric.mem_closedBall, dist_zero_right]\n    exact le_of_lt hρ\n  exact Set.Finite.of_finite_image himg (Subtype.val_injective.injOn)\n```\n\nWait — in liSummable the set was `{ρ : {ρ // IsNontrivialZero ρ} | ¬ ((2:ℝ)*n ≤ ‖(ρ:ℂ)‖)}` and the image-subset argument used `lt_of_not_ge hρ`. Mine: ‖ρ‖ < R directly ⟹ dist ≤ R: le_of_lt hρ where hρ : ‖ρ‖ < R ✓ — but hρ after rintro: `⟨ρ, hρ, rfl⟩` where hρ : ‖(ρ:ℂ)‖ < R (the set membership). ✓. Also note in liSummable the membership target included `ρ.2` for the {IsNontrivialZero} part ✓ same.\n\nHmm — one difference: liSummable's hfin2/himg used the set-builder on the SUBTYPE with the negated condition; the Set.Finite.of_finite_image with Subtype.val_injective.injOn — wait `Set.Finite.of_finite_image (hs : (f '' s).Finite) (hi : Set.InjOn f s) : s.Finite` ✓.\n\nMembership: `hz.2.1` where hz.2 : IsNontrivialZero z — as discussed hz.2.1 : riemannZeta z = 0 — and membership in riemannZetaZeros is .rfl ✓ (liSummable line 312: `exact ⟨hz.1, hz.2.1⟩` ✓ copy).\n\n```lean\n/-- The series is absolutely summable at every s (the ii′-1a D-trick:\ndominator (17/6)(‖s‖+1)·mult/(1+‖γ‖²), finite head inside ‖ρ‖ < R₀). -/\ntheorem seriesSummable (s : ℂ) :\n    Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => seriesTerm s ρ) := by\n  set R₀ : ℝ := max 2 (2 * ‖s‖) with hR₀\n  have hR₀2 : (2 : ℝ) ≤ R₀ := le_max_left _ _\n  have hR₀s : 2 * ‖s‖ ≤ R₀ := le_max_right _ _\n  set C : ℝ := 17 / 6 * (‖s‖ + 1) with hC\n  have hbase : Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n      C * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ))))) :=\n    (WeilEF.zero_sum_inv_sq zetaSeam).mul_left C\n  set D : {ρ : ℂ // IsNontrivialZero ρ} → ℝ := fun ρ =>\n    if R₀ ≤ ‖(ρ : ℂ)‖ then\n      C * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ))))\n    else ‖seriesTerm s ρ‖ with hDdef\n  have hfin : {ρ : {ρ // IsNontrivialZero ρ} | ¬ (R₀ ≤ ‖(ρ : ℂ)‖)}.Finite := by\n    have := finite_subtype_norm_lt R₀\n    apply this.subset  -- hmm: {¬ R₀ ≤ ‖ρ‖} = {‖ρ‖ < R₀}: not_le: ¬(R₀ ≤ x) ↔ x < R₀ — defeq? not_le : ¬ a ≤ b ↔ b < a ✓ defeq? `not_le` is an iff (propext'd) — the SETS are equal by defeq of the membership? {x | ¬ R₀ ≤ ‖x‖} vs {x | ‖x‖ < R₀}: membership x ∈ {x | p x} is p x; p = ¬ R₀ ≤ ‖x‖ vs q = ‖x‖ < R₀: these are defeq (lt is DEFINED as ¬ ≤ in linear orders? x < y := x ≤ y ∧ ¬ y ≤ x in Mathlib's LT for ℝ?? ℝ's <: `lt_iff_le_not_ge`... For ℝ, a < b is defined via the LinearOrder instance — InstLT; Real.lt is defined as a ≤ b ∧ ¬ b ≤ a?? Actually Real's LT is defined directly (Real.lt := ...). Hmm risky. Use Set.Finite.subset with intro: `apply this.subset; intro ρ hρ; exact not_le.mp hρ` — subset direction: {¬ R₀ ≤ ‖ρ‖} ⊆ {‖ρ‖ < R₀}: not_le.mp ✓.\n  ...\n```\nCleaner: just call finite_subtype_norm_lt R₀ and subset via not_le.\n\nThen hE (D − base summable via finite support), hD, then Summable.of_norm_bounded hD with:\n```lean\n  refine Summable.of_norm_bounded D hD (fun ρ => ?_)\n  by_cases hρ : R₀ ≤ ‖(ρ : ℂ)‖\n  · simp only [D, if_pos hρ]\n    have h2 : (2:ℝ) ≤ ‖(ρ:ℂ)‖ := hR₀2.trans hρ\n    have hs2 : 2 * ‖s‖ ≤ ‖(ρ:ℂ)‖ := hR₀s.trans hρ\n    have h := seriesTerm_norm_le ρ h2 hs2\n    apply h.trans\n    -- (17/6)‖s‖·mult/(1+γ²) ≤ C·mult/(1+γ²): C = (17/6)(‖s‖+1)\n    rw [hC]  -- hmm hC : C = ... set already replaces. With `set`, C is substituted everywhere; use `show`. The dominator in D if_pos branch is C * (mult/(1+γ²)). Goal: 17/6*‖s‖*(mult/(1+γ²)) ≤ C*(mult/(1+γ²)).\n    -- Both as single divisions? D branch: C * (mult/(1+γ²)). seriesTerm_norm_le RHS: 17/6*‖s‖*(mult/(1+γ²)).\n    have hg0 : (0:ℝ) ≤ (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ:ℂ))) := by positivity\n    -- 17/6*‖s‖ ≤ 17/6*(‖s‖+1) = C\n    have hC' : 17 / 6 * ‖s‖ ≤ C := by rw [hC]; nlinarith [norm_nonneg s]  -- 17/6·‖s‖ ≤ 17/6·(‖s‖+1)\n    -- a * X ≤ b * X with X ≥ 0\n    calc 17 / 6 * ‖s‖ * ((zeroMult ρ:ℝ) / (1 + Complex.normSq (gammaOf (ρ:ℂ))))\n        ≤ C * ((zeroMult ρ:ℝ) / (1 + Complex.normSq (gammaOf (ρ:ℂ)))) :=\n          mul_le_mul_of_nonneg_right hC' hg0\n  · simp only [D, if_neg hρ, le_refl]\n```\nCareful with `set` and D's definition matching liSummable: in liSummable they used `set D ... with hDdef` and then `simp only [D, if_pos hρ]` — the set replaces occurrences; the D if-branch has C * (...) — but in liSummable they wrote the explicit constant (9/2)*(n:ℝ)^2 not a variable. With C a set-variable: hbase : Summable fun ρ => C * (...) ✓; hE : Summable fun ρ => D ρ − C*(...) via summable_of_hasFiniteSupport with support ⊆ {¬ R₀ ≤ ‖ρ‖}: for ρ ∉ support... the proof:\n```lean\n  have hE : Summable (fun ρ : {ρ // IsNontrivialZero ρ} =>\n      D ρ - C * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ:ℂ))))) := by\n    apply summable_of_hasFiniteSupport\n    apply hfin.subset\n    intro ρ hρ\n    simp only [Function.mem_support, ne_eq] at hρ\n    by_contra hball\n    apply hρ\n    have hball' : R₀ ≤ ‖(ρ : ℂ)‖ := not_not.mp hball\n    simp only [D, if_pos hball']\n    ring\n```\n✓ (mirrors liSummable lines 322–333).\n\nhD:\n```lean\n  have hD : Summable D := by\n    have hsum := hbase.add hE\n    have heq : (fun ρ : {ρ // IsNontrivialZero ρ} =>\n        C * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ:ℂ)))) +\n          (D ρ - C * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ:ℂ)))))) = D := by\n      funext ρ\n      ring\n    rw [heq] at hsum\n    exact hsum\n```\n✓ mirrors.\n\nHmm wait — in liSummable, `Summable.of_norm_bounded hD (fun ρ => ?_)` — signature: `Summable.of_norm_bounded (hg : Summable g) (h : ∀ i, ‖f i‖ ≤ g i) : Summable f`? Let me double check argument order: liSummable line 344: `refine Summable.of_norm_bounded hD (fun ρ => ?_)` — goal after refine: ∀ ρ... they did `fun ρ => ?_` so signature (f := _) (g := D) (hg : Summable D) (hfg : ∀ i, ‖f i‖ ≤ D i)? Wait: `Summable.of_norm_bounded {f g : ι → α} (hg : Summable g) (hfg : ∀ i, ‖f i‖ ≤ g i) : Summable f`? Hmm but then `refine Summable.of_norm_bounded hD (fun ρ => ?_)` leaves goal `‖seriesTerm s ρ‖ ≤ D ρ` ✓ matches. But there might be a Real requirement: g : ι → ℝ — `Summable.of_norm_bounded` for real g: yes `Summable.of_norm_bounded (hg : Summable g) (h : ∀ i, ‖f i‖ ≤ g i)` requires g real-valued I think (or NormedField). D is ℝ-valued ✓.\n\nAlso check: in liSummable the goal was Summable (liSummand n) — the def; here Summable (fun ρ => seriesTerm s ρ) — I'll state seriesSummable as Summable (seriesTerm s)?? seriesTerm s : subtype → ℂ ✓ can state `Summable (seriesTerm s)`. Hmm but with `refine Summable.of_norm_bounded hD ...` the f is inferred from goal ✓.\n\n§4:\n\n```lean\n/-! ## 3. Balls avoiding the nontrivial zeros -/\n\n/-- Around any point that is not a nontrivial zero there is a ball\ncontaining no nontrivial zero: continuity where ζ s₀ ≠ 0; the order\nnormal form where ζ s₀ = 0, s₀ ≠ 1; the zetaA factorization at s₀ = 1. -/\nlemma exists_ball_avoid_nontrivialZeros (s₀ : ℂ) (hs₀ : ¬ IsNontrivialZero s₀) :\n    ∃ δ : ℝ, 0 < δ ∧ ∀ ρ : {ρ : ℂ // IsNontrivialZero ρ}, (ρ : ℂ) ∉ Metric.ball s₀ δ := by\n  by_cases h1 : s₀ = 1\n  · subst h1\n    obtain ⟨ε, hε, hball⟩ := Metric.eventually_nhds_iff_ball.mp zetaA_ne_zero_near_one\n    refine ⟨ε, hε, fun ρ hρ => ?_⟩\n    -- ρ nontrivial zero in ball(1, ε): ρ ≠ 1 (re < 1), zetaA ρ = (ρ−1)ζ ρ = 0 contra hball\n    have hρ1 : (ρ : ℂ) ≠ 1 := by\n      intro h\n      have : (ρ : ℂ).re < 1 := ρ.2.2.2\n      rw [h] at this\n      simp at this  -- this : (1:ℂ).re < 1 → re 1 = 1: 1 < 1 false: `rw [Complex.one_re] at this; exact lt_irrefl _ this`? simp should close: Complex.one_re is simp. Use: rw [h, Complex.one_re] at this; exact lt_irrefl 1 this.\n    have hz := hball (ρ : ℂ) hρ\n    rw [zetaA_apply hρ1] at hz  -- zetaA ρ = (ρ−1)·ζ ρ\n    rw [ρ.2.1, mul_zero] at hz  -- ζ ρ = 0: ρ.2.1 : riemannZeta ↑ρ = 0 ✓\n    exact hz rfl\n  · by_cases h0 : riemannZeta s₀ = 0\n    · -- NF\n      obtain ⟨h, hh, hh0, hfh⟩ :=\n        (analyticAt_riemannZeta h1).analyticOrderAt_ne_top.mp (zeta_order_ne_top_of_ne h1)\n      obtain ⟨ε₁, hε₁, hball₁⟩ := Metric.eventually_nhds_iff_ball.mp\n        (hh.continuousAt.eventually_ne hh0)\n      obtain ⟨ε₂, hε₂, hball₂⟩ := Metric.eventually_nhds_iff_ball.mp hfh\n      refine ⟨min ε₁ ε₂, lt_min hε₁ hε₂, fun ρ hρ => ?_⟩\n      -- ρ ∈ ball s₀ (min ε₁ ε₂): ζ ρ = (ρ−s₀)^m • h ρ\n      have hmem1 : (ρ : ℂ) ∈ Metric.ball s₀ ε₁ := Metric.ball_subset_ball (min_le_left _ _) hρ\n      have hmem2 : (ρ : ℂ) ∈ Metric.ball s₀ ε₂ := Metric.ball_subset_ball (min_le_right _ _) hρ\n      have heq := hball₂ (ρ : ℂ) hmem2  -- ζ ρ = (ρ − s₀)^m • h ρ\n      have hne : h (ρ : ℂ) ≠ 0 := hball₁ (ρ : ℂ) hmem1\n      have hpow : ((ρ : ℂ) - s₀) ^ analyticOrderNatAt riemannZeta s₀ ≠ 0 ∨ ... \n      -- need: either ρ = s₀ (then contra hs₀) or pow ≠ 0\n      by_cases hρs : (ρ : ℂ) = s₀\n      · rw [hρs] at hs₀? no: ρ nontrivial, ρ = s₀ ⟹ IsNontrivialZero s₀: exact hs₀ (hρs ▸ ρ.2)\n      · have hpow : ((ρ : ℂ) - s₀) ^ analyticOrderNatAt riemannZeta s₀ ≠ 0 :=\n          pow_ne_zero _ (sub_ne_zero.mpr hρs)\n        have hz : riemannZeta (ρ : ℂ) ≠ 0 := by\n          rw [heq, smul_eq_mul]  -- (pow • h ρ): smul_eq_mul\n          exact mul_ne_zero hpow hne\n        exact hz ρ.2.1\n    · -- continuity\n      obtain ⟨ε, hε, hball⟩ := Metric.eventually_nhds_iff_ball.mp\n        ((analyticAt_riemannZeta h1).continuousAt.eventually_ne h0)\n      refine ⟨ε, hε, fun ρ hρ => ?_⟩\n      exact hball (ρ : ℂ) hρ ρ.2.1\n```\n\nCheck details:\n- `zetaA_ne_zero_near_one : ∀ᶠ w in 𝓝 (1:ℂ), zetaA w ≠ 0` ✓ (LiResidue line 81).\n- After subst h1, s₀ replaced by 1 ✓.\n- ρ.2.2.2 : (ρ:ℂ).re < 1: ρ.2 : ζ ρ = 0 ∧ 0 < re ∧ re < 1: ρ.2.2.2... ρ.2.2 : 0 < re ∧ re < 1? Hmm: And association: a ∧ b ∧ c = a ∧ (b ∧ c): ρ.2.1 : a = ζ ρ = 0; ρ.2.2 : b ∧ c; ρ.2.2.1?? Accessing nested: ρ.2.2.1 = (b ∧ c).1 = b? Wait — .2.2 is (ρ.2).2 : b ∧ c. Then .2.2.1 : b, .2.2.2 : c. Hmm but earlier in liSummand_norm_le: hz.2.1.le : 0 ≤ re where hz = ρ.2 : hz.2 : b ∧ c... hz.2.1 : (b ∧ c).1 = b = 0 < re ✓ .le : 0 ≤ ✓. And hz.2.2.le : re ≤ 1: hz.2.2 : c = re < 1 ✓. So: ρ.2.1 : ζ ρ = 0; ρ.2.2.1 : 0 < re; ρ.2.2.2 : re < 1. In my draft above I wrote `ρ.2.2.2` for re < 1 ✓ and `ρ.2.1` for ζ ρ = 0 ✓. But careful — earlier in finite_subtype_norm_lt I wrote `hz.2.1` for the riemannZetaZeros membership where hz : z ∈ closedBall ∧ IsNontrivialZero z: hz.2 : IsNontrivialZero z; hz.2.1 : ζ z = 0 ✓ consistent.\n\n- For `rw [h] at this` where this : (ρ:ℂ).re < 1 and h : (ρ:ℂ) = 1: gives (1:ℂ).re < 1; then `simp at this`: Complex.one_re : (1:ℂ).re = 1 — simp reduces to 1 < 1 = False, closes goal? `simp at this` with this : 1 < 1 → this becomes False → closes any goal ✓ (simp at this with False closes). OK.\n- `Metric.ball_subset_ball : ε₁ ≤ ε₂ → ball x ε₁ ⊆ ball x ε₂` ✓ exists. Membership: hρ : (ρ:ℂ) ∈ ball s₀ (min ε₁ ε₂); ball_subset_ball (min_le_left ε₁ ε₂) hρ — hρ needs coercion to set membership ✓ fine.\n- heq : riemannZeta (ρ:ℂ) = ((ρ:ℂ) − s₀) ^ analyticOrderNatAt riemannZeta s₀ • h (ρ:ℂ). hball₂ : ∀ y ∈ ball s₀ ε₂, riemannZeta y = ... ✓ (hfh is =ᶠ[𝓝 s₀]: eventually_nhds_iff_ball.mp gives ∃ ε > 0, ∀ y ∈ ball, f y = g y ✓).\n- smul_eq_mul ✓.\n- hρs ▸ ρ.2: ρ.2 : IsNontrivialZero (ρ:ℂ); hρs : (ρ:ℂ) = s₀; hρs ▸ ρ.2 : IsNontrivialZero s₀ ✓ (▸ direction: rewrites (ρ:ℂ) to s₀ in the type ✓).\n- continuity case: hball : ∀ y ∈ ball s₀ ε, riemannZeta y ≠ 0 ✓; exact hball (ρ:ℂ) hρ ρ.2.1 : hball ... : ζ ρ ≠ 0 applied to ρ.2.1 : ζ ρ = 0 gives False, goal is (ρ:ℂ) ∉ ball — wait! The goal is `(ρ:ℂ) ∉ Metric.ball s₀ δ` and hρ : (ρ:ℂ) ∈ ball... I wrote `fun ρ hρ => ?_` — hρ : (ρ:ℂ) ∈ Metric.ball s₀ δ ✓, goal False? No — goal after intro ρ hρ: the statement ∀ ρ, (ρ:ℂ) ∉ ball — `fun ρ hρ => ?_` with hρ : ∈ ball, then goal is False (∉ unfolds to ¬ ∈ = ∈ → False). ✓ So exact hz ρ.2.1 where hz : ζ ρ ≠ 0, ρ.2.1 : ζ ρ = 0 ⟹ False ✓. In zetaA case: exact hz rfl where hz : zetaA ρ = 0 → False... wait hz := hball ρ hρ : zetaA ρ ≠ 0; after rw [zetaA_apply hρ1, ρ.2.1, mul_zero] at hz: hz : (0:ℂ) ≠ 0; exact hz rfl ✓.\n\nHmm — `rw [ρ.2.1, mul_zero] at hz`: hz : (ρ − 1)·ζ ρ ≠ 0 — rw ρ.2.1 : ζ ρ = 0 at hz: hz : (ρ−1)*0 ≠ 0; rw [mul_zero] at hz: hz : (0:ℂ) ≠ 0 ✓. But wait — after rw [zetaA_apply hρ1] at hz, hz : (ρ−1) * riemannZeta ρ ≠ 0 ✓.\n\nNow §4 analyticity:\n\n```lean\n/-! ## 4. Analyticity off the zeros -/\n\n/-- The M-test majorant on a ball avoiding the zeros. -/\nlemma seriesTerm_summable_majorant (M : ℝ) :\n    Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n      17 / 6 * M * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ))))) :=\n  (WeilEF.zero_sum_inv_sq zetaSeam).mul_left _\n\ntheorem seriesFun_analyticAt {s₀ : ℂ} (hs₀ : ¬ IsNontrivialZero s₀) :\n    AnalyticAt ℂ seriesFun s₀ := by\n  obtain ⟨δ, hδ, hball⟩ := exists_ball_avoid_nontrivialZeros s₀ hs₀\n  set M : ℝ := ‖s₀‖ + δ with hM\n  set R₀ : ℝ := max 2 (2 * M) with hR₀\n  -- the dominator\n  set u : {ρ : ℂ // IsNontrivialZero ρ} → ℝ := fun ρ =>\n    17 / 6 * M * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ)))) with hu\n  have hsum_u : Summable u := seriesTerm_summable_majorant M\n  -- the eventual bound\n  have hfu : ∀ᶠ ρ in cofinite, ∀ s ∈ Metric.ball s₀ δ, ‖seriesTerm s ρ‖ ≤ u ρ := by\n    rw [Filter.mem_cofinite]  -- hmm: ∀ᶠ in cofinite ↔ the set of good ρ is cofinite; use Filter.eventually_cofinite: (∀ᶠ x in cofinite, p x) ↔ {x | p x}ᶜ.Finite? There's `Filter.eventually_cofinite : (∀ᶠ x in cofinite, p x) ↔ {x | ¬ p x}.Finite`. Use that.\n    ...\n```\n`Filter.eventually_cofinite : (∀ᶠ x ∈ cofinite? ...)`: statement `Filter.eventually_cofinite {p : α → Prop} : (∀ᶠ x in cofinite, p x) ↔ {x | ¬p x}.Finite` — exists? I believe yes. Then show {ρ | ¬ ∀ s ∈ ball, ...}.Finite ⊆ {ρ | ‖ρ‖ < R₀} finite: if ‖ρ‖ ≥ R₀ then the bound holds: need ¬(∀...) ⟹ ‖ρ‖ < R₀ — i.e. prove {ρ | ¬P ρ} ⊆ {ρ | ‖ρ‖ < R₀} then .subset.\n\nFor ρ with R₀ ≤ ‖ρ‖, prove P ρ: ∀ s ∈ ball, ‖seriesTerm s ρ‖ ≤ u ρ:\n- h2 : 2 ≤ ‖ρ‖ (max_left trans)\n- s ∈ ball s₀ δ: ‖s‖ ≤ ‖s₀‖ + δ = M: ‖s‖ = ‖(s − s₀) + s₀‖ ≤ ‖s−s₀‖ + ‖s₀‖ < δ + ‖s₀‖: from mem_ball: dist s s₀ < δ: dist_eq_norm: ‖s − s₀‖ < δ ✓; so ‖s‖ < M hence ≤.\n- 2‖s‖ ≤ 2M ≤ R₀ ≤ ‖ρ‖ ✓ (max_right).\n- seriesTerm_norm_le ρ h2 hs2 : ‖term‖ ≤ 17/6·‖s‖·mult/(1+γ²).\n- ≤ 17/6·M·mult/(1+γ²) = u ρ: since ‖s‖ ≤ M and the other factor ≥ 0: \n  17/6*‖s‖*(mult/(1+γ²)) ≤ 17/6*M*(mult/(1+γ²)): mul_le_mul_of_nonneg_right (by nlinarith/linarith: 17/6·‖s‖ ≤ 17/6·M) (positivity) ✓.\n\n- Then:\n```lean\n  have hu' : HasSumUniformlyOn (fun ρ => fun s : ℂ => seriesTerm s ρ)\n      (fun s => ∑' ρ, seriesTerm s ρ) (Metric.ball s₀ δ) :=\n    HasSumUniformlyOn.of_norm_le_summable_eventually hsum_u hfu\n  have htend : TendstoLocallyUniformlyOn\n      (fun t : Finset {ρ : ℂ // IsNontrivialZero ρ} => fun s => ∑ ρ ∈ t, seriesTerm s ρ)\n      (fun s => ∑' ρ, seriesTerm s ρ) atTop (Metric.ball s₀ δ) :=\n    TendstoUniformlyOn.tendstoLocallyUniformlyOn\n      (hasSumUniformlyOn_iff_tendstoUniformlyOn.mp hu')\n  have hdiff : DifferentiableOn ℂ (fun s => ∑' ρ, seriesTerm s ρ) (Metric.ball s₀ δ) := by\n    apply htend.differentiableOn _ isOpen_ball\n    apply Filter.Eventually.of_forall\n    intro t s hs\n    rw [show (fun s => ∑ ρ ∈ t, seriesTerm s ρ) = ∑ ρ ∈ t, (fun s => seriesTerm s ρ) from by\n      funext s; simp [Finset.sum_apply]]\n    apply DifferentiableAt.differentiableWithinAt\n    apply DifferentiableAt.sum\n    intro ρ hρ\n    -- each term differentiable at s: s ≠ ρ (ball avoids zeros), ρ ≠ 0\n    have hsρ : s - (ρ : ℂ) ≠ 0 := by\n      have hρout : (ρ : ℂ) ∉ Metric.ball s₀ δ := hball ρ\n      intro h\n      apply hρout\n      -- s − ρ = 0 ⟹ ρ = s ∈ ball\n      have : (ρ : ℂ) = s := sub_eq_zero.mp h  -- h : s − ρ = 0 ⟹ s = ρ: sub_eq_zero : s − ρ = 0 ↔ s = ρ: gives s = ρ: then ρ = s via .symm\n      rw [← this]  -- hmm: want ρ ∈ ball: rw this: ρ ↦ s: goal s ∈ ball: exact hs\n      exact hs  -- wait membership: hs : s ∈ ball s₀ δ from DifferentiableOn intro\n    have hρ0 : (ρ : ℂ) ≠ 0 := by\n      intro h\n      have := ρ.2.2.1  -- 0 < (ρ:ℂ).re\n      rw [h] at this\n      simp at this  -- (0:ℂ).re < ... : 0 < 0 false\n    have h1 : DifferentiableAt ℂ (fun s : ℂ => 1 / (s - (ρ : ℂ))) s :=\n      (differentiableAt_const (1 : ℂ)).div\n        (differentiableAt_id.sub (differentiableAt_const _)) hsρ\n    have h2 : DifferentiableAt ℂ (fun s : ℂ => 1 / (ρ : ℂ)) s := differentiableAt_const _\n    show DifferentiableAt ℂ (fun s => (zeroMult ρ : ℂ) * (1 / (s - (ρ : ℂ)) + 1 / (ρ : ℂ))) s\n    exact (h1.add h2).const_mul _\n```\nHmm — the goal after `apply DifferentiableAt.sum; intro ρ hρ` is `DifferentiableAt ℂ (fun s => seriesTerm s ρ) s`? Actually DifferentiableAt.sum signature: `DifferentiableAt.sum (h : ∀ i ∈ t, DifferentiableAt ℂ (f i) x) : DifferentiableAt ℂ (∑ i ∈ t, f i) x`? In LiDigamma: `apply DifferentiableAt.sum; intro m hm; ...exact h1.sub h2` where the goal was DifferentiableAt ℂ (fun s => dpsiTermC s m) s and they proved it via pieces with `show` implicit. dpsiTermC was a def — the goal displayed as the def but reducible. For me: goal DifferentiableAt ℂ (fun s => seriesTerm s ρ) s; seriesTerm is a def — `(h1.add h2).const_mul _` has type DifferentiableAt ℂ (fun s => mult * (1/(s−ρ) + 1/ρ))?? `.const_mul : DifferentiableAt ℂ f x → DifferentiableAt ℂ (fun y => c * f y) x` gives fun s => c * (1/(s−ρ)+1/ρ) — with c = (zeroMult ρ : ℂ): matches seriesTerm s ρ up to def-unfolding: need `show DifferentiableAt ℂ (fun s => (zeroMult ρ : ℂ) * (1 / (s - (ρ:ℂ)) + 1 / (ρ:ℂ))) s` first (defeq unfold) ✓.\n\nAlso `intro t s hs` — the Eventually goal: ∀ᶠ t in atTop, DifferentiableOn ℂ (fun s => ∑ ρ∈t, seriesTerm s ρ) (ball): `Filter.Eventually.of_forall; intro t` then goal DifferentiableOn ...; DifferentiableOn is ∀ s ∈ ball, DifferentiableWithinAt: `intro s hs` ✓ (LiDigamma did `intro t s hs` after of_forall ✓).\n\n- Then:\n```lean\n  have han : AnalyticOnNhd ℂ (fun s => ∑' ρ, seriesTerm s ρ) (Metric.ball s₀ δ) :=\n    hdiff.analyticOnNhd isOpen_ball\n  -- AnalyticAt at s₀: han s₀ (mem_ball_self hδ) : AnalyticAt ℂ (fun s => ∑' ...) s₀\n  -- and seriesFun = fun s => ∑' ρ, seriesTerm s ρ by rfl\n  exact han s₀ (Metric.mem_ball_self hδ)\n```\nWait — AnalyticOnNhd ℂ f s = ∀ x ∈ s, AnalyticAt ℂ f x: `han s₀ (mem)` : AnalyticAt ℂ (fun s => ∑' ρ, seriesTerm s ρ) s₀. Goal: AnalyticAt ℂ seriesFun s₀. seriesFun s₀ := ∑' ρ, seriesTerm s₀ ρ — but AnalyticAt ℂ f x with f = the lambda vs f = seriesFun: these are different functions (seriesFun is a def whose unfolding gives the lambda). AnalyticAt ℂ seriesFun s₀ — the lambda `fun s => ∑' ρ, seriesTerm s ρ` is DEFEQ to seriesFun (funext-free: seriesFun unfolds to fun s => ∑' ρ, seriesTerm s ρ ✓ definitionally). So `exact han s₀ hmem` should typecheck by defeq ✓ (like DinfC in LiDigamma — they did need a funext rw for the Pi.add form, but plain def unfolding is defeq).\n\n```lean\n/-- The series is analytic on the complement of the nontrivial zeros. -/\ntheorem seriesFun_analyticOnNhd :\n    AnalyticOnNhd ℂ seriesFun {s : ℂ | ¬ IsNontrivialZero s} :=\n  fun s₀ hs₀ => seriesFun_analyticAt hs₀\n```\n\n§5:\n\n```lean\n/-! ## 5. Isolation and the reduced series -/\n\n/-- Each nontrivial zero is isolated from the others (finiteness in\ncompact balls + minimum distance). -/\ntheorem nontrivialZero_isolated (ρ₀ : {ρ : ℂ // IsNontrivialZero ρ}) :\n    ∃ δ : ℝ, 0 < δ ∧ ∀ ρ₁ : {ρ : ℂ // IsNontrivialZero ρ}, ρ₁ ≠ ρ₀ →\n      δ ≤ ‖(ρ₁ : ℂ) - (ρ₀ : ℂ)‖ := by\n  -- the nontrivial zeros in closedBall ρ₀ 1 form a finite set\n  have hcomp : IsCompact (Metric.closedBall (ρ₀ : ℂ) 1) := isCompact_closedBall _ _\n  have hzeros : (Metric.closedBall (ρ₀ : ℂ) 1) ∩ {ρ : ℂ | IsNontrivialZero ρ}\n      ⊆ (Metric.closedBall (ρ₀ : ℂ) 1) ∩ riemannZetaZeros := by\n    intro z hz\n    exact ⟨hz.1, hz.2.1⟩\n  have hfin : ((Metric.closedBall (ρ₀ : ℂ) 1) ∩ {ρ : ℂ | IsNontrivialZero ρ}).Finite :=\n    (hcomp.inter_riemannZetaZeros_finite).subset hzeros\n  -- as a finset of subtype elements (excluding ρ₀)\n  set S : Set {ρ : ℂ // IsNontrivialZero ρ} :=\n    {ρ | (ρ : ℂ) ∈ Metric.closedBall (ρ₀ : ℂ) 1 ∧ ρ ≠ ρ₀} with hS\n  have hSfin : S.Finite := by\n    have himg : (Subtype.val '' S).Finite := by\n      apply hfin.subset\n      rintro z ⟨ρ, ⟨hρ, -⟩, rfl⟩\n      exact ⟨hρ, ρ.2⟩\n    exact Set.Finite.of_finite_image himg (Subtype.val_injective.injOn)\n  by_cases hne : S.Nonempty\n  · -- δ = (min distance)/2\n    set d : Finset ℝ := hSfin.toFinset.image (fun ρ => ‖(ρ : ℂ) - (ρ₀ : ℂ)‖) with hd\n    have hdne : d.Nonempty := by\n      obtain ⟨ρ, hρ⟩ := hne\n      refine ⟨‖(ρ : ℂ) - (ρ₀ : ℂ)‖, ?_⟩\n      simp only [hd, Finset.mem_image, Set.Finite.mem_toFinset]\n      exact ⟨ρ, hρ, rfl⟩\n    have hdpos : ∀ x ∈ d, 0 < x := by\n      intro x hx\n      simp only [hd, Finset.mem_image, Set.Finite.mem_toFinset] at hx\n      obtain ⟨ρ, hρ, rfl⟩ := hx\n      have h1 : (ρ : ℂ) ≠ (ρ₀ : ℂ) := fun h => hρ.2 (Subtype.ext h)\n      exact norm_pos_iff.mpr (sub_ne_zero.mpr h1)\n    refine ⟨d.min' hdne / 2, by positivity?, fun ρ₁ hρ₁ => ?_⟩\n    · positivity needs d.min' hdne > 0: hdpos _ (d.min'_mem hdne): have := hdpos _ (d.min'_mem hdne); positivity? no — positivity can't use hypotheses. `exact half_pos (hdpos _ (Finset.min'_mem _ _))`... half_pos : 0 < a/2? `half_pos (h : 0 < a) : 0 < a / 2` ✓.\n    · by_cases hmem : (ρ₁ : ℂ) ∈ Metric.closedBall (ρ₀ : ℂ) 1\n      · -- ρ₁ ∈ S ⟹ its distance ∈ d ≥ min'\n        have h1 : ρ₁ ∈ S := ⟨hmem, hρ₁⟩\n        have h2 : ‖(ρ₁ : ℂ) - (ρ₀ : ℂ)‖ ∈ d := by\n          simp only [hd, Finset.mem_image, Set.Finite.mem_toFinset]\n          exact ⟨ρ₁, h1, rfl⟩\n        have h3 : d.min' hdne ≤ ‖(ρ₁ : ℂ) - (ρ₀ : ℂ)‖ := Finset.min'_le _ _ h2\n        linarith [hdpos _ (Finset.min'_mem _ _)]\n      · -- outside the ball: dist ≥ 1 ≥ min'/2 (min' ≤ 1 since distances in the ball ≤ 1)\n        have h4 : 1 ≤ ‖(ρ₁ : ℂ) - (ρ₀ : ℂ)‖ := by\n          have : (1 : ℝ) ≤ dist (ρ₁ : ℂ) (ρ₀ : ℂ) := by\n            by_contra h\n            apply hmem\n            rw [Metric.mem_closedBall]\n            exact le_of_lt (not_le.mp h)\n          rwa [dist_eq_norm] at this\n        -- min' ≤ 1: min' ∈ d comes from a ball element: any element of d is ≤ 1\n        have h5 : d.min' hdne ≤ 1 := by\n          have hm := Finset.min'_mem d hdne\n          simp only [hd, Finset.mem_image, Set.Finite.mem_toFinset] at hm\n          obtain ⟨ρ, hρ, rfl⟩ := hm\n          rw [Metric.mem_closedBall, dist_eq_norm] at hρ  -- hρ.1 : dist ≤ 1\n          -- hρ : (ρ:ℂ) ∈ closedBall ∧ ρ ≠ ρ₀; hρ.1 : dist (ρ:ℂ) ρ₀ ≤ 1: dist_eq_norm: ‖ρ − ρ₀‖ ≤ 1 ✓\n          exact hρ.1\n        linarith\n  · refine ⟨1 / 2, by norm_num, fun ρ₁ hρ₁ => ?_⟩\n    by_contra h\n    push_neg at h  -- h : ‖ρ₁ − ρ₀‖ < 1/2\n    apply hne  -- S nonempty: ρ₁ ∈ S\n    -- ρ₁ ∈ S: dist < 1/2 < 1 ⟹ in closedBall; ≠ ρ₀ ✓\n    exact ⟨ρ₁, ⟨by rw [Metric.mem_closedBall, dist_eq_norm]; linarith, hρ₁⟩⟩... \n    -- hne : ¬ S.Nonempty: apply hne: goal S.Nonempty: exact ⟨ρ₁, hSmem⟩: Set.Nonempty def: ∃ x, x ∈ S: ⟨ρ₁, ...⟩: S membership is the pair ✓\n```\nCareful: `by_contra h` on goal `1/2 ≤ ‖ρ₁ − ρ₀‖`: push_neg gives ‖…‖ < 1/2 ✓. Then S.Nonempty ⟨ρ₁, hmem_pair⟩ where hmem_pair : (ρ₁:ℂ) ∈ closedBall ∧ ρ₁ ≠ ρ₀ ✓; hne : ¬S.Nonempty — apply hne then exact the Nonempty... `exact hne ⟨ρ₁, ...⟩` ✓.\n\nHmm — `Set.Finite.mem_toFinset` needs the set to match hSfin.toFinset: membership ρ ∈ hSfin.toFinset ↔ ρ ∈ S ✓ via Set.Finite.mem_toFinset (hSfin : S.Finite) — as a simp lemma it fires as written? `Set.Finite.mem_toFinset (hs : s.Finite) : x ∈ hs.toFinset ↔ x ∈ s` — in simp only I should write `Set.Finite.mem_toFinset` and it rewrites `x ∈ hSfin.toFinset` to `x ∈ S` — but d was defined with hSfin.toFinset ✓.\n\nOne concern: `simp only [hd, Finset.mem_image, Set.Finite.mem_toFinset]` — hd is a `set` equation: simp only [hd]?? With `set ... with hd`, hd : d = hSfin.toFinset.image ... — simp only [hd] rewrites d → the image ✓ then mem_image ✓ then mem_toFinset ✓. Wait actually with `set`, occurrences of the image-finset get replaced by d in the goal — the goal has d; simp [hd] rewrites d back. But `set` also abstracts... fine, this pattern works (banked in previous files presumably).\n\nAlternative simpler for h2/hmem: `Finset.mem_image.mpr ⟨ρ₁, by rwa [Set.Finite.mem_toFinset], rfl⟩`. I'll use explicit .mpr forms to be safe.\n\n- reduced series:\n```lean\n/-- The reduced summand: the ρ₀-term zeroed out. -/\ndef seriesTermSub (ρ₀ : {ρ : ℂ // IsNontrivialZero ρ}) (s : ℂ)\n    (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ :=\n  if ρ = ρ₀ then 0 else seriesTerm s ρ\n\n/-- The reduced series (the ρ₀ polar term removed): analytic AT ρ₀. -/\ndef seriesFunSub (ρ₀ : {ρ : ℂ // IsNontrivialZero ρ}) (s : ℂ) : ℂ :=\n  ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, seriesTermSub ρ₀ s ρ\n\nlemma seriesTermSub_norm_le (ρ₀ : {ρ : ℂ // IsNontrivialZero ρ}) (s : ℂ)\n    (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ‖seriesTermSub ρ₀ s ρ‖ ≤ ‖seriesTerm s ρ‖ := by\n  by_cases h : ρ = ρ₀ <;> simp [seriesTermSub, h]\n\ntheorem seriesTermSub_summable (ρ₀ : {ρ : ℂ // IsNontrivialZero ρ}) (s : ℂ) :\n    Summable (seriesTermSub ρ₀ s) :=\n  Summable.of_norm_bounded (seriesSummable s) (fun ρ => seriesTermSub_norm_le ρ₀ s ρ)\n```\nWait — Summable.of_norm_bounded with g = seriesTerm s (ℂ-valued) — fine (norm_bounded works for any normed g? signature: (hg : Summable g) (h : ∀ i, ‖f i‖ ≤ g i) — hmm if g is ℂ-valued then g i : ℂ but ‖f i‖ : ℝ ≤ g i : ℂ — type error! of_norm_bounded requires g : ι → ℝ. seriesTerm s is ℂ-valued! So this fails. Options: g := fun ρ => ‖seriesTerm s ρ‖: Summable (fun ρ => ‖seriesTerm s ρ‖) — from seriesSummable: `Summable.norm`? `Summable.norm (hf : Summable f) : Summable (fun i => ‖f i‖)` ✓ exists. So:\n```lean\n  Summable.of_norm_bounded (seriesSummable s).norm (fun ρ => seriesTermSub_norm_le ρ₀ s ρ)\n```\n✓.\n\nThen the pointwise split:\n```lean\nlemma seriesTerm_add_single (ρ₀ : {ρ : ℂ // IsNontrivialZero ρ}) (s : ℂ) :\n    (fun ρ => seriesTerm s ρ) =\n      (fun ρ => seriesTermSub ρ₀ s ρ) + (fun ρ => if ρ = ρ₀ then seriesTerm s ρ else 0) := by\n  funext ρ\n  by_cases h : ρ = ρ₀ <;> simp [seriesTermSub, h]\n\nlemma single_summable (ρ₀ : {ρ : ℂ // IsNontrivialZero ρ}) (s : ℂ) :\n    Summable (fun ρ => if ρ = ρ₀ then seriesTerm s ρ else (0 : ℂ)) := by\n  apply summable_of_hasFiniteSupport\n  apply (Set.finite_singleton ρ₀).subset\n  intro ρ hρ\n  simp only [Function.mem_support, ne_eq] at hρ\n  by_contra h\n  apply hρ\n  simp [h]  -- ρ = ρ₀? h : ¬ ρ = ρ₀... wait: support membership: f ρ ≠ 0; want ρ ∈ {ρ₀}: by_contra h : ρ ∉ {ρ₀} i.e. ρ ≠ ρ₀ (Set.mem_singleton_iff): then if_neg: f ρ = 0 contra.\n```\nHmm: goal after intro ρ hρ: ρ ∈ {ρ₀} (singleton set membership = ρ = ρ₀?). {ρ₀} as Set of the subtype: membership ρ ∈ ({ρ₀} : Set _) ↔ ρ = ρ₀ via Set.mem_singleton_iff — is it defeq? Set.singleton membership: ρ ∈ {ρ₀} is ρ = ρ₀ definitionally? `{a} : Set α := insert a ∅`; membership: insert def: x ∈ insert a s ↔ x = a ∨ x ∈ s... not defeq to equality cleanly. Use: `by_contra h; rw [Set.mem_singleton_iff] at h`? Wait direction: goal ρ ∈ {ρ₀}; by_contra h : ¬ ρ ∈ {ρ₀}; then f ρ = 0: if_neg (fun heq => h (Set.mem_singleton_iff.mpr heq))... let me write:\n```lean\n  apply summable_of_hasFiniteSupport ((Set.finite_singleton ρ₀).subset ?_)\n  intro ρ hρ\n  by_contra h\n  rw [Function.mem_support, ne_eq] at hρ\n  apply hρ\n  rw [if_neg (fun he => h (Set.mem_singleton_iff.mpr he))]\n```\nHmm — cleaner pattern from liSummable's hE: they did\n```lean\n    apply summable_of_hasFiniteSupport\n    apply hfin.subset\n    intro ρ hρ\n    simp only [Function.mem_support, ne_eq] at hρ\n    by_contra hball\n    apply hρ\n    ...\n```\nwhere the subset goal was support ⊆ finite-set. So here: subset target: Function.support f ⊆ {ρ₀}: intro ρ hρ (hρ : ρ ∈ support f: f ρ ≠ 0); goal ρ ∈ {ρ₀}: by_contra h; apply hρ; show f ρ = 0: if_neg: needs ρ ≠ ρ₀: from h : ¬ ρ ∈ {ρ₀}: Set.mem_singleton_iff.not...: `fun he => h (Set.mem_singleton_iff.mpr he)` : ρ ≠ ρ₀... wait he : ρ = ρ₀; Set.mem_singleton_iff.mpr he : ρ ∈ {ρ₀} ✓ contra h ✓. Then `simp only [if_neg that]` closes f ρ = 0. ✓.\n\n```lean\n/-- Pointwise split: seriesFun = seriesFunSub + the ρ₀-term (everywhere). -/\nlemma seriesFun_eq_sub_add (ρ₀ : {ρ : ℂ // IsNontrivialZero ρ}) (s : ℂ) :\n    seriesFun s = seriesFunSub ρ₀ s + seriesTerm s ρ₀ := by\n  have h1 : seriesFun s = ∑' ρ, (seriesTermSub ρ₀ s ρ + (if ρ = ρ₀ then seriesTerm s ρ else 0)) := by\n    rw [seriesFun]  -- unfold; then congr via funext\n    congr 1  -- ∑' congr: tsum_congr? funext: use `tsum_congr (f g) (h : ∀ x, f x = g x)`? Hmm — ∑' over dependent: `tsum_congr : (∀ b, f b = g b) → ∑' f = ∑' g` ✓ exists. But seriesFun s := ∑' ρ, seriesTerm s ρ — unfold seriesFun first: `show ∑' ρ, seriesTerm s ρ = _`: then tsum_congr with the pointwise: by_cases simp.\n    ...\n```\nLet me write:\n```lean\n  show ∑' ρ, seriesTerm s ρ = _\n  rw [show seriesFunSub ρ₀ s = ∑' ρ, seriesTermSub ρ₀ s ρ from rfl]\n  rw [← Summable.tsum_add (seriesTermSub_summable ρ₀ s) (single_summable ρ₀ s)]\n  -- goal: ∑' ρ, seriesTerm s ρ = ∑' ρ, (seriesTermSub ρ₀ s ρ + if ...)\n  apply tsum_congr\n  intro ρ\n  by_cases h : ρ = ρ₀ <;> simp [seriesTermSub, h]\n  -- single tsum = seriesTerm s ρ₀: tsum_eq_single\n  rw [tsum_eq_single ρ₀ (fun ρ hρ => if_neg hρ)]  -- hmm: the if: if ρ = ρ₀ then seriesTerm s ρ else 0: for ρ ≠ ρ₀: if_neg hρ : the if = 0 ✓; tsum_eq_single : ∑' b, f b = f a given ∀ b ≠ a, f b = 0. Then f ρ₀ = if ρ₀ = ρ₀ then ... else 0 = if_pos rfl: seriesTerm s ρ₀ ✓ simp.\n```\nOrdering: goal after rw [← Summable.tsum_add]: ∑' seriesTerm s = ∑' ρ, (sub ρ + single ρ)? Careful: `Summable.tsum_add (hf : Summable f) (hg : Summable g) : ∑' x, (f x + g x) = ∑' f + ∑' g`? Actually the name: `Summable.tsum_add : ∑' x, (f x + g x) = ...`. Hmm — in recent Mathlib: `Summable.tsum_add (hf : Summable f) (hg : Summable g) : ∑' x, (f x + g x) = ∑' x, f x + ∑' x, g x`. So ← direction rewrites `∑' sub + ∑' single` to `∑' (sub + single)`. My goal chain:\n\ngoal: seriesFun s = seriesFunSub ρ₀ s + seriesTerm s ρ₀\n⟹ show: ∑' term = ∑' sub + seriesTerm s ρ₀ (unfold seriesFun, seriesFunSub — `show` with both unfolded; seriesFunSub ρ₀ s unfolds to ∑' sub ✓ defeq so `show` accepts)\n⟹ rw [tsum_eq_single ρ₀ h]: rewrites `∑' ρ, if ρ = ρ₀ then seriesTerm s ρ else 0` — but the goal has `seriesTerm s ρ₀` not the single-tsum. Go the other way: first convert: have hsingle : ∑' ρ, (if ρ = ρ₀ then seriesTerm s ρ else 0) = seriesTerm s ρ₀ := tsum_eq_single...: \n```lean\n  have hsingle : ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},\n      (if ρ = ρ₀ then seriesTerm s ρ else (0:ℂ)) = seriesTerm s ρ₀ := by\n    apply tsum_eq_single\n    intro ρ hρ\n    exact if_neg hρ\n    -- after apply tsum_eq_single: remaining goal ∀ b ≠ ρ₀, f b = 0: intro; exact if_neg hρ — wait if_neg : ¬a → (if a then b else c) = c: hρ : ρ ≠ ρ₀ but the condition is ρ = ρ₀: if_neg hρ : (if ρ = ρ₀ then seriesTerm s ρ else 0) = 0 ✓. But tsum_eq_single's f a: after the ∀-goal, remaining: f ρ₀ = seriesTerm s ρ₀?? No: tsum_eq_single ρ₀ h : ∑' f = f ρ₀; the apply unifies ∑' f with the LHS and f ρ₀ with RHS = seriesTerm s ρ₀: f ρ₀ = if ρ₀ = ρ₀ then ... : needs if_pos rfl reduction — apply unification up to defeq should handle (if_pos rfl is defeq ✓)... risky; safer:\n    rw [tsum_eq_single ρ₀ (fun ρ hρ => if_neg hρ)]\n    exact if_pos rfl\n```\ni.e. prove via rw + exact. Fine.\n\nThen:\n```lean\n  calc seriesFun s = ∑' ρ, seriesTerm s ρ := rfl\n    _ = ∑' ρ, (seriesTermSub ρ₀ s ρ + (if ρ = ρ₀ then seriesTerm s ρ else 0)) := by\n        apply tsum_congr\n        intro ρ\n        by_cases h : ρ = ρ₀ <;> simp [seriesTermSub, h]\n    _ = ∑' ρ, seriesTermSub ρ₀ s ρ + ∑' ρ, (if ρ = ρ₀ then seriesTerm s ρ else 0) :=\n        Summable.tsum_add (seriesTermSub_summable ρ₀ s) (single_summable ρ₀ s)\n    _ = seriesFunSub ρ₀ s + seriesTerm s ρ₀ := by rw [hsingle]; rfl\n```\n`tsum_congr`: signature `tsum_congr (h : ∀ b, f b = g b) : ∑' f = ∑' g`? It's `theorem tsum_congr (h : ∀ b, f b = g b) : ∑' b, f b = ∑' b, g b` ✓. The by_cases branches: h : ρ = ρ₀: goal seriesTerm s ρ = seriesTermSub ρ₀ s ρ + (if ρ = ρ₀ then seriesTerm s ρ else 0): simp [seriesTermSub, h]: seriesTermSub → if ρ = ρ₀ then 0 else ... with h: simp [h] reduces both ifs: LHS... the goal becomes seriesTerm s ρ = 0 + seriesTerm s ρ?? simp [h]: `if_pos h`... h : ρ = ρ₀: simp [seriesTermSub, h] rewrites if ρ = ρ₀ via h (simp uses h to decide) ⟹ RHS = 0 + seriesTerm s ρ = seriesTerm s ρ ✓ closes by rfl via simp. Neg branch: h : ¬ρ = ρ₀: RHS = seriesTerm s ρ + 0 ✓. \n\nThe last `_ = seriesFunSub ρ₀ s + seriesTerm s ρ₀`: first summand: ∑' ρ, seriesTermSub ρ₀ s ρ = seriesFunSub ρ₀ s — rfl defeq: `by rw [hsingle]` then goal ∑' sub + seriesTerm s ρ₀ = seriesFunSub ρ₀ s + seriesTerm s ρ₀ — the subs are defeq but not syntactically: rfl closes ✓ (rfl works up to defeq for `exact rfl`? `rfl` tactic: closes a = b if defeq ✓).\n\nHmm — actually to be safe use `show` conversions instead. It'll be fine.\n\nThen:\n```lean\n/-- The series minus its ρ₀-term is analytic at ρ₀. -/\ntheorem seriesFunSub_analyticAt (ρ₀ : {ρ : ℂ // IsNontrivialZero ρ}) :\n    AnalyticAt ℂ (seriesFunSub ρ₀) (ρ₀ : ℂ) := by\n  obtain ⟨δ, hδ, hiso⟩ := nontrivialZero_isolated ρ₀\n  set δ' := δ / 2 with hδ'\n  have hδ'0 : 0 < δ' := half_pos hδ\n  set M : ℝ := ‖(ρ₀ : ℂ)‖ + δ' with hM\n  set u : {ρ : ℂ // IsNontrivialZero ρ} → ℝ := fun ρ =>\n    17 / 6 * M * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ)))) with hu\n  have hsum_u : Summable u := seriesTerm_summable_majorant M\n  have hfu : ∀ᶠ ρ in cofinite, ∀ s ∈ Metric.ball (ρ₀ : ℂ) δ', ‖seriesTermSub ρ₀ s ρ‖ ≤ u ρ := by\n    rw [Filter.eventually_cofinite]\n    apply (finite_subtype_norm_lt (max 2 (2 * M))).subset\n    intro ρ hρ\n    simp only [Set.mem_setOf_eq, not_forall] at hρ\n    -- hρ : ∃ s ∈ ball, ¬ ‖sub‖ ≤ u ρ: get s\n    by_contra hball\n    apply hρ  -- wait direction: I want: if ‖ρ‖ ≥ R₀ then ∀ s ∈ ball, bound. Contrapositive: ¬(∀...) ⟹ ‖ρ‖ < R₀. intro ρ hρ with hρ : ¬ ∀ s ∈ ball...; goal ρ ∈ {ρ | ‖ρ‖ < R₀}: by_contra hball: ‖ρ‖ ≥ R₀; derive ∀ s ∈ ball bound; contra hρ.\n    ...\n```\nLet me structure the contrapositive cleanly:\n```lean\n    apply (finite_subtype_norm_lt (max 2 (2 * M))).subset\n    intro ρ hρ\n    -- hρ : ρ ∈ {ρ | ¬ ∀ s ∈ ball, ‖sub ρ s‖ ≤ u ρ}; goal: ‖ρ‖ < R₀\n    by_contra hlt\n    rw [not_lt] at hlt  -- R₀ ≤ ‖ρ‖\n    apply hρ\n    intro s hs\n    -- s ∈ ball(ρ₀, δ'): ‖s‖ < ‖ρ₀‖ + δ' = M ⟹ 2‖s‖ ≤ 2M ≤ R₀ ≤ ‖ρ‖; 2 ≤ R₀ ≤ ‖ρ‖\n    have hsM : ‖s‖ ≤ M := by\n      have h : ‖s‖ < M := by\n        calc ‖s‖ ≤ ‖s - (ρ₀:ℂ)‖ + ‖(ρ₀:ℂ)‖ := by\n              nth_rewrite 1 [show s = (s - (ρ₀:ℂ)) + (ρ₀:ℂ) from by ring]\n              exact norm_add_le _ _\n          _ < δ' + ‖(ρ₀:ℂ)‖ := by\n              have := Metric.mem_ball.mp hs  -- dist s ρ₀ < δ'\n              rw [dist_eq_norm] at this\n              linarith\n          _ = M := by rw [hM]; ring\n      exact le_of_lt h\n    have h2 : (2:ℝ) ≤ ‖(ρ:ℂ)‖ := (le_max_left _ _).trans hlt\n    have hs2 : 2 * ‖s‖ ≤ ‖(ρ:ℂ)‖ := ((le_max_right _ _) : 2*M ≤ max 2 (2*M)).trans hlt ∘ ... \n```\n2‖s‖ ≤ 2M (from hsM) ≤ R₀ (max_right) ≤ ‖ρ‖ (hlt): `exact (by linarith : 2 * ‖s‖ ≤ max 2 (2*M)).trans hlt`? linarith [hsM, le_max_right 2 (2*M)]... do: have h2M : 2*‖s‖ ≤ 2*M := by linarith; exact (h2M.trans (le_max_right _ _)).trans hlt ✓.\n\nThen:\n```lean\n    by_cases h0 : ρ = ρ₀\n    · simp [seriesTermSub, h0]\n      -- goal ‖0‖ ≤ u ρ₀: norm_zero; positivity of u: (17/6)*M*(mult/(1+γ²)) ≥ 0: M = ‖ρ₀‖+δ' > 0: positivity with haves... positivity can't use hM's nonneg directly: M = ‖ρ₀‖ + δ' ≥ 0 since both ≥ 0: have hM0 : 0 ≤ M := by rw [hM]; positivity (‖·‖ nonneg + hδ'0.le: linarith [norm_nonneg (ρ₀:ℂ), hδ'0]). Then positivity for the product with hM0 in context? positivity doesn't read hypotheses. Use explicit: mul_nonneg (mul_nonneg (by norm_num : (0:ℝ) ≤ 17/6) hM0) (div_nonneg (Nat.cast_nonneg _) (by linarith [Complex.normSq_nonneg (gammaOf (ρ:ℂ))]))... \n      -- simpler: simp [seriesTermSub, h0]; positivity?? no. Explicit:\n      rw [seriesTermSub, if_pos h0, norm_zero]\n      have hg0 : (0:ℝ) < 1 + Complex.normSq (gammaOf (ρ:ℂ)) := by\n        have := Complex.normSq_nonneg (gammaOf (ρ:ℂ)); linarith\n      have hM0 : (0:ℝ) ≤ M := by rw [hM]; linarith [norm_nonneg (ρ₀:ℂ), hδ'0.le]\n      exact mul_nonneg (mul_nonneg (by norm_num) hM0)\n        (div_nonneg (Nat.cast_nonneg _) hg0.le)\n    · rw [seriesTermSub, if_neg h0]\n      exact (seriesTerm_norm_le ρ h2 hs2).trans (by\n        -- 17/6‖s‖mult/(1+γ²) ≤ 17/6 M mult/(1+γ²)\n        have hg0 : (0:ℝ) ≤ (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ:ℂ))) := by\n          have := Complex.normSq_nonneg (gammaOf (ρ:ℂ))\n          positivity  -- hmm positivity: (mult:ℝ)/(1+γ²): mult cast nonneg ✓, 1+γ² > 0 needs normSq_nonneg — positivity knows normSq_nonneg? It's a lemma not marked... positivity extension for Complex.normSq? Unsure. Safer: div_nonneg (Nat.cast_nonneg _) (by linarith [Complex.normSq_nonneg _]).\n        exact mul_le_mul_of_nonneg_right (by nlinarith [hsM, norm_nonneg s] : 17/6*‖s‖ ≤ 17/6*M) hg0)\n```\nWait — but u ρ is DEFINED as 17/6 * M * (mult/(1+γ²)) via `set` — the goal after `rw [seriesTermSub, if_neg h0]` is ‖seriesTerm s ρ‖ ≤ u ρ; with set, u ρ is displayed as the lambda applied: u ρ — set introduces u := fun ρ => ... and replaces occurrences; u ρ is a beta-redex?? `set ... := fun ρ => body` then `u ρ` — Lean keeps u as a local def; u ρ beta-reduces to body[ρ] — defeq but not syntactic. The goal `‖seriesTerm s ρ‖ ≤ u ρ`: my `.trans` target: 17/6*M*(...) ≤ u ρ — I must provide the proof term of type ... ≤ u ρ; my calc gives ... ≤ 17/6*M*(...) which is defeq to u ρ: `exact` accepts defeq ✓. But when I write the bound inline `(by ... : 17/6*‖s‖ ≤ 17/6*M)` fine.\n\nHmm — wait, `set u : ... → ℝ := fun ρ => ...` — then occurrences of `fun ρ => 17/6*M*(...)` get folded to u. The application u ρ doesn't auto-unfold in the goal display but defeq holds ✓ exact works.\n\nAlso — `hs` : s ∈ Metric.ball (ρ₀:ℂ) δ'. Metric.mem_ball.mp hs : dist s ρ₀ < δ' ✓.\n\nThen the uniform-convergence + differentiability on ball(ρ₀, δ'):\n```lean\n  have hu' : HasSumUniformlyOn (fun ρ => fun s : ℂ => seriesTermSub ρ₀ s ρ)\n      (fun s => ∑' ρ, seriesTermSub ρ₀ s ρ) (Metric.ball (ρ₀ : ℂ) δ') :=\n    HasSumUniformlyOn.of_norm_le_summable_eventually hsum_u hfu\n  have htend := TendstoUniformlyOn.tendstoLocallyUniformlyOn\n    (hasSumUniformlyOn_iff_tendstoUniformlyOn.mp hu')\n  have hdiff : DifferentiableOn ℂ (fun s => ∑' ρ, seriesTermSub ρ₀ s ρ)\n      (Metric.ball (ρ₀ : ℂ) δ') := by\n    apply htend.differentiableOn _ isOpen_ball\n    apply Filter.Eventually.of_forall\n    intro t s hs\n    rw [show (fun s => ∑ ρ ∈ t, seriesTermSub ρ₀ s ρ)\n        = ∑ ρ ∈ t, (fun s => seriesTermSub ρ₀ s ρ) from by\n      funext s; simp [Finset.sum_apply]]\n    apply DifferentiableAt.differentiableWithinAt\n    apply DifferentiableAt.sum\n    intro ρ hρt\n    by_cases h0 : ρ = ρ₀\n    · show DifferentiableAt ℂ (fun s => if ρ = ρ₀ then (0:ℂ) else seriesTerm s ρ) s\n      rw [if_pos h0]\n      exact differentiableAt_const 0\n    · have hsρ : s - (ρ : ℂ) ≠ 0 := by\n        have hle : δ ≤ ‖(ρ : ℂ) - (ρ₀ : ℂ)‖ := hiso ρ h0\n        have hlt : ‖s - (ρ₀ : ℂ)‖ < δ' := by\n          have := Metric.mem_ball.mp hs\n          rw [dist_eq_norm] at this\n          exact this\n        intro hzero\n        -- ‖ρ − ρ₀‖ ≤ ‖ρ − s‖ + ‖s − ρ₀‖ < 0 + δ' = δ/2 < δ contra\n        have h1 : ‖(ρ : ℂ) - (ρ₀ : ℂ)‖ ≤ ‖(ρ : ℂ) - s‖ + ‖s - (ρ₀ : ℂ)‖ := by\n          nth_rewrite 1 [show (ρ:ℂ) - (ρ₀:ℂ) = ((ρ:ℂ) - s) + (s - (ρ₀:ℂ)) from by ring]\n          exact norm_add_le _ _\n        have h2 : ‖(ρ : ℂ) - s‖ = 0 := by\n          have : s = (ρ:ℂ) := sub_eq_zero.mp hzero\n          rw [← this, sub_self, norm_zero]\n        rw [h2] at h1\n        linarith [hle, hlt, hδ'0]  -- δ ≤ 0 + δ' = δ/2 ⟹ δ ≤ δ/2 contra δ > 0\n      have hρ0 : (ρ : ℂ) ≠ 0 := by\n        intro h\n        have := ρ.2.2.1\n        rw [h] at this\n        simp at this\n      show DifferentiableAt ℂ (fun s => if ρ = ρ₀ then (0:ℂ) else seriesTerm s ρ) s\n      rw [if_neg h0]\n      show DifferentiableAt ℂ (fun s => (zeroMult ρ : ℂ) * (1 / (s - (ρ:ℂ)) + 1 / (ρ:ℂ))) s\n      exact (((differentiableAt_const (1:ℂ)).div (differentiableAt_id.sub (differentiableAt_const _)) hsρ).add (differentiableAt_const _)).const_mul _\n  have han := hdiff.analyticOnNhd isOpen_ball\n  exact han (ρ₀:ℂ) (Metric.mem_ball_self hδ'0)\n```\nWait the final: goal AnalyticAt ℂ (seriesFunSub ρ₀) (ρ₀:ℂ); han : AnalyticOnNhd ℂ (fun s => ∑' ρ, seriesTermSub ρ₀ s ρ) (ball...) — defeq to seriesFunSub ρ₀ ✓; han (ρ₀:ℂ) (mem_ball_self) : AnalyticAt ℂ (fun s => ...) (ρ₀:ℂ) — exact defeq ✓.\n\nhmm hδ'0 in the last linarith: δ ≤ δ/2 with δ > 0: linarith [hle, hlt, hδ] where hδ : 0 < δ: from h1 (with h2 rw'd): ‖ρ−ρ₀‖ ≤ 0 + ‖s−ρ₀‖ — rw [h2] at h1 gives ‖ρ−ρ₀‖ ≤ 0 + ‖s−ρ₀‖... zero_add not auto: linarith handles: ‖ρ−ρ₀‖ ≤ 0 + ‖s−ρ₀‖, ‖s−ρ₀‖ < δ' = δ/2, hle: δ ≤ ‖ρ−ρ₀‖ ⟹ δ < δ/2 ⟹ δ ≤ 0 contra hδ : 0 < δ — but hδ' = δ/2 defeq: δ' is a set-variable: hlt : ‖s−ρ₀‖ < δ' where δ' := δ/2 — linarith sees δ' opaque! Need hδ' : δ' = δ/2 in the linarith list. set ... with hδ' gives hδ' : δ' = δ/2 ✓ include it: linarith [hle, hlt, hδ, hδ'] — wait `set δ' := δ/2 with hδ'` : hδ' : δ' = δ/2 ✓.\n\nAlso hlt could just reuse hs directly: Metric.mem_ball.mp hs : dist s ρ₀ < δ' ✓ dist_eq_norm ✓.\n\nThen the final assembly:\n```lean\n/-- The series with its ρ₀-term subtracted equals the reduced series\n(everywhere); hence the polar subtraction is analytic at ρ₀. -/\ntheorem seriesFun_sub_term (ρ₀ : {ρ : ℂ // IsNontrivialZero ρ}) (s : ℂ) :\n    seriesFun s - seriesTerm s ρ₀ = seriesFunSub ρ₀ s := by\n  have h := seriesFun_eq_sub_add ρ₀ s\n  linarith?? — ℂ not ordered: use: rw [h]; ring  -- h : seriesFun s = seriesFunSub ρ₀ s + seriesTerm s ρ₀: goal seriesFun s − seriesTerm s ρ₀ = seriesFunSub ρ₀ s: rw [h]: (a + b) − b = a: ring ✓\n  -- actually: conv? `rw [h]; ring` — ring on (x + y) − y = x ✓\n```\nHmm — ring works for ℂ equalities ✓.\n\n```lean\ntheorem seriesFun_sub_self_term_analyticAt (ρ₀ : {ρ : ℂ // IsNontrivialZero ρ}) :\n    AnalyticAt ℂ (fun s => seriesFun s - seriesTerm s ρ₀) (ρ₀ : ℂ) := by\n  apply AnalyticAt.congr (seriesFunSub_analyticAt ρ₀)\n  filter_upwards with s  -- EventualEq: ∀ᶠ s in 𝓝 ρ₀, seriesFunSub ρ₀ s = seriesFun s − seriesTerm s ρ₀ — pointwise true!\n  exact (seriesFun_sub_term ρ₀ s).symm\n```\nAnalyticAt.congr (hf : AnalyticAt f x) (hg : f =ᶠ[𝓝 x] g) : AnalyticAt g x — so hf = seriesFunSub_analyticAt (f = seriesFunSub ρ₀), g = fun s => seriesFun s − seriesTerm s ρ₀; need seriesFunSub ρ₀ =ᶠ[𝓝 ρ₀] g: Filter.Eventually.of_forall (fun s => (seriesFun_sub_term ρ₀ s).symm) ✓.\n\n```lean\n/-- The polar subtraction form consumed by 5e-iv: s ↦ seriesFun s −\nmult(ρ₀)/(s−ρ₀) is analytic at ρ₀. -/\ntheorem seriesFun_sub_polar_analyticAt (ρ₀ : {ρ : ℂ // IsNontrivialZero ρ}) :\n    AnalyticAt ℂ (fun s => seriesFun s - (zeroMult (ρ₀:ℂ) : ℂ) / (s - (ρ₀:ℂ))) (ρ₀:ℂ) := by\n  have h := seriesFun_sub_self_term_analyticAt ρ₀\n  have heq : (fun s => seriesFun s - (zeroMult (ρ₀:ℂ) : ℂ) / (s - (ρ₀:ℂ)))\n      = (fun s => (seriesFun s - seriesTerm s ρ₀) + (zeroMult (ρ₀:ℂ) : ℂ) / (ρ₀:ℂ)) := by\n    funext s\n    rw [seriesTerm]\n    ring\n  rw [heq]\n  exact h.add (differentiableAt_const _).analyticAt\n```\nCheck: seriesTerm s ρ₀ = mult·(1/(s−ρ₀) + 1/ρ₀) = mult/(s−ρ₀) + mult/ρ₀ — as ℂ expressions with div: mult*(1/(s−ρ₀) + 1/ρ₀) = mult/(s−ρ₀) + mult/ρ₀: ring? ring normalizes a/b to a*b⁻¹ ✓ and distributes ✓ (no field_simp needed since no cancellations of inverses). Goal after funext s, rw [seriesTerm]: seriesFun s − mult/(s−ρ₀) = (seriesFun s − mult*(1/(s−ρ₀)+1/ρ₀)) + mult/ρ₀: ring ✓.\n\n`DifferentiableAt.analyticAt` — BANKED GOTCHA (session 026): DifferentiableAt.analyticAt does NOT exist! Use: for a constant function: `(differentiableAt_const _).analyticAt` invalid. AnalyticAt of const: `analyticAt_const : AnalyticAt 𝕜 (fun _ => c) x` ✓ exists (I believe). Use analyticAt_const.\n\nLet me double-check `analyticAt_const` exists in this Mathlib — Analytic/Basic.lean: `theorem analyticAt_const : AnalyticAt 𝕜 (fun _ => c) x` ✓ standard.\n\nAlso `(zeroMult (ρ₀:ℂ) : ℂ)` — zeroMult applied to (ρ₀ : ℂ) then cast ℕ→ℂ. In liSummand they wrote `(zeroMult ρ : ℂ)` with ρ : subtype — Lean coerces ρ to ℂ for zeroMult ✓ same here; but to be safe write `(zeroMult (ρ₀ : ℂ) : ℂ)`. Hmm — in seriesTerm the coercion is already there; for consistency in heq rewrite: seriesTerm s ρ₀ = (zeroMult ↑ρ₀ : ℂ) * (...): rw [seriesTerm] exposes the def with (zeroMult ↑ρ₀ : ℂ) — hmm the def is `(zeroMult ρ : ℂ)` with ρ the subtype var — instantiated at ρ₀: `(zeroMult ↑ρ₀ : ℂ)`? zeroMult's argument: ρ₀ coerced: `zeroMult ↑ρ₀`. Fine — ring handles regardless of the exact form ✓.\n\nAlso for §4's `seriesFun_analyticOnNhd`: AnalyticOnNhd ℂ seriesFun {s | ¬ IsNontrivialZero s} = ∀ x ∈ s, AnalyticAt: `fun s₀ hs₀ => seriesFun_analyticAt hs₀` — hs₀ : s₀ ∈ {s | ¬ ...} = ¬ IsNontrivialZero s₀ (defeq set membership ✓).\n\nNow — remaining risk points:\n1. `Filter.eventually_cofinite` name/direction. Check: Mathlib Order/Filter/Cofinite.lean: `theorem eventually_cofinite {p : α → Prop} : (∀ᶠ x in cofinite, p x) ↔ {x | ¬p x}.Finite`? Let me verify.\n2. `HasSumUniformlyOn.of_norm_le_summable_eventually` hfu form: ∀ᶠ n in cofinite, ∀ x ∈ s, ‖f n x‖ ≤ u n — matches ✓ (from the source above).\n3. `Metric.eventually_nhds_iff_ball` ✓ verified.\n4. `analyticAt_riemannZeta` — Mathlib: `analyticAt_riemannZeta {s : ℂ} (hs : s ≠ 1) : AnalyticAt ℂ riemannZeta s`? Used in LiSides line 370: `analyticAt_riemannZeta hρ` with hρ : ρ ≠ 1 ✓.\n5. `ContinuousAt.eventually_ne` ✓ (used in LiResidue line 82).\n6. `AnalyticAt.continuousAt` ✓ used LiResidue 82.\n7. `(analyticAt_riemannZeta h1).analyticOrderAt_ne_top.mp` ✓ LiSides pattern.\n8. `smul_eq_mul` ✓.\n9. In §4 partial sums: `DifferentiableAt.sum` — signature: `(h : ∀ i ∈ t, DifferentiableAt ...)`? LiDigamma: `apply DifferentiableAt.sum; intro m hm` ✓.\n10. `htend.differentiableOn _ isOpen_ball` ✓ pattern from LiDigamma (`htend.differentiableOn _ dpsiDomain_isOpen`).\n11. `hdiff.analyticOnNhd isOpen_ball` ✓.\n12. `Metric.mem_ball_self : 0 < r → x ∈ ball x r` ✓.\n13. `Finset.min'_le`, `Finset.min'_mem` ✓ standard.\n14. `Set.finite_singleton` ✓; `summable_of_hasFiniteSupport` ✓.\n15. `tsum_congr` ✓.\n16. `half_pos` ✓.\n17. `abs_norm_sub_norm_le : |‖a‖ − ‖b‖| ≤ ‖a − b‖` — check name: Mathlib `abs_norm_sub_norm_le : |‖x‖ − ‖y‖| ≤ ‖x − y‖` ✓ exists (norm_sub_le_norm... no). Actually the name is `abs_norm_sub_norm_le` ✓ I'm fairly confident.\n\nLet me verify #1 and #17 and `tsum_congr`, `analyticAt_const`, `DifferentiableAt.sum`, `Finset.min'_le`, `Complex.norm_natCast`/`RCLike.norm_natCast` quickly.","signature":""},{"type":"text","text":"Now verifying the remaining lemma names in one sweep."},{"type":"tool_use","id":"Bash_37","name":"Bash","input":{"command":"cd D:/Python/Quantum/zeta-23-lean/.lake/packages/mathlib && grep -rn \"theorem eventually_cofinite\\b\" Mathlib/Order/Filter/Cofinite.lean | head -2; grep -rn \"theorem abs_norm_sub_norm_le\\b\\|lemma abs_norm_sub_norm_le\\b\" Mathlib/Analysis/ -r | head -2; grep -rn \"theorem tsum_congr\\b\\|lemma tsum_congr\\b\" Mathlib/Topology/Algebra/InfiniteSum/Basic.lean | head -2; grep -rn \"theorem analyticAt_const\\b\" Mathlib/Analysis/Analytic/Basic.lean | head -2; grep -rn \"theorem DifferentiableAt.sum\\b\\|lemma DifferentiableAt.sum\\b\" Mathlib/ -r | head -2; grep -rn \"theorem half_pos\\b\" Mathlib/Algebra/Order/ -r | head -2; grep -rn \"theorem Summable.tsum_add\\b\" Mathlib/ -r | head -2; grep -rn \"theorem Summable.norm\\b\" Mathlib/ -r | head -2; grep -rn \"theorem Metric.ball_subset_ball\\b\" Mathlib/ -r | head -2","description":"Verify lemma names batch"},"extra_content":null}]