[{"type":"thinking","thinking":"The ContDiffAt pattern: AnalyticAt → .contDiffAt. For my zpow term: AnalyticAt (fun t => (t + c)^{−1})? Via analyticAt_const.div (analyticAt_id.add analyticAt_const) hs — for (t+c)^{(−1:ℤ)} — write as 1/(t+c): the zpow_neg_one conversion. So:\n\n```lean\n  have hF1 : ContDiffAt ℂ j (fun t : ℂ => (t + -(ρ : ℂ)) ^ (-1 : ℤ)) s := by\n    have h2 : AnalyticAt ℂ (fun t : ℂ => t + -(ρ : ℂ)) s := analyticAt_id.add analyticAt_const\n    have h3 : AnalyticAt ℂ (fun t : ℂ => 1 / (t + -(ρ : ℂ))) s := analyticAt_const.div h2 hs'\n    have e : (fun t : ℂ => (t + -(ρ : ℂ)) ^ (-1 : ℤ)) = fun t => 1 / (t + -(ρ : ℂ)) := by\n      funext t\n      rw [zpow_neg_one, one_div]\n    rw [e]\n    exact h3.contDiffAt\n```\nHmm — wait, zpow_neg_one : a^{−1} = a⁻¹; one_div : 1/a = a⁻¹: so (t+c)^{−1} = (t+c)⁻¹ = 1/(t+c): rw [zpow_neg_one] gives (t+c)⁻¹; goal RHS 1/(t+c): one_div says 1/(t+c) = (t+c)⁻¹: after rw [zpow_neg_one] the goal is (t+c)⁻¹ = 1/(t+c) — close by rw [one_div] (turns RHS into ⁻¹ ✓) or rfl (1/a and a⁻¹ are defeq — HDiv.hDiv 1 a vs Inv.inv a — not syntactically equal but defeq via one_div? they're NOT defeq — 1/a = 1 * a⁻¹? no: instDiv: a/b = a * b⁻¹: so 1/a = 1 * a⁻¹ — defeq to a⁻¹ by one_mul ✓ rfl-check might work; the rw [zpow_neg_one, one_div] makes both sides a⁻¹ ✓ safe).\n\nNow §5 main lemma — the M-test on ball(0, δ/2). The SummableLocallyUniformlyOn_of_locally_bounded signature from LiDigamma:720-722: \n```lean\n  apply SummableLocallyUniformlyOn_of_locally_bounded dpsiDomain_isOpen\n  intro K hK hKc\n  refine ⟨bound, summable_bound, fun m s hs => ?_⟩\n```\nwhere hK : K ⊆ domain, hKc : IsCompact K, hs : s ∈ K. So it wants: for every compact K ⊆ u, a summable bound valid on K. My domain u := Metric.ball 0 (δ/2); K ⊆ u ⟹ ∀ s ∈ K, ‖s‖ < δ/2.\n\nThe bound family for the j-th derivative family: u_j ρ := mult·j!·2^{j+1}·δ^{1−j}·... — wait it must be a REAL summable family: u_j ρ := (j ! : ℝ) * 2^{j+1} * δ^{1-j}?? δ^{1−j} with j ≥ 1 — δ < 1 maybe; δ^{1−j} = δ^{-(j−1)}: as (1/δ)^{j−1}. Let me define: u ρ := ((j ! : ℝ) * 2 ^ (j + 1) * (1 / δ) ^ (j - 1)) * ((zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ 2)? — from my earlier estimate: term ≤ mult·j!·2^{j+1}·‖ρ‖^{−2}·δ^{1−j} where δ^{1−j} = (1/δ)^{j−1} ✓ (j ≥ 1). So C_j := j!·2^{j+1}·(1/δ)^{j−1}, u ρ := C_j·(mult/‖ρ‖²) — summable via summable_mult_div_norm_sq.mul_left ✓.\n\nPer-term bound for s ∈ K:\n‖iteratedDerivWithin j (seriesTerm · ρ) u s‖ = ‖iteratedDeriv j (seriesTerm · ρ) s‖ (Within_of_isOpen isOpen_ball (hK hs)) = ‖mult·(−1)^j j! (s−ρ)^{−j−1}‖ = mult·j!·‖s−ρ‖^{−(j+1)} [norm computations] ≤ mult·j!·2^{j+1}·‖ρ‖^{−(j+1)} [‖s−ρ‖ ≥ ‖ρ‖/2] ≤ mult·j!·2^{j+1}·‖ρ‖^{−2}·(1/δ)^{j−1} [‖ρ‖^{−(j−1)} ≤ (1/δ)^{j−1}... wait: ‖ρ‖^{−(j+1)} = ‖ρ‖^{−2}·‖ρ‖^{−(j−1)} ≤ ‖ρ‖^{−2}·δ^{−(j−1)} ✓ since ‖ρ‖ ≥ δ].\n\nNorm of the closed form: ‖mult·(−1)^j·j!·(s−ρ)^{−j−1}‖ = mult·1·j!·‖s−ρ‖^{−(j+1)}: norm_mul chain: ‖(−1:ℂ)^j‖ = 1 (the LiDigamma:736-738 hsign pattern ✓); RCLike.norm_natCast for j!; norm_zpow + the exponent rewrite (−(j:ℤ)−1 = −((j+1:ℕ):ℤ), zpow_neg, zpow_natCast) → ‖s−ρ‖^{j+1}⁻¹ (the LiDigamma:740 pattern ✓ exactly clone).\n\nThe steps:\n```lean\nlemma seriesTerm_deriv_summableLocallyUniformlyOn (j : ℕ) (hj : 1 ≤ j)\n    {δ : ℝ} (hδ : 0 < δ) (hball : ∀ ρ : {ρ : ℂ // IsNontrivialZero ρ}, (ρ : ℂ) ∉ Metric.ball 0 δ) :\n    SummableLocallyUniformlyOn\n      (fun ρ => iteratedDerivWithin j (fun s => seriesTerm s ρ) (Metric.ball 0 (δ / 2)))\n      (Metric.ball 0 (δ / 2)) := by\n  apply SummableLocallyUniformlyOn_of_locally_bounded isOpen_ball\n  intro K hK hKc\n  set C : ℝ := (j ! : ℝ) * 2 ^ (j + 1) * (1 / δ) ^ (j - 1) with hC\n  refine ⟨fun ρ => C * ((zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ 2),\n    summable_mult_div_norm_sq.mul_left C, fun ρ s hs => ?_⟩\n  have hsu : s ∈ Metric.ball (0 : ℂ) (δ / 2) := hK hs\n  have hsnorm : ‖s‖ < δ / 2 := by\n    rw [Metric.mem_ball, dist_zero_right] at hsu\n    exact hsu\n  have hρδ : δ ≤ ‖(ρ : ℂ)‖ := by\n    by_contra h\n    exact hball ρ (by rw [Metric.mem_ball, dist_zero_right]; exact lt_of_not_ge h)\n  have hρpos : (0 : ℝ) < ‖(ρ : ℂ)‖ := lt_of_lt_of_le hδ hρδ\n  have hsρ : s - (ρ : ℂ) ≠ 0 := by\n    intro h\n    rw [h] at hsnorm?? hmm: s = ρ ⟹ ‖ρ‖ < δ/2 contradicts δ ≤ ‖ρ‖:\n    have : (ρ:ℂ) = s := sub_eq_zero.mp h ▸ ... \n    -- s − ρ = 0 ⟹ s = ρ: sub_eq_zero.mp h : s = ρ\n    rw [sub_eq_zero.mp h] at hsnorm\n    linarith [hρδ, hsnorm]\n  rw [iteratedDerivWithin_of_isOpen isOpen_ball hsu, iteratedDeriv_seriesTerm j hj ρ hsρ]\n  -- norm of the closed form\n  rw [norm_mul, norm_mul]\n  have hsign : ‖(-1 : ℂ) ^ j‖ = 1 := by\n    have h7 : ‖((-1 : ℂ))‖ = 1 := by rw [norm_neg, norm_one]\n    rw [norm_pow, h7, one_pow]\n  rw [RCLike.norm_natCast, hsign, one_mul, norm_zpow]\n  rw [show (-(j : ℤ) - 1 : ℤ) = -(((j + 1 : ℕ) : ℤ)) by push_cast; ring, zpow_neg, zpow_natCast]\n  -- goal: mult * (j! * (‖s−ρ‖^{j+1})⁻¹) ≤ C * (mult/‖ρ‖²)\n  have hnormsρ : ‖(ρ : ℂ)‖ / 2 ≤ ‖s - (ρ : ℂ)‖ := by\n    have h1 : ‖(ρ : ℂ)‖ - ‖s‖ ≤ ‖s - (ρ : ℂ)‖ := by\n      have := norm_sub_norm_le (ρ : ℂ) s  -- ‖ρ‖ − ‖s‖ ≤ ‖ρ − s‖\n      rw [norm_sub_rev] at this?? — norm_sub_rev : ‖a − b‖ = ‖b − a‖\n      ...\n    have h2 : ‖(ρ : ℂ)‖ / 2 ≤ ‖(ρ : ℂ)‖ - ‖s‖ := by\n      have : ‖s‖ ≤ ‖(ρ : ℂ)‖ / 2 := by linarith [hsnorm, hρδ]\n      linarith [norm_nonneg s]\n    exact h2.trans h1\n  -- assemble\n  have hfact : (1 : ℝ) ≤ j ! := Nat.one_le_cast.mpr (Nat.one_le_iff_ne_zero.mpr (Nat.factorial_ne_zero j))?? \n    -- for absorbing: mult·j!·(‖s−ρ‖^{j+1})⁻¹ ≤ mult·j!·(‖ρ‖/2)^{j+1}⁻¹·...\n  calc (zeroMult ρ : ℝ) * ((j ! : ℝ) * (‖s - (ρ : ℂ)‖ ^ (j + 1))⁻¹)\n      ≤ (zeroMult ρ : ℝ) * ((j ! : ℝ) * ((‖(ρ : ℂ)‖ / 2) ^ (j + 1))⁻¹) := by\n        apply mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _)\n        apply mul_le_mul_of_nonneg_left _ (by positivity : (0:ℝ) ≤ (j ! : ℝ))\n        exact inv_le_inv₀ (pow_pos (by positivity... ) ...) hmm inv direction: ‖s−ρ‖ ≥ ‖ρ‖/2 ⟹ (‖s−ρ‖^{j+1})⁻¹ ≤ ((‖ρ‖/2)^{j+1})⁻¹: `inv_le_inv₀ (ha : 0 < a) (hab : a ≤ b) : b⁻¹ ≤ a⁻¹`? signature: inv_le_inv₀ : 0 < a → a ≤ b → b⁻¹ ≤ a⁻¹ ✓ I think. With a = (‖ρ‖/2)^{j+1}, b = ‖s−ρ‖^{j+1}: pow_le_pow_left₀ (by linarith : 0 ≤ ‖ρ‖/2) hnormsρ (j+1) : a ≤ b ✓; pow_pos (by linarith : 0 < ‖ρ‖/2) : 0 < a ✓.\n    _ = (zeroMult ρ : ℝ) * ((j ! : ℝ) * (2 / ‖(ρ : ℂ)‖) ^ (j + 1)) := by\n        rw [div_pow, inv_div??] — ((‖ρ‖/2)^{j+1})⁻¹ = (2/‖ρ‖)^{j+1}: inv_div: (a/b)⁻¹ = b/a: ((‖ρ‖/2)^{j+1})⁻¹ = ((‖ρ‖/2)⁻¹)^{j+1} (inv_pow) = (2/‖ρ‖)^{j+1} (inv_div : (a/b)⁻¹ = b/a ✓). rw [inv_pow, inv_div]\n    _ ≤ (zeroMult ρ : ℝ) * ((j ! : ℝ) * ((2 ^ (j + 1)) * ((1 / δ) ^ (j - 1)) * (1 / ‖(ρ : ℂ)‖ ^ 2))) := by\n        apply mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _)\n        apply mul_le_mul_of_nonneg_left _ (by positivity)\n        -- (2/‖ρ‖)^{j+1} = 2^{j+1}/‖ρ‖^{j+1} = 2^{j+1}·(1/‖ρ‖²)·(1/‖ρ‖^{j−1}) ≤ 2^{j+1}·(1/‖ρ‖²)·(1/δ)^{j−1}\n        rw [div_pow]\n        rw [show (2 : ℝ) ^ (j + 1) / ‖(ρ : ℂ)‖ ^ (j + 1) =\n            2 ^ (j + 1) * (1 / ‖(ρ : ℂ)‖ ^ 2) * (1 / ‖(ρ : ℂ)‖ ^ (j - 1)) by\n          rw [one_div_mul_one_div?? ...] — algebra: 1/‖ρ‖^{j+1} = (1/‖ρ‖²)(1/‖ρ‖^{j−1}): pow: ‖ρ‖^{j+1} = ‖ρ‖²·‖ρ‖^{j−1}: pow: j+1 = 2+(j−1) (j ≥ 1: Nat... careful: j − 1 for j : ℕ, j ≥ 1: j − 1 + 2 = j + 1 ✓ omega. rw [← pow_add]; congr: omega]\n        apply mul_le_mul_of_nonneg_left _ (by positivity : (0:ℝ) ≤ 2^(j+1))\n        apply mul_le_mul_of_nonneg_left _ (by positivity)\n        exact one_div_le_one_div_of_le (pow_pos hδ (j-1)) (pow_le_pow_left₀ hδ.le hρδ (j-1))\n    _ = C * ((zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ 2) := by\n        rw [hC]\n        ring\n```\nThe last ring: C·(mult/‖ρ‖²) = j!·2^{j+1}·(1/δ)^{j−1}·mult/‖ρ‖² vs mult·(j!·(2^{j+1}·((1/δ)^{j−1}·(1/‖ρ‖²)))) — ring ✓ (division forms: ·(1/‖ρ‖²) vs /‖ρ‖² — ring handles).\n\npow: j+1 = 2+(j−1): `have : j + 1 = 2 + (j - 1) := by omega` then rw [← pow_add, this]. ✓\n\nWait — one_detail: the goal after the Within/global/zpow rewrites: the term form. iteratedDeriv_seriesTerm gives: mult·((−1)^j·j!·(s−ρ)^{−j−1}) — after norm_mul ×2: ‖mult‖·‖(−1)^j‖·‖j!‖·‖(s−ρ)^{−j−1}‖ — hmm the bracket is ((−1)^j * j! * (s−ρ)^z): norm_mul twice: ‖(−1)^j‖·‖j!·(s−ρ)^z‖ → then need another norm_mul for j!·(s−ρ)^z. LiDigamma did: rw [norm_mul, norm_mul] on mult·((−1)^k·k!·z) — the outer split: mult · (X) and X = (−1)^k · (k! · z)?: their closed form: -((-1))^k * k! * z parses as ((−(−1)^k)·k!)·z: norm_mul, norm_mul: ‖−(−1)^k‖·‖k!·z‖ → ‖−(−1)^k‖·(‖k!‖·‖z‖)?? norm_mul on ‖k!·z‖... they did rw [norm_mul, norm_mul] then hsign rw then one_mul, RCLike.norm_natCast, norm_zpow — sequence at 735-739: `rw [norm_mul, norm_mul]; rw [hsign, one_mul, RCLike.norm_natCast, norm_zpow]` — so after two norm_mul: ‖−(−1)^k‖ · (‖↑k!‖ · ‖z‖)?? — norm_mul twice: ‖a·b·c‖ = ‖a‖·‖b·c‖ = ‖a‖·(‖b‖·‖c‖) ✓. Their a = −(−1)^k (hsign: ‖−(−1)^k‖ = 1), b = k! (natCast), c = z. Mine: a = (−1)^j (hsign), b = j!, c = z — and the OUTER mult·(closed form): seriesTerm's value mult·(X): one more norm_mul: total three. My plan wrote rw [norm_mul, norm_mul] — need one more for the outer mult: order: mult·((−1)^j·j!·z): norm_mul → ‖mult‖·‖(−1)^j·j!·z‖; norm_mul → ‖mult‖·(‖(−1)^j‖·‖j!·z‖); norm_mul → ‖mult‖·(‖(−1)^j‖·(‖j!‖·‖z‖)). So THREE norm_mul. Then RCLike.norm_natCast on ‖(zeroMult ρ:ℂ)‖ = mult (ℝ) ✓, hsign, one_mul, RCLike.norm_natCast on j!, norm_zpow on z. Write rw [norm_mul, norm_mul, norm_mul, RCLike.norm_natCast, hsign, one_mul, RCLike.norm_natCast, norm_zpow] — careful RCLike.norm_natCast might rewrite both casts at once (rw rewrites first match only? rw rewrites ALL matches of the first unifier — banked gotcha \"rw first-unifier-only\"... RCLike.norm_natCast : ‖(↑n)‖ = ↑n — two instances (zeroMult and j!): rw rewrites all occurrences matching the first found pattern... first unifier: probably zeroMult; need it twice for j!. Use simp only [RCLike.norm_natCast] to rewrite all ✓ or rw twice.\n\nThen the show-exponent rewrite + zpow_neg + zpow_natCast (clone LiDigamma:740) → c-part becomes (‖s−ρ‖^{j+1})⁻¹. Goal: mult·(1·(j!·(‖s−ρ‖^{j+1})⁻¹)) ≤ C·(mult/‖ρ‖²) — after one_mul. Then the calc. In the calc I assumed the goal form mult·(j!·(‖s−ρ‖^{j+1})⁻¹) ≤ ... — write the calc's first line to match (with 1· removed — include `one_mul` to clean).\n\nnorm_sub_norm_le: ‖a‖ − ‖b‖ ≤ ‖a − b‖: `norm_sub_norm_le (a b) : ‖a‖ - ‖b‖ ≤ ‖a - b‖` ✓ exists. With norm_sub_rev : ‖a − b‖ = ‖b − a‖ ✓. So ‖ρ‖ − ‖s‖ ≤ ‖ρ − s‖ = ‖s − ρ‖ ✓.\n\ninv_le_inv₀ signature: `inv_le_inv₀ (ha : 0 < a) (h : a ≤ b) : b⁻¹ ≤ a⁻¹` — hmm in current Mathlib: inv_le_inv₀ : a ≤ b → 0 < a → b⁻¹ ≤ a⁻¹?? arg order uncertain. Alternative: `one_div_le_one_div_of_le (ha : 0 < a) (h : a ≤ b) : 1/b ≤ 1/a` ✓ (session-033 confirmed \"one_div_le_one_div_of_le takes the small side's positivity first\" ✓). Use that with 1/x forms instead of ⁻¹ — the zpow_neg gives (‖s−ρ‖^{j+1})⁻¹ — convert ⁻¹ to 1/x: `inv_eq_one_div : a⁻¹ = 1/a` ✓. rw [inv_eq_one_div] then one_div_le_one_div_of_le.\n\nHmm wait — actually simpler: skip the inv form: from the calc, rewrite ((‖ρ‖/2)^{j+1})⁻¹ → 1/(‖ρ‖/2)^{j+1}, use one_div_le_one_div_of_le directly. And ((‖ρ‖/2)^{j+1}) → (2/‖ρ‖)^{j+1}: one_div_div: 1/(a/b) = b/a: (‖ρ‖/2)^{j+1} = ‖ρ‖^{j+1}/2^{j+1}: 1/(that) = 2^{j+1}/‖ρ‖^{j+1} — maybe cleaner to go through: (2/‖ρ‖)^{j+1} = 2^{j+1}/‖ρ‖^{j+1} (div_pow) ✓ as planned.\n\nOK. Then the main termwise lemma:\n\n```lean\nlemma iteratedDeriv_seriesFun_zero (j : ℕ) (hj : 1 ≤ j) :\n    iteratedDeriv j seriesFun 0 =\n      ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, (zeroMult ρ : ℂ) *\n        ((-1 : ℂ) ^ j * (j ! : ℂ) * ((0 : ℂ) - (ρ : ℂ)) ^ (-(j : ℤ) - 1)) := by\n  obtain ⟨δ, hδ, hball⟩ := exists_ball_avoid_nontrivialZeros 0 not_isNontrivialZero_zero\n  have hmem : (0 : ℂ) ∈ Metric.ball (0 : ℂ) (δ / 2) := by\n    rw [Metric.mem_ball, dist_zero_right, norm_zero]\n    exact half_pos hδ\n  have hmain : iteratedDerivWithin j seriesFun (Metric.ball 0 (δ / 2)) 0 =\n      ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},\n        iteratedDerivWithin j (fun s => seriesTerm s ρ) (Metric.ball 0 (δ / 2)) 0 := by\n    rw [iteratedDerivWithin_tsum j isOpen_ball hmem\n      (fun s _ => seriesSummable s)\n      (fun j' hj'1 _ => seriesTerm_deriv_summableLocallyUniformlyOn j' hj'1 hδ hball)\n      ?_]\n    · intro ρ j' r hjm hr\n      -- differentiability side condition, clone LiDigamma:759-785\n      rcases Nat.eq_zero_or_pos j' with hj0 | hj0\n      · subst hj0\n        rw [iteratedDerivWithin_zero]\n        -- seriesTerm differentiable in s at r (r − ρ ≠ 0 since r ∈ ball)\n        have hrρ : r - (ρ : ℂ) ≠ 0 := by\n          intro h\n          have hrn : ‖r‖ < δ / 2 := by\n            rw [Metric.mem_ball, dist_zero_right] at hr\n            exact hr\n          have hρδ : δ ≤ ‖(ρ : ℂ)‖ := by\n            by_contra hc\n            exact hball ρ (by rw [Metric.mem_ball, dist_zero_right]; exact lt_of_not_ge hc)\n          rw [sub_eq_zero.mp h] at hrn\n          linarith\n        rw [seriesTerm]\n        apply DifferentiableAt.const_mul\n        apply DifferentiableAt.add\n        · exact (differentiableAt_const (1 : ℂ)).div (differentiableAt_id.sub differentiableAt_const) hrρ\n        · exact differentiableAt_const _\n      · have h5 : (fun t => iteratedDerivWithin j' (fun z => seriesTerm z ρ) (Metric.ball 0 (δ/2)) t) =ᶠ[𝓝 r]\n            fun t => (zeroMult ρ : ℂ) * ((-1 : ℂ) ^ j' * (j' ! : ℂ) * (t - (ρ : ℂ)) ^ (-(j' : ℤ) - 1)) := by\n          filter_upwards [isOpen_ball.mem_nhds hr] with t ht\n          have htρ : t - (ρ : ℂ) ≠ 0 := ...\n          rw [iteratedDerivWithin_of_isOpen isOpen_ball ht, iteratedDeriv_seriesTerm j' hj0 ρ htρ]\n        apply h5.differentiableAt_iff.mpr\n        -- the closed form is differentiable (zpow, r − ρ ≠ 0)\n        have hrρ : r - (ρ : ℂ) ≠ 0 := ...\n        apply DifferentiableAt.const_mul\n        apply DifferentiableAt.const_mul\n        -- (t−ρ)^{−j'−1} differentiable\n        have h4 : DifferentiableAt ℂ (fun t : ℂ => t - (ρ : ℂ)) r :=\n          differentiableAt_id.sub differentiableAt_const\n        exact ((hasDerivAt_zpow (-(j' : ℤ) - 1) (r - (ρ : ℂ)) (Or.inl hrρ)).differentiableAt).comp r h4\n        -- ↑ but the ∘ defeq bridge needed: ((fun x => x^z) ∘ fun t => t−ρ) = fun t => (t−ρ)^z := rfl\n  -- convert Within → global\n  rw [← iteratedDerivWithin_of_isOpen isOpen_ball hmem]\n  rw [hmain]\n  apply tsum_congr\n  intro ρ\n  have h0ρ : (0 : ℂ) - (ρ : ℂ) ≠ 0 := by\n    intro h\n    have : (ρ:ℂ) = 0 := by have := congrArg Neg.neg h; simpa using this\n    have h2 := ρ.2.2.1\n    rw [this, Complex.zero_re] at h2\n    exact lt_irrefl 0 h2\n  rw [iteratedDerivWithin_of_isOpen isOpen_ball hmem, iteratedDeriv_seriesTerm j hj ρ h0ρ]\n```\nNotes:\n- iteratedDerivWithin_tsum's conclusion: iteratedDerivWithin k (∑' f) u x = ∑' n, iteratedDerivWithin k (f n) u x — with seriesFun = ∑' seriesTerm ✓ — rw [iteratedDerivWithin_tsum ...] rewrites the LHS; but the hypothesis-side goals: the pattern from LiDigamma:752-755: `rw [iteratedDerivWithin_tsum k dpsiDomain_isOpen dpsiDomain_half (fun s hs => ...) (fun j hj1 _ => ...) ?_]` — the last ?_ is the differentiability condition, discharged after with the two bullets (· apply tsum_congr ... wait no — in LiDigamma, after the rw there were TWO goals: the main (tsum_congr per-term) and ?_ (differentiability). They structured:\n```lean\n  rw [iteratedDerivWithin_tsum k ... ?_]\n  · apply tsum_congr\n    intro m\n    exact iteratedDerivWithin_dpsiTermC ...\n  · intro n j r hjm hr\n    ...\n```\nSo the rw generates: goal1 = the resulting equation (needs tsum_congr), goal2 = the differentiability side condition. I'll mirror: rw [...]; · tsum_congr per-term (within→global→seriesTerm closed form); · the differentiability intro.\n\nHmm wait — in my hmain I wrote the equation directly as the target with the per-term Within forms — so after rw [iteratedDerivWithin_tsum ...], the goal becomes ∑' ρ, iteratedDerivWithin j (seriesTerm · ρ) u 0 = ∑' ρ, iteratedDerivWithin j (seriesTerm · ρ) u 0 (rfl) — no. Let me restructure hmain to produce EXACTLY the tsum-lemma's output, then do the per-term conversion separately:\n\n```lean\n  have hmain : iteratedDerivWithin j seriesFun (Metric.ball 0 (δ / 2)) 0 =\n      ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},\n        iteratedDerivWithin j (fun s => seriesTerm s ρ) (Metric.ball 0 (δ / 2)) 0 := by\n    rw [seriesFun]\n    rw [iteratedDerivWithin_tsum j isOpen_ball hmem (fun s _ => seriesSummable s)\n      (fun j' hj'1 _ => seriesTerm_deriv_summableLocallyUniformlyOn j' hj'1 hδ hball) ?_]\n    · intro ρ j' r hjm hr\n      (differentiability side condition)\n```\nWait — does the rw [iteratedDerivWithin_tsum] leave the tsum_congr goal? In LiDigamma the target was the VALUE equation (they needed the per-term closed form at 1/2, hence the first bullet). For hmain, the target is EXACTLY the tsum-lemma's conclusion shape — after rw, goal closes by rfl?? No — rw [iteratedDerivWithin_tsum ...] rewrites instances of the LHS pattern (iteratedDerivWithin k (∑' f) u x) in the goal — the goal IS that equation; the rw rewrites the LHS to the RHS form, leaving `∑' ... = ∑' ...` rfl — closed automatically by rw ✓ plus the side-condition goal remains. But the ?_ placeholder in the rw args: supplying ?_ as the last arg means the side condition becomes a NEW goal instead of being unified — with two goals: (1) rfl-closed main? Actually with ?_ in the rw, after rewriting the main goal is closed; the ?_ goal is the side condition. Order of goals: the ?_ comes as a new goal. So:\n```lean\n    rw [iteratedDerivWithin_tsum j isOpen_ball hmem ... ?_]\n    intro ρ j' r hjm hr\n    (discharge)\n```\nBut careful — if the main goal closes by rfl during rw, the remaining goal is the side condition ✓. Hmm — but does `seriesFun` need unfolding first? seriesFun 0 vs ∑' seriesTerm: the tsum-lemma's LHS pattern: iteratedDerivWithin j (fun s => ∑' ρ, seriesTerm s ρ) — goal's function is seriesFun (a def) — the pattern fun s => ∑' ρ, seriesTerm s ρ vs seriesFun — rw needs syntactic match: unfold seriesFun first: rw [seriesFun] — but seriesFun is a def — rw [seriesFun] (the Fexpr-pattern ✓ works). BUT it rewrites seriesFun EVERYWHERE including inside hmem?? no — hmem is a hypothesis, rw [seriesFun] only at goal ✓. Goal after: iteratedDerivWithin j (fun s => ∑' ρ, seriesTerm s ρ) u 0 = ... ✓ then the tsum-rw matches.\n\nWait — actually does iteratedDerivWithin_tsum's LHS have the form with the LAMBDA (fun s => ∑' n, f n s)? The lemma: iteratedDerivWithin k (fun x => ∑' n, f n x) u x = ∑' n, iteratedDerivWithin k (f n) u x presumably. After rw [seriesFun], goal LHS: iteratedDerivWithin j (fun s => ∑' ρ, seriesTerm s ρ) (ball) 0 ✓ matches.\n\nThen final: \n```lean\n  rw [← iteratedDerivWithin_of_isOpen isOpen_ball hmem, hmain]\n  apply tsum_congr\n  intro ρ\n  rw [iteratedDerivWithin_of_isOpen isOpen_ball hmem, iteratedDeriv_seriesTerm j hj ρ h0ρ]\n```\n✓ (with h0ρ proved before).\n\nSide-condition (j' = 0 case): after rw [iteratedDerivWithin_zero]: goal DifferentiableAt ℂ (fun s => seriesTerm s ρ) r — rw [seriesTerm]: function fun s => mult·(1/(s−ρ) + 1/ρ): DifferentiableAt.const_mul _ (hr-diff): DifferentiableAt (fun s => 1/(s−ρ) + 1/ρ) r: .add of: (differentiableAt_const 1).div (differentiableAt_id.sub differentiableAt_const) hrρ + differentiableAt_const ✓. Then const_mul needs DifferentiableAt of the inner: `DifferentiableAt.const_mul (hg : DifferentiableAt g x) (c) : DifferentiableAt (fun x => c * g x) x`? signature: DifferentiableAt.const_mul (hd : DifferentiableAt 𝕜 f x) (c : 𝔸')?? Hmm — for ℂ: `DifferentiableAt.const_mul (hf : DifferentiableAt 𝕜 f x) (c : 𝕜) : DifferentiableAt 𝕜 (fun x => c * f x) x`? arg order — from LiDigamma:785: `exact (differentiableAt_const _).mul h6` — they used .mul with the const on the LEFT: (differentiableAt_const _).mul h6 : DifferentiableAt (fun r => const · h6-fun) ✓ — const_mul via mul with const first ✓. My term mult·(X): (differentiableAt_const (zeroMult ρ : ℂ)).mul hX ✓ same pattern.\n\nFor the j' ≥ 1 case: h5 eventuallyEq — the closed-form differentiability: const_mul·const_mul·zpow-comp: ((hasDerivAt_zpow ...).differentiableAt).comp r h4 — produces DifferentiableAt ((fun x => x^z) ∘ (fun t => t−ρ)) r — vs needed (fun t => (t−ρ)^z): the rfl bridge (LiDigamma:781-783 pattern ✓):\n```lean\n        have h6 : DifferentiableAt ℂ (fun t : ℂ => (t - (ρ : ℂ)) ^ (-(j' : ℤ) - 1)) r := by\n          have h7 := ((hasDerivAt_zpow (-(j' : ℤ) - 1) (r - (ρ : ℂ)) (Or.inl hrρ)).differentiableAt).comp r h4\n          have heq : ((fun x : ℂ => x ^ (-(j' : ℤ) - 1)) ∘ fun t : ℂ => t - (ρ : ℂ)) =\n              fun t : ℂ => (t - (ρ : ℂ)) ^ (-(j' : ℤ) - 1) := rfl\n          rw [heq] at h7\n          exact h7\n        exact (differentiableAt_const _).mul ((differentiableAt_const _).mul h6)\n```\n✓ clone.\n\n- htρ/hrρ for r, t ∈ ball: ‖t‖ < δ/2, ‖ρ‖ ≥ δ ⟹ t − ρ ≠ 0 (as shown: if t = ρ then ‖ρ‖ < δ/2 < δ ✗).\n\n§6 capstone:\n\n```lean\n/-! ## 6. The capstone -/\n\n/-- gFun agrees with B + seriesFun on a full neighbourhood of 0. -/\nlemma gFun_eventuallyEq_zero (hZC : ZeroCountProp) :\n    gFun =ᶠ[𝓝 0] (fun s => momentB hZC + seriesFun s) := by\n  -- from the punctured version + the value at 0\n  have hp : ∀ᶠ s in 𝓝[≠] (0 : ℂ), gFun s = momentB hZC + seriesFun s := by\n    filter_upwards [good_eventually_zero, self_mem_nhdsWithin] with s ⟨hζ, h1, hn⟩ h0\n    exact gFun_eq_momentB hZC hζ h0 h1 hn\n  -- upgrade: 𝓝 0 = 𝓝[≠] 0 ⊔ pure 0\n  ...\n```\nFor the upgrade — look for the lemma: `Filter.EventuallyEq.insert`? Hmm. There's: `nhdsWithin_union`? The clean one: `Filter.EventuallyEq.of_nhdsWithin_punctured`? Let me think of the standard: (𝓝[≠] a) and f a = g a gives f =ᶠ[𝓝 a] g: prove via: 𝓝 a = 𝓝[{a}ᶜ] a ⊔ 𝓝[{a}] a?? Hmm. Standard lemma: `eventually_nhdsWithin_iff`? The insert fact: {a} ∈ 𝓝 a... Write manually:\n```lean\n  rw [Filter.EventuallyEq] at hp ⊢\n  rw [eventually_nhds_iff]  -- ?? does eventually_nhds_iff exist: (∀ᶠ x in 𝓝 a, p x) ↔ p a ∨ ∀ᶠ x in 𝓝[≠] a, p x — hmm name...\n```\nMathlib: `eventually_nhdsWithin_iff` is about s. For nhds: there IS `Filter.eventually_nhds_iff_eventually_nhdsWithin`? not sure. There's `eventually_nhds_iff` : (∀ᶠ x in 𝓝 a, p x) ↔ ∀ ε > 0... no that's metric. \n\nRobust manual: use Metric.eventually_nhds_iff_ball both ways:\n```lean\n  rw [Metric.eventually_nhdsWithin_iff_ball?? no...\n```\nAlternative — the punctured-to-full upgrade: \n```lean\n  have h0 : gFun 0 = momentB hZC + seriesFun 0 := by\n    rw [gFun_zero hZC, seriesFun_zero, add_zero]\n  -- ∀ᶠ s in 𝓝 0: use that 𝓝[≠] 0 ≤ 𝓝 0 and {0}ᶜ ∪ {0}:\n  filter_upwards [hp.filter_mono (nhdsWithin_le_nhds?? wrong direction]...\n```\nHmm: hp : ∀ᶠ s in 𝓝[≠] 0, P s. Want ∀ᶠ s in 𝓝 0, P' s where P' accounts for s = 0. Trick: ∀ᶠ s in 𝓝 0, s ∈ {0}ᶜ → P s?? Use: eventually_nhdsWithin_iff : (∀ᶠ x in 𝓝[s] a, p x) ↔ ∀ᶠ x in 𝓝 a, x ∈ s → p x: hp ↔ ∀ᶠ s in 𝓝 0, s ≠ 0 → P s. Then filter_upwards [that] with s hs: cases s = 0: if s = 0 use h0; else hs h. So:\n```lean\n  rw [eventually_nhdsWithin_iff] at hp\n  filter_upwards [hp] with s hs\n  by_cases h : s = 0\n  · subst h\n    exact h0\n  · exact hs h\n```\neventually_nhdsWithin_iff : (∀ᶠ x in 𝓝[s] a, p x) ↔ ∀ᶠ x in 𝓝 a, x ∈ s → p x ✓ exists (I'm fairly confident). With s = {0}ᶜ: 𝓝[{0}ᶜ] 0 = 𝓝[≠] 0 — is hp stated with 𝓝[≠]? 𝓝[≠] a is notation for 𝓝[{a}ᶜ] a ✓ same. ✓\n\nThen:\n```lean\ntheorem sigmaP_eq_neg_iteratedDeriv_gFun_div (hZC : ZeroCountProp) {k : ℕ} (hk : 1 ≤ k) :\n    sigmaP k = -(iteratedDeriv (k - 1) gFun 0) / ((k - 1)! : ℂ) := by\n  rcases Nat.lt_or_ge k 2 with hk1 | hk2\n  · have hk1' : k = 1 := by omega\n    subst hk1'\n    rw [Nat.sub_self, iteratedDeriv_zero, Nat.factorial_zero, Nat.cast_one, div_one]\n    exact sigmaP_one_eq_neg_gFun_zero hZC\n  · -- k ≥ 2\n    have hcong := iteratedDeriv_congr_of_eventuallyEq (gFun_eventuallyEq_zero hZC) (k - 1)\n    rw [hcong]\n    -- iteratedDeriv (k−1) (B + seriesFun) 0 = iteratedDeriv (k−1) seriesFun 0\n    have hcf : ContDiffAt ℂ (k - 1 : ℕ∞)?? ...\n```\nHmm — iteratedDeriv_add's ContDiffAt requirement: `iteratedDeriv_add (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x)` — with n : ℕ (the same n as the iteratedDeriv order). The LiDigamma usage: `iteratedDeriv_add hcf hcg` with hcf : ContDiffAt ℂ k ... — k : ℕ (the order) — ContDiffAt ℂ k — the k coerces to ℕ∞ ✓ (ContDiffAt takes ℕ∞). So:\n```lean\n    have hcf : ContDiffAt ℂ (k - 1 : ℕ) (fun _ : ℂ => momentB hZC) 0 := contDiff_const.contDiffAt\n    have hcg : ContDiffAt ℂ (k - 1 : ℕ) seriesFun 0 :=\n      (seriesFun_analyticAt not_isNontrivialZero_zero).contDiffAt\n    rw [iteratedDeriv_add hcf hcg, iteratedDeriv_const, if_neg (by omega : k - 1 ≠ 0), zero_add]\n```\nHmm — ContDiffAt ℂ (k−1 : ℕ) — the coercion: ContDiffAt's smoothness parameter type ℕ∞ (WithTop ℕ∞?): in current Mathlib ContDiffAt 𝕜 (n : ℕ∞)?? — actually `ContDiffAt 𝕜 n` with n : ℕ∞ = WithTop ℕ∞? — plain ℕ works via coercion: LiDigamma:695 wrote ContDiffAt ℂ k with k : ℕ ✓ (coercion inserted). For k−1 : write (k - 1 : ℕ) — the iteratedDeriv (k−1) has k−1 : ℕ — the coercion matches automatically.\n\nAnalyticAt.contDiffAt : AnalyticAt ℂ f x → ContDiffAt ℂ n f x? — signature: `AnalyticAt.contDiffAt (h : AnalyticAt ℂ f x) : ContDiffAt ℂ n f x`? — for ANY n (analytic ⟹ C^∞) ✓ I believe `AnalyticAt.contDiffAt` exists (analyticAt.contDiff? hmm). LiDigamma:701: `exact h3.neg.contDiffAt` — AnalyticAt.neg then .contDiffAt ✓ — so AnalyticAt.contDiffAt exists ✓ and the n is implicit/inferred ✓.\n\nThen:\n```lean\n    -- = ∑' ρ, mult·(−1)^{k−1}(k−1)!·(0−ρ)^{−k} = −(k−1)!·sigmaP k\n    rw [iteratedDeriv_seriesFun_zero (k - 1) (by omega)]\n    -- exponent: −(k−1:ℤ)−1 = −(k:ℤ)\n    have hexp : (-(k - 1 : ℤ) - 1 : ℤ) = -(k : ℤ) := by\n      have : ((k : ℤ) - 1 : ℤ) = ((k - 1 : ℕ) : ℤ) := by\n        rw [Int.ofNat_sub (by omega : 1 ≤ k)]\n      ...\n      push_cast [this]... \n```\nHmm — careful: (k − 1 : ℤ) with k : ℕ: the iteratedDeriv_seriesFun_zero's exponent is −(j:ℤ)−1 with j := k−1 (ℕ sub!): −((k−1:ℕ):ℤ)−1. Want = −(k:ℤ): ((k−1:ℕ):ℤ) = (k:ℤ)−1 (Int.ofNat_sub hk : ((k−1:ℕ):ℤ) = (k:ℤ)−1 ✓ `Int.ofNat_sub (h : m ≤ n) : (↑(n − m) : ℤ) = ↑n − ↑m` ✓). So −((k−1:ℕ):ℤ)−1 = −((k:ℤ)−1)−1 = −(k:ℤ) ✓: \n```lean\n    have hexp : (-(((k - 1 : ℕ) : ℤ)) - 1 : ℤ) = -(k : ℤ) := by\n      rw [Int.ofNat_sub hk]\n      push_cast\n      ring\n```\npush_cast for the (↑k : ℤ) forms... ((k:ℤ)−1) — fine: rw [Int.ofNat_sub hk]: goal -(↑k − 1) − 1 = -↑k: ring ✓ (no push_cast needed).\n\nThen per-term evaluation at 0:\n```lean\n    -- ∑' ρ, mult·((−1)^{k−1}(k−1)!·(0−ρ)^{−(k:ℤ)}) = −(k−1)!·sigmaP k\n    have heval : (∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, (zeroMult ρ : ℂ) *\n        ((-1 : ℂ) ^ (k - 1) * ((k - 1)! : ℂ) * ((0 : ℂ) - (ρ : ℂ)) ^ (-(k - 1 : ℤ) - 1))) =\n        -(((k - 1)! : ℂ)) * sigmaP k := by\n      rw [hexp]\n      -- per-term: mult·((−1)^{k−1}(k−1)!·(0−ρ)^{−k}) = −(k−1)!·mult·(1/ρ)^k\n      have hper : ∀ ρ : {ρ : ℂ // IsNontrivialZero ρ},\n          (zeroMult ρ : ℂ) * ((-1 : ℂ) ^ (k - 1) * ((k - 1)! : ℂ) * ((0 : ℂ) - (ρ : ℂ)) ^ (-(k : ℤ))) =\n          -(((k - 1)! : ℂ)) * ((zeroMult ρ : ℂ) * (1 / (ρ : ℂ)) ^ k) := by\n        intro ρ\n        have hρ0 : (ρ : ℂ) ≠ 0 := ...\n        -- (0−ρ)^{−k} = (−ρ)^{−k} = (−1)^k·(ρ^k)⁻¹·... \n        have e1 : ((0 : ℂ) - (ρ : ℂ)) ^ (-(k : ℤ)) = (-1 : ℂ) ^ k * (1 / (ρ : ℂ)) ^ k := by\n          rw [zero_sub]\n          -- (−ρ)^{(−k:ℤ)} = ((−ρ)^k)⁻¹ = ((−1)^k ρ^k)⁻¹ = (−1)^k (ρ^k)⁻¹ = (−1)^k (1/ρ)^k\n          rw [zpow_neg, zpow_natCast, neg_pow]\n          rw [mul_inv]\n          -- ((−1)^k)⁻¹·(ρ^k)⁻¹ = (−1)^k·(ρ^k)⁻¹: ((−1)^k)⁻¹ = (−1)^k\n          have h2 : ((-1 : ℂ) ^ k)⁻¹ = (-1 : ℂ) ^ k := by\n            apply inv_eq_of_mul_eq_one_right\n            rw [← pow_add, ← two_mul]\n            -- (−1)^{2k} = 1: Even: even (2k): Even.neg_one_pow?? \n            have : ((-1 : ℂ) ^ 2) ^ k = 1 := by\n              rw [show (-1 : ℂ) ^ 2 = 1 by ring]\n              exact one_pow k\n            rwa [← pow_mul, mul_comm 2 k, pow_mul] at this?? \n          rw [h2, ← mul_pow, one_div]\n          -- (−1)^k·(ρ^k)⁻¹ vs (−1)^k·(1/ρ)^k: (1/ρ)^k = (ρ^k)⁻¹: one_div_pow?? inv_pow: (ρ⁻¹)^k = (ρ^k)⁻¹; 1/ρ = ρ⁻¹: one_div... \n          congr 1\n          rw [one_div, ← inv_pow]\n        rw [e1]\n        -- mult·((−1)^{k−1}(k−1)!·((−1)^k·(1/ρ)^k)) = −(k−1)!·mult·(1/ρ)^k\n        have hsign : (-1 : ℂ) ^ (k - 1) * (-1 : ℂ) ^ k = -1 := by\n          rw [← pow_add]\n          -- (−1)^{k−1+k} = (−1)^{2k−1} = −1\n          have h2 : k - 1 + k = 2 * k - 1 := by omega\n          rw [h2]\n          -- (−1)^{2k−1} = (−1)^{2k}/(−1) = 1/(−1) = −1: pow_sub?? for ℕ: 2k−1: use: 2k−1 = 2(k−1)+1: \n          have h3 : 2 * k - 1 = 2 * (k - 1) + 1 := by omega\n          rw [h3, pow_add]\n          have h4 : (-1 : ℂ) ^ (2 * (k - 1)) = 1 := by\n            rw [pow_mul, show (-1 : ℂ) ^ 2 = 1 by ring]\n            exact one_pow _\n          rw [h4, one_mul]\n          -- (−1)^1 = −1\n          exact pow_one _\n        -- assemble: mult·((−1)^{k−1}·(k−1)!·((−1)^k·w)) = −(k−1)!·mult·w\n        calc (zeroMult ρ : ℂ) * ((-1 : ℂ) ^ (k - 1) * ((k - 1)! : ℂ) * ((-1 : ℂ) ^ k * (1 / (ρ : ℂ)) ^ k))\n            = ((zeroMult ρ : ℂ) * ((k - 1)! : ℂ) * (1 / (ρ : ℂ)) ^ k) * ((-1 : ℂ) ^ (k - 1) * (-1 : ℂ) ^ k) := by ring\n          _ = ((zeroMult ρ : ℂ) * ((k - 1)! : ℂ) * (1 / (ρ : ℂ)) ^ k) * (-1) := by rw [hsign]\n          _ = -(((k - 1)! : ℂ)) * ((zeroMult ρ : ℂ) * (1 / (ρ : ℂ)) ^ k) := by ring\n      rw [tsum_congr hper, ← sigmaP_eq_unpaired hk2]\n      -- ∑' ρ, −(k−1)!·(mult·(1/ρ)^k) = −(k−1)!·∑' ... : tsum_mul_left\n      rw [tsum_mul_left]\n```\nCareful: hper's RHS: −(k−1)!·(mult·(1/ρ)^k) — the unpaired family: mult·(1/ρ)^k: ∑' ρ, −(k−1)!·(mult·(1/ρ)^k) = −(k−1)!·∑' mult·(1/ρ)^k (tsum_mul_left ✓) = −(k−1)!·sigmaP k (sigmaP_eq_unpaired hk2 ✓).\n\nzpow manipulations: ((0:ℂ)−ρ)^(−k:ℤ): zero_sub → (−ρ)^(−k:ℤ); zpow_neg : a^{−n} = (a^n)⁻¹ ✓ `zpow_neg (a) (n : ℤ) : a ^ (-n) = (a ^ n)⁻¹`; zpow_natCast : a^{(n:ℤ)} = a^n ✓. So (−ρ)^{(−(k:ℤ))} → wait the exponent is −(k:ℤ) where k : ℕ cast — zpow_neg needs the exponent literally as −x: −(k:ℤ) = −((k:ℕ):ℤ): pattern a ^ (-x) with x := (k:ℤ) ✓. → ((−ρ)^(k:ℤ))⁻¹ → zpow_natCast → ((−ρ)^k)⁻¹ → neg_pow : (−a)^n = (−1)^n·a^n ✓ `neg_pow (a) (n : ℕ)` — used LiSwaps:106 ✓. → ((−1)^k·ρ^k)⁻¹ → mul_inv : (a·b)⁻¹ = a⁻¹·b⁻¹ ✓. → (−1)^k⁻¹·(ρ^k)⁻¹: h2: ((−1)^k)⁻¹ = (−1)^k via inv_eq_of_mul_eq_one_right : a·b = 1 → a⁻¹ = b: with a := (−1)^k, b := (−1)^k: need (−1)^k·(−1)^k = 1: ← pow_add: (−1)^{k+k}: k+k = 2k: ← two_mul: then (−1)^{2k}: pow_mul: ((−1)²)^k = 1^k = 1: \n```lean\n          have h2 : ((-1 : ℂ) ^ k)⁻¹ = (-1 : ℂ) ^ k := by\n            apply inv_eq_of_mul_eq_one_right\n            rw [← pow_add, ← two_mul, pow_mul]\n            rw [show (-1 : ℂ) ^ 2 = 1 by ring]\n            exact one_pow k\n```\ninv_eq_of_mul_eq_one_right : a * b = 1 → a⁻¹ = b ✓ exists (session-033-ish? `inv_eq_of_mul_eq_one_right` ✓ I'm fairly confident; else `inv_eq_of_mul_eq_one_left`). The a here is (−1)^k (the thing being inverted) and b = (−1)^k: goal a·b = 1 ✓.\n\nThen: (−1)^k·(ρ^k)⁻¹ = (−1)^k·(1/ρ)^k: (1/ρ)^k = (ρ^k)⁻¹: `one_div_pow`? or inv_pow: (ρ⁻¹)^k = (ρ^k)⁻¹ ✓ `inv_pow (a) (n)`; 1/ρ = ρ⁻¹: one_div. So congr 1; rw [one_div, ← inv_pow] — goal (−1)^k·(ρ^k)⁻¹ = (−1)^k·(ρ⁻¹)^k?? wait — my e1's RHS is (−1)^k·(1/ρ)^k: after rw [h2] on LHS: (−1)^k·(ρ^k)⁻¹ = (−1)^k·(1/ρ)^k: congr 1 → (ρ^k)⁻¹ = (1/ρ)^k: rw [one_div]: (ρ^k)⁻¹ = (ρ⁻¹)^k: ← inv_pow ✓.\n\nHold on — e1's statement: ((0:ℂ)−ρ)^(−k:ℤ) = (−1)^k·(1/ρ)^k. Let me re-derive: (−ρ)^{−k} = ((−ρ)^k)⁻¹ = ((−1)^k·ρ^k)⁻¹ = ((−1)^k)⁻¹·(ρ^k)⁻¹ = (−1)^k·(ρ^k)⁻¹ = (−1)^k·(1/ρ)^k ✓ (since (1/ρ)^k = 1/ρ^k = (ρ^k)⁻¹ ✓).\n\nHmm — and zpow_neg signature: `zpow_neg (a : α) (n : ℤ) : a ^ (-n) = (a ^ n)⁻¹` ✓ exists. zpow_natCast : `zpow_natCast (a : α) (n : ℕ) : a ^ (n : ℤ) = a ^ n` ✓.\n\nhsign: (−1)^{k−1}·(−1)^k = −1: ← pow_add: (−1)^{(k−1)+k}: k−1+k = 2k−1 (omega, k ≥ 2 — hmm Nat: k−1+k with k ≥ 2 ✓ omega): then 2k−1 = 2(k−1)+1 (omega k ≥ 2 ✓): pow_add: (−1)^{2(k−1)}·(−1)^1: h4: (−1)^{2(k−1)} = ((−1)²)^{k−1} = 1: pow_mul : a^{m·n} = (a^m)^n ✓ `pow_mul (a) (m n) : a ^ (m * n) = (a ^ m) ^ n`. 2·(k−1) — pow_mul with m = 2, n = k−1 ✓. one_mul; pow_one ✓.\n\npow_add : a^{m+n} = a^m·a^n ✓.\n\nThe final capstone assembly:\n```lean\n    rw [heval]  -- goal: sigmaP k = −(−(k−1)!·sigmaP k)/(k−1)!\n    -- = sigmaP k: field\n    have hfact : ((k - 1)! : ℂ) ≠ 0 := by\n      rw [Ne, Nat.cast_eq_zero]\n      exact Nat.factorial_ne_zero (k - 1)\n    field_simp [hfact]\n    ring\n```\ngoal after heval: sigmaP k = −(−(k−1)!·sigmaP k)/((k−1)!) : field_simp [hfact]; ring ✓ (−(−X)/Y = X/Y = ... : −(−(k−1)!·σ)/(k−1)! = σ·((k−1)!/(k−1)!) = σ ✓ ring after clearing).\n\nHmm wait — the goal after rw [hcong, ..., heval]: sigmaP k = -(iteratedDeriv...)/... where the iteratedDeriv was rewritten to the tsum and then heval replaced the tsum with −(k−1)!·sigmaP k — the rw chain: hcong rewrites iteratedDeriv (k−1) gFun 0 → iteratedDeriv (k−1) (B+seriesFun) 0 ✓; then iteratedDeriv_add etc rewrite; iteratedDeriv_seriesFun_zero rewrites iteratedDeriv (k−1) seriesFun 0 → the tsum ✓; heval is a standalone — rw [heval] rewrites the tsum → −(k−1)!·sigmaP k ✓. Goal: sigmaP k = −(−(k−1)!·sigmaP k)/(k−1)! ✓ field_simp+ring.\n\nOne concern — the rw [hcong]: hcong : iteratedDeriv (k−1) gFun 0 = iteratedDeriv (k−1) (fun s => B + seriesFun s) 0 — iteratedDeriv_congr_of_eventuallyEq (h : f =ᶠ[𝓝 x] g) (n) : iteratedDeriv n f x = iteratedDeriv n g x ✓ (LiDigamma:568). ✓\n\nAnd iteratedDeriv_add's function form: fun s => B + seriesFun s — the lemma iteratedDeriv_add (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) : iteratedDeriv n (f + g) x = ...?? or pointwise fun x => f x + g x? From LiDigamma:702 the rw worked on their lambda with pointwise mix (1/(m+1) + −(1/(s+m+1)))?? They had heq-rewritten to a Pi.add form: line 688-693: `(fun s => dpsiTermC s m) = (fun s => 1/...) + fun s => -(1/...)` — note the FIRST is a bare function and `+ fun s => ...` — so it's HAdd of functions with a lambda — mixed. iteratedDeriv_add hcf hcg rewrote iteratedDeriv k ((fun s => 1/...) + fun s => ...) — so the lemma's LHS is iteratedDeriv n (f + g) x with Pi.add? or the pointwise lambda? Their form: (fun s => ...) + fun s => ... — that IS Pi.add (HAdd.hAdd of two functions). So iteratedDeriv_add : iteratedDeriv n (f + g) x = iteratedDeriv n f x + iteratedDeriv n g x with Pi.add ✓. My function: fun s => B + seriesFun s — LAMBDA with pointwise add — NOT syntactically (fun _ => B) + seriesFun. The rw [iteratedDeriv_add hcf hcg] would need the goal's function to match (f + g): MISMATCH. Fix: bridge: have : (fun s => momentB hZC + seriesFun s) = (fun _ : ℂ => momentB hZC) + seriesFun := by funext s; rfl?? — Pi.add_apply: ((f+g) s = f s + g s) rfl ✓ so funext s; rfl works? (fun _ => B) + seriesFun applied at s = B + seriesFun s ✓ rfl. So:\n```lean\n    have eadd : (fun s => momentB hZC + seriesFun s) = (fun _ : ℂ => momentB hZC) + seriesFun := by\n      funext s\n      rfl\n    rw [eadd, iteratedDeriv_add hcf hcg, ...]\n```\n✓ (the Pi.add_apply gotcha again).\n\nSimilarly iteratedDeriv_const : iteratedDeriv n (fun _ => c) x = if n = 0 then c else 0 — from LiDigamma:703 `rw [iteratedDeriv_const, if_neg (by omega : k ≠ 0)]` ✓.\n\nOK — also `sigmaP_one_eq_neg_gFun_zero` and the k=1 branch: after subst hk1' (k := 1): goal sigmaP 1 = −(iteratedDeriv (1−1) gFun 0)/((1−1)!:ℂ): rw [Nat.sub_self?? 1−1 = 0: `Nat.sub_self 1 : 1 − 1 = 0`? hmm Nat.sub_self : n − n = 0 ✓; but the term is (1 − 1 : ℕ) — reduces to 0 definitionally — `show sigmaP 1 = -(iteratedDeriv 0 gFun 0)/((0)!:ℂ)`?? Nat subtraction 1−1 computes ✓ — simp [iteratedDeriv_zero]: simplest: `simp only [Nat.sub_self?..., iteratedDeriv_zero, Nat.factorial_zero, Nat.cast_one, div_one]`— Nat.sub_self needs the literal n − n form: (1 − 1) — simp only [Nat.sub_self] might not fire on numerals (1 − 1 is OfNat−OfNat — simp would compute via Nat.reduceSub? just use `norm_num`?? risky on the goal shape. Alternative: change k−1 to 0 via `show`: sigmaP 1 = −(iteratedDeriv (1−1) gFun 0)/...: `conv_rhs => rw [show (1 : ℕ) - 1 = 0 from rfl]`?? 1−1 = 0 is rfl ✓ (Nat sub computes). So: `show sigmaP 1 = -(iteratedDeriv 0 gFun 0) / ((0)! : ℂ)` — is the goal defeq? (1−1) ≡ 0 ✓ defeq: `show` with defeq target ✓ should work. Then rw [iteratedDeriv_zero, Nat.factorial_zero, Nat.cast_one, div_one] → sigmaP 1 = −gFun 0 ✓ exact sigmaP_one_eq_neg_gFun_zero hZC.\n\nHmm — (0)! vs Nat.factorial 0 — the goal's form: ((1 - 1)! : ℂ) — after show: ((0)!:ℂ) — Nat.factorial 0 = 1: rw [Nat.factorial_zero]?? Nat.factorial_zero : (0)! = 1 ✓ then Nat.cast_one, div_one ✓.\n\nWait — actually there's subtlety: after `subst hk1'`, k is replaced by 1 everywhere: goal sigmaP 1 = −(iteratedDeriv (1−1) gFun 0)/(((1−1))!:ℂ). `show sigmaP 1 = -(iteratedDeriv 0 gFun 0) / ((0)! : ℂ)`: defeq check: (1−1:ℕ) ≡ 0 ✓, ((1−1)!:ℂ) ≡ ((0)!:ℂ) ✓ — should pass.\n\nAlright — write §4–§6 now. It's a lot; let me write carefully. Also need in §4: hρ0/h1ρ helpers — reuse the ones from seriesFun_one (write once as private-ish lemmas? They're used repeatedly: ρ ≠ 0, 1−ρ ≠ 0, ‖ρ‖ > 0, ‖1−ρ‖ > 0). Make small lemmas:\n\n```lean\nlemma nontrivialZero_ne_zero (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : (ρ : ℂ) ≠ 0 := by\n  intro h0\n  have h2 := ρ.2.2.1\n  rw [h0, Complex.zero_re] at h2\n  exact lt_irrefl 0 h2\n\nlemma one_sub_nontrivialZero_ne_zero (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : (1 : ℂ) - (ρ : ℂ) ≠ 0 := by\n  intro h\n  have h3 : (1 : ℂ) = (ρ : ℂ) := sub_eq_zero.mp h\n  have h4 := ρ.2.2.2\n  rw [← h3, Complex.one_re] at h4\n  exact lt_irrefl 1 h4\n\nlemma norm_nontrivialZero_pos (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : (0 : ℝ) < ‖(ρ : ℂ)‖ :=\n  norm_pos_iff.mpr (nontrivialZero_ne_zero ρ)\n\nlemma norm_one_sub_nontrivialZero_pos (ρ : {ρ : ℂ // IsNontrivialZero ρ}) :\n    (0 : ℝ) < ‖(1 : ℂ) - (ρ : ℂ)‖ :=\n  norm_pos_iff.mpr (one_sub_nontrivialZero_ne_zero ρ)\n```\n✓ (norm_pos_iff : 0 < ‖x‖ ↔ x ≠ 0 ✓).\n\nLet me write the whole §4–§6 block now, appending before `end NguyenRH1`. This is big — I'll write it in two Write/Edit operations (§4, then §5+§6).","signature":""},{"type":"text","text":"Patterns confirmed. Writing §4 (summability budget + k=1 rearrangement) now."},{"type":"tool_use","id":"Edit_89","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiMoments.lean","old_string":"end NguyenRH1","new_string":"/-! ## 4. The summability budget and the k = 1 rearrangement -/\n\nlemma nontrivialZero_ne_zero (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : (ρ : ℂ) ≠ 0 := by\n  intro h0\n  have h2 := ρ.2.2.1\n  rw [h0, Complex.zero_re] at h2\n  exact lt_irrefl 0 h2\n\nlemma one_sub_nontrivialZero_ne_zero (ρ : {ρ : ℂ // IsNontrivialZero ρ}) :\n    (1 : ℂ) - (ρ : ℂ) ≠ 0 := by\n  intro h\n  have h3 : (1 : ℂ) = (ρ : ℂ) := sub_eq_zero.mp h\n  have h4 := ρ.2.2.2\n  rw [← h3, Complex.one_re] at h4\n  exact lt_irrefl 1 h4\n\nlemma norm_nontrivialZero_pos (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : (0 : ℝ) < ‖(ρ : ℂ)‖ :=\n  norm_pos_iff.mpr (nontrivialZero_ne_zero ρ)\n\nlemma norm_one_sub_nontrivialZero_pos (ρ : {ρ : ℂ // IsNontrivialZero ρ}) :\n    (0 : ℝ) < ‖(1 : ℂ) - (ρ : ℂ)‖ :=\n  norm_pos_iff.mpr (one_sub_nontrivialZero_ne_zero ρ)\n\n/-- **Master summability**: Σ mult/‖ρ‖² over the zeros (the ii′-2\nfinite-ball + (9/4)-comparison skeleton). -/\nlemma summable_mult_div_norm_sq :\n    Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => (zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ 2) := by\n  have hbase : Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n      (9 / 4) * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ)))) :=\n    (WeilEF.zero_sum_inv_sq zetaSeam).mul_left (9 / 4)\n  set D : {ρ : ℂ // IsNontrivialZero ρ} → ℝ := fun ρ =>\n    if (2 : ℝ) ≤ ‖(ρ : ℂ)‖ then\n      (9 / 4) * (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ))\n    else (zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ 2 with hDdef\n  have hfin : {ρ : {ρ // IsNontrivialZero ρ} | ¬ ((2 : ℝ) ≤ ‖(ρ : ℂ)‖)}.Finite := by\n    have hcomp : IsCompact (Metric.closedBall (0 : ℂ) 2) := isCompact_closedBall _ _\n    have hzeros : (Metric.closedBall (0 : ℂ) 2) ∩ {ρ : ℂ | IsNontrivialZero ρ}\n        ⊆ (Metric.closedBall (0 : ℂ) 2) ∩ 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 ρ} |\n        ¬ ((2 : ℝ) ≤ ‖(ρ : ℂ)‖)}).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 (lt_of_not_ge hρ)\n    exact Set.Finite.of_finite_image himg (Subtype.val_injective.injOn)\n  have hE : Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n      D ρ - (9 / 4) * ((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' : (2 : ℝ) ≤ ‖(ρ : ℂ)‖ := not_not.mp hball\n    simp only [D, if_pos hball']\n    ring\n  have hD : Summable D := by\n    have hsum := hbase.add hE\n    have heq : (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n        (9 / 4) * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ))) +\n          (D ρ - (9 / 4) * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ))))) = D := by\n      funext ρ\n      ring\n    rw [heq] at hsum\n    exact hsum\n  refine Summable.of_norm_bounded hD (fun ρ => ?_)\n  by_cases hρ : (2 : ℝ) ≤ ‖(ρ : ℂ)‖\n  · simp only [D, if_pos hρ]\n    have hz := ρ.2\n    have hρpos : (0 : ℝ) < ‖(ρ : ℂ)‖ := lt_of_lt_of_le (by norm_num) hρ\n    have hgpos : (0 : ℝ) < 1 + Complex.normSq (gammaOf (ρ : ℂ)) := by\n      have hnn := Complex.normSq_nonneg (gammaOf (ρ : ℂ))\n      linarith\n    have hcomp : 1 + Complex.normSq (gammaOf (ρ : ℂ)) ≤ 9 / 4 * ‖(ρ : ℂ)‖ ^ 2 :=\n      normSq_gammaOf_le_mul_norm_sq (n := 1) le_rfl hz.2.1.le hz.2.2.le (by simpa using hρ)\n    have key : (zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ 2 ≤\n        (9 / 4) * (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ)) := by\n      rw [div_le_div_iff₀ (pow_pos hρpos 2) hgpos]\n      calc (zeroMult ρ : ℝ) * (1 + Complex.normSq (gammaOf ρ))\n          ≤ (zeroMult ρ : ℝ) * (9 / 4 * ‖(ρ : ℂ)‖ ^ 2) :=\n            mul_le_mul_of_nonneg_left hcomp (Nat.cast_nonneg _)\n        _ = (9 / 4 * (zeroMult ρ : ℝ)) * ‖(ρ : ℂ)‖ ^ 2 := by ring\n    rw [Real.norm_of_nonneg (by positivity)]\n    exact key\n  · simp only [D, if_neg hρ]\n    rw [Real.norm_of_nonneg (by positivity)]\n\n/-- The avoiding-ball lower bound: every zero has δ ≤ ‖ρ‖. -/\nlemma exists_norm_lower_bound :\n    ∃ δ : ℝ, 0 < δ ∧ ∀ ρ : {ρ : ℂ // IsNontrivialZero ρ}, δ ≤ ‖(ρ : ℂ)‖ := by\n  obtain ⟨δ, hδ, hball⟩ := exists_ball_avoid_nontrivialZeros 0 not_isNontrivialZero_zero\n  refine ⟨δ, hδ, fun ρ => ?_⟩\n  by_contra h\n  exact hball ρ (by rw [Metric.mem_ball, dist_zero_right]; exact lt_of_not_ge h)\n\n/-- Σ mult·ρ^{−k} is absolutely summable for k ≥ 2. -/\nlemma summable_mult_inv_pow {k : ℕ} (hk : 2 ≤ k) :\n    Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => (zeroMult ρ : ℂ) * (1 / (ρ : ℂ)) ^ k) := by\n  obtain ⟨m, rfl⟩ := Nat.exists_eq_add_of_le hk\n  obtain ⟨δ, hδ, hδle⟩ := exists_norm_lower_bound\n  apply Summable.of_norm_bounded (summable_mult_div_norm_sq.mul_left ((1 / δ) ^ m))\n  intro ρ\n  have hρδ := hδle ρ\n  have hρpos : (0 : ℝ) < ‖(ρ : ℂ)‖ := lt_of_lt_of_le hδ hρδ\n  rw [norm_mul, norm_pow, norm_div, norm_one, RCLike.norm_natCast, div_pow, one_pow]\n  calc (zeroMult ρ : ℝ) * (1 / ‖(ρ : ℂ)‖ ^ (2 + m))\n      = (zeroMult ρ : ℝ) * ((1 / ‖(ρ : ℂ)‖ ^ 2) * (1 / ‖(ρ : ℂ)‖ ^ m)) := by\n        rw [pow_add, ← one_div_mul_one_div]\n    _ ≤ (zeroMult ρ : ℝ) * ((1 / ‖(ρ : ℂ)‖ ^ 2) * (1 / δ ^ m)) := by\n        apply mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _)\n        apply mul_le_mul_of_nonneg_left _ (by positivity : (0 : ℝ) ≤ 1 / ‖(ρ : ℂ)‖ ^ 2)\n        exact one_div_le_one_div_of_le (pow_pos hδ m) (pow_le_pow_left₀ hδ.le hρδ m)\n    _ = (1 / δ) ^ m * ((zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ 2) := by\n        rw [div_pow, one_pow]\n        ring\n\n/-- The conjugation reindex: Σ mult·ρ̄^{−k} = Σ mult·ρ^{−k}. -/\nlemma tsum_mult_inv_pow_conj (k : ℕ) :\n    (∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, (zeroMult ρ : ℂ) * (1 / ((starRingEnd ℂ) (ρ : ℂ))) ^ k) =\n      ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, (zeroMult ρ : ℂ) * (1 / (ρ : ℂ)) ^ k := by\n  have h := Equiv.tsum_eq conjZeroEquiv\n    (fun σ : {σ : ℂ // IsNontrivialZero σ} => (zeroMult σ : ℂ) * (1 / (σ : ℂ)) ^ k)\n  rw [← h]\n  apply tsum_congr\n  intro ρ\n  have e1 : ((conjZeroEquiv ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ) = (starRingEnd ℂ) (ρ : ℂ) :=\n    rfl\n  rw [e1, zeroMult_conj ρ.2]\n\n/-- The conj-summability transfer. -/\nlemma summable_mult_inv_pow_conj {k : ℕ} (hk : 2 ≤ k) :\n    Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n      (zeroMult ρ : ℂ) * (1 / ((starRingEnd ℂ) (ρ : ℂ))) ^ k) := by\n  have e : (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n      (zeroMult ρ : ℂ) * (1 / ((starRingEnd ℂ) (ρ : ℂ))) ^ k) =\n      fun ρ => (fun σ : {σ : ℂ // IsNontrivialZero σ} => (zeroMult σ : ℂ) * (1 / (σ : ℂ)) ^ k)\n        (conjZeroEquiv ρ) := by\n    funext ρ\n    have e1 : ((conjZeroEquiv ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ) = (starRingEnd ℂ) (ρ : ℂ) :=\n      rfl\n    rw [e1, zeroMult_conj ρ.2]\n  rw [e]\n  exact (Equiv.summable_iff conjZeroEquiv _).mpr (summable_mult_inv_pow hk)\n\n/-- **The unpaired form** (k ≥ 2): the paired sum collapses to the\nunpaired sum by conj-invariance: sigmaP k = ½(S + S) = S. -/\nlemma sigmaP_eq_unpaired {k : ℕ} (hk : 2 ≤ k) :\n    sigmaP k = ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, (zeroMult ρ : ℂ) * (1 / (ρ : ℂ)) ^ k := by\n  have hs1 := summable_mult_inv_pow hk\n  have hs2 := summable_mult_inv_pow_conj hk\n  have step : ∑' ρ, sigmaSlice k ρ = ∑' ρ, (1 / 2 : ℂ) *\n      ((zeroMult ρ : ℂ) * (1 / (ρ : ℂ)) ^ k +\n        (zeroMult ρ : ℂ) * (1 / ((starRingEnd ℂ) (ρ : ℂ))) ^ k) := by\n    apply tsum_congr\n    intro ρ\n    rw [sigmaSlice]\n    ring\n  rw [sigmaP, step, tsum_mul_left, tsum_add hs1 hs2, tsum_mult_inv_pow_conj k]\n  ring\n\n/-- The reflected master summability: Σ mult/‖1−ρ‖² (reindex transfer). -/\nlemma summable_mult_div_norm_sq_one_sub :\n    Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n      (zeroMult ρ : ℝ) / ‖(1 : ℂ) - (ρ : ℂ)‖ ^ 2) := by\n  have e : (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n      (zeroMult ρ : ℝ) / ‖(1 : ℂ) - (ρ : ℂ)‖ ^ 2) =\n      fun ρ => (fun σ : {σ : ℂ // IsNontrivialZero σ} => (zeroMult σ : ℝ) / ‖(σ : ℂ)‖ ^ 2)\n        (oneSubZeroEquiv ρ) := by\n    funext ρ\n    have e1 : ((oneSubZeroEquiv ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ) = 1 - (ρ : ℂ) := rfl\n    rw [e1, zeroMult_one_sub ρ.2.2.1 ρ.2.2.2]\n  rw [e]\n  exact (Equiv.summable_iff oneSubZeroEquiv _).mpr summable_mult_div_norm_sq\n\n/-- The AM-GM bound: mult/(‖ρ‖‖1−ρ‖) ≤ ½(mult/‖ρ‖² + mult/‖1−ρ‖²). -/\nlemma mult_div_norm_mul_norm_le (ρ : {ρ : ℂ // IsNontrivialZero ρ}) :\n    (zeroMult ρ : ℝ) / (‖(ρ : ℂ)‖ * ‖(1 : ℂ) - (ρ : ℂ)‖) ≤\n      (1 / 2) * ((zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ 2 +\n        (zeroMult ρ : ℝ) / ‖(1 : ℂ) - (ρ : ℂ)‖ ^ 2) := by\n  have hρ0 := norm_nontrivialZero_pos ρ\n  have h1ρ0 := norm_one_sub_nontrivialZero_pos ρ\n  have key : 2 / (‖(ρ : ℂ)‖ * ‖(1 : ℂ) - (ρ : ℂ)‖) ≤\n      1 / ‖(ρ : ℂ)‖ ^ 2 + 1 / ‖(1 : ℂ) - (ρ : ℂ)‖ ^ 2 := by\n    have h1 : (0 : ℝ) ≤ (1 / ‖(ρ : ℂ)‖ - 1 / ‖(1 : ℂ) - (ρ : ℂ)‖) ^ 2 := sq_nonneg _\n    have hexp : (1 / ‖(ρ : ℂ)‖ - 1 / ‖(1 : ℂ) - (ρ : ℂ)‖) ^ 2 =\n        1 / ‖(ρ : ℂ)‖ ^ 2 - 2 / (‖(ρ : ℂ)‖ * ‖(1 : ℂ) - (ρ : ℂ)‖) +\n          1 / ‖(1 : ℂ) - (ρ : ℂ)‖ ^ 2 := by\n      rw [sub_sq, div_pow, div_pow, one_pow, one_pow, one_div_mul_one_div, mul_one_div]\n    rw [hexp] at h1\n    linarith\n  calc (zeroMult ρ : ℝ) / (‖(ρ : ℂ)‖ * ‖(1 : ℂ) - (ρ : ℂ)‖)\n      = (zeroMult ρ : ℝ) / 2 * (2 / (‖(ρ : ℂ)‖ * ‖(1 : ℂ) - (ρ : ℂ)‖)) := by ring\n    _ ≤ (zeroMult ρ : ℝ) / 2 * (1 / ‖(ρ : ℂ)‖ ^ 2 + 1 / ‖(1 : ℂ) - (ρ : ℂ)‖ ^ 2) :=\n        mul_le_mul_of_nonneg_left key (div_nonneg (Nat.cast_nonneg _) (by norm_num))\n    _ = (1 / 2) * ((zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ 2 +\n        (zeroMult ρ : ℝ) / ‖(1 : ℂ) - (ρ : ℂ)‖ ^ 2) := by ring\n\n/-- The mixed family Σ mult/(ρ(1−ρ)) is absolutely summable. -/\nlemma summable_mult_one_div_mul_one_sub :\n    Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n      (zeroMult ρ : ℂ) * (1 / ((ρ : ℂ) * (1 - (ρ : ℂ))))) := by\n  have hsum := summable_mult_div_norm_sq.add summable_mult_div_norm_sq_one_sub\n  apply Summable.of_norm_bounded (hsum.mul_left (1 / 2))\n  intro ρ\n  rw [norm_mul, norm_div, norm_one, RCLike.norm_natCast, norm_mul]\n  exact mult_div_norm_mul_norm_le ρ\n\n/-- The V-family is absolutely summable (1/ρ̄ − 1/(1−ρ) = O(‖ρ‖⁻¹‖1−ρ‖⁻¹)). -/\nlemma summable_mult_vTerm :\n    Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n      (zeroMult ρ : ℂ) * (1 / ((starRingEnd ℂ) (ρ : ℂ)) - 1 / (1 - (ρ : ℂ)))) := by\n  have hsum := summable_mult_div_norm_sq.add summable_mult_div_norm_sq_one_sub\n  apply Summable.of_norm_bounded (hsum.mul_left (1 / 2))\n  intro ρ\n  have hρ0 := norm_nontrivialZero_pos ρ\n  have h1ρ0 := norm_one_sub_nontrivialZero_pos ρ\n  have hconj : ‖((starRingEnd ℂ) (ρ : ℂ))‖ = ‖(ρ : ℂ)‖ := by\n    rw [starRingEnd_apply, Complex.norm_conj]\n  have hid : 1 / ((starRingEnd ℂ) (ρ : ℂ)) - 1 / (1 - (ρ : ℂ)) =\n      ((1 : ℂ) - (ρ : ℂ) - (starRingEnd ℂ) (ρ : ℂ)) /\n        (((starRingEnd ℂ) (ρ : ℂ)) * (1 - (ρ : ℂ))) := by\n    field_simp [ne_of_gt hρ0, ne_of_gt h1ρ0]\n    ring\n  have hnum : ‖(1 : ℂ) - (ρ : ℂ) - (starRingEnd ℂ) (ρ : ℂ)‖ ≤ 1 := by\n    have e : (1 : ℂ) - (ρ : ℂ) - (starRingEnd ℂ) (ρ : ℂ) = ((1 - 2 * (ρ : ℂ).re : ℝ) : ℂ) := by\n      rw [sub_sub, Complex.add_conj]\n      push_cast\n      ring\n    rw [e, Complex.norm_real, Real.norm_eq_abs, abs_le]\n    have hre0 := ρ.2.2.1\n    have hre1 := ρ.2.2.2\n    constructor <;> linarith\n  rw [norm_mul, hid, norm_div, norm_mul, hconj, RCLike.norm_natCast]\n  calc (zeroMult ρ : ℝ) * (‖(1 : ℂ) - (ρ : ℂ) - (starRingEnd ℂ) (ρ : ℂ)‖ /\n        (‖(ρ : ℂ)‖ * ‖(1 : ℂ) - (ρ : ℂ)‖))\n      ≤ (zeroMult ρ : ℝ) * (1 / (‖(ρ : ℂ)‖ * ‖(1 : ℂ) - (ρ : ℂ)‖)) := by\n        apply mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _)\n        exact div_le_div_of_nonneg_right hnum\n          (mul_pos hρ0 h1ρ0) |>.trans_eq (one_div _) |>.trans_eq' rfl\n    _ = (zeroMult ρ : ℝ) / (‖(ρ : ℂ)‖ * ‖(1 : ℂ) - (ρ : ℂ)‖) := by ring\n    _ ≤ (1 / 2) * ((zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ 2 +\n          (zeroMult ρ : ℝ) / ‖(1 : ℂ) - (ρ : ℂ)‖ ^ 2) := mult_div_norm_mul_norm_le ρ\n\n/-- **The V-sum vanishes**: the conj reindex gives V = W and the reflect\nreindex gives W = −V. -/\nlemma vTerm_tsum_eq_zero :\n    (∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},\n      (zeroMult ρ : ℂ) * (1 / ((starRingEnd ℂ) (ρ : ℂ)) - 1 / (1 - (ρ : ℂ)))) = 0 := by\n  set V := ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},\n      (zeroMult ρ : ℂ) * (1 / ((starRingEnd ℂ) (ρ : ℂ)) - 1 / (1 - (ρ : ℂ))) with hV\n  have h1 : V = ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},\n      (zeroMult ρ : ℂ) * (1 / (ρ : ℂ) - 1 / (1 - (starRingEnd ℂ) (ρ : ℂ))) := by\n    have h := Equiv.tsum_eq conjZeroEquiv (fun σ : {σ : ℂ // IsNontrivialZero σ} =>\n      (zeroMult σ : ℂ) * (1 / ((starRingEnd ℂ) (σ : ℂ)) - 1 / (1 - (σ : ℂ))))\n    rw [hV, ← h]\n    apply tsum_congr\n    intro ρ\n    have e1 : ((conjZeroEquiv ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ) = (starRingEnd ℂ) (ρ : ℂ) :=\n      rfl\n    rw [e1, zeroMult_conj ρ.2]\n    congr 1\n    simp [starRingEnd_apply]\n  have h2 : (∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},\n      (zeroMult ρ : ℂ) * (1 / (ρ : ℂ) - 1 / (1 - (starRingEnd ℂ) (ρ : ℂ)))) = -V := by\n    have h := Equiv.tsum_eq oneSubZeroEquiv (fun σ : {σ : ℂ // IsNontrivialZero σ} =>\n      (zeroMult σ : ℂ) * (1 / (σ : ℂ) - 1 / (1 - (starRingEnd ℂ) (σ : ℂ))))\n    rw [← h]\n    rw [hV, ← tsum_neg]\n    apply tsum_congr\n    intro ρ\n    have e1 : ((oneSubZeroEquiv ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ) = 1 - (ρ : ℂ) := rfl\n    rw [e1, zeroMult_one_sub ρ.2.2.1 ρ.2.2.2]\n    have e2 : (1 : ℂ) - (starRingEnd ℂ) (1 - (ρ : ℂ)) = (starRingEnd ℂ) (ρ : ℂ) := by\n      rw [map_sub, map_one, sub_sub_cancel]\n    rw [e2]\n    ring\n  have h3 : V = -V := h1.trans h2\n  exact eq_zero_of_neg_eq h3.symm\n\n/-- The first family (1/ρ + 1/ρ̄) is summable (the sigmaSlice 1 form). -/\nlemma summable_mult_fst :\n    Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n      (zeroMult ρ : ℂ) * (1 / (ρ : ℂ) + 1 / ((starRingEnd ℂ) (ρ : ℂ)))) := by\n  apply (sigmaSlice_summable 1 le_rfl).congr\n  intro ρ\n  rw [sigmaSlice, pow_one, pow_one]\n  ring\n\n/-- The second family (1/ρ + 1/(1−ρ)) is summable (the mixed form). -/\nlemma summable_mult_snd :\n    Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n      (zeroMult ρ : ℂ) * (1 / (ρ : ℂ) + 1 / (1 - (ρ : ℂ)))) := by\n  apply summable_mult_one_div_mul_one_sub.congr\n  intro ρ\n  have hρ0 := nontrivialZero_ne_zero ρ\n  have h1ρ := one_sub_nontrivialZero_ne_zero ρ\n  congr 1\n  field_simp [hρ0, h1ρ]\n  ring\n\n/-- **Twice σ₁ is the mixed series**: 2·sigmaP 1 = Σ mult/(ρ(1−ρ)).\nThe two pairings differ by V = 0. -/\nlemma two_mul_sigmaP_one :\n    (2 : ℂ) * sigmaP 1 = ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},\n      (zeroMult ρ : ℂ) * (1 / ((ρ : ℂ) * (1 - (ρ : ℂ)))) := by\n  have h1 : (2 : ℂ) * sigmaP 1 = ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},\n      (zeroMult ρ : ℂ) * (1 / (ρ : ℂ) + 1 / ((starRingEnd ℂ) (ρ : ℂ))) := by\n    rw [sigmaP, ← tsum_mul_left]\n    apply tsum_congr\n    intro ρ\n    rw [sigmaSlice, pow_one, pow_one]\n    ring\n  have h2 : (∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},\n      (zeroMult ρ : ℂ) * (1 / ((ρ : ℂ) * (1 - (ρ : ℂ))))) =\n      ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},\n        (zeroMult ρ : ℂ) * (1 / (ρ : ℂ) + 1 / (1 - (ρ : ℂ))) := by\n    apply tsum_congr\n    intro ρ\n    have hρ0 := nontrivialZero_ne_zero ρ\n    have h1ρ := one_sub_nontrivialZero_ne_zero ρ\n    congr 1\n    field_simp [hρ0, h1ρ]\n    ring\n  have h3 : (∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},\n      (zeroMult ρ : ℂ) * (1 / (ρ : ℂ) + 1 / ((starRingEnd ℂ) (ρ : ℂ)))) -\n        (∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},\n          (zeroMult ρ : ℂ) * (1 / (ρ : ℂ) + 1 / (1 - (ρ : ℂ)))) =\n      ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},\n        (zeroMult ρ : ℂ) * (1 / ((starRingEnd ℂ) (ρ : ℂ)) - 1 / (1 - (ρ : ℂ))) := by\n    rw [← tsum_sub summable_mult_fst summable_mult_snd]\n    apply tsum_congr\n    intro ρ\n    ring\n  have hFst : (∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},\n      (zeroMult ρ : ℂ) * (1 / (ρ : ℂ) + 1 / ((starRingEnd ℂ) (ρ : ℂ)))) =\n      ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},\n        (zeroMult ρ : ℂ) * (1 / (ρ : ℂ) + 1 / (1 - (ρ : ℂ))) :=\n    sub_eq_zero.mp (by rw [h3]; exact vTerm_tsum_eq_zero)\n  rw [h1, hFst, ← h2]\n\n/-- **(M) at k = 1**: σ₁ = −gFun(0). Via 2σ₁ = seriesFun(1) =\ngFun(1) − B = −2·gFun(0). -/\nlemma sigmaP_one_eq_neg_gFun_zero (hZC : ZeroCountProp) : sigmaP 1 = -gFun 0 := by\n  have h2 := two_mul_sigmaP_one\n  rw [← seriesFun_one] at h2\n  have hg1 := gFun_one hZC\n  have hg0 := gFun_zero hZC\n  have hfe := gFun_one_eq_neg\n  linear_combination (h2 - hg1 + hg0 + hfe) / 2\n\nend NguyenRH1"},"extra_content":null}]