← Session 28 — ii′-5e: partial-fraction identity (zero series + F entire)
thinking (331 chars)
`Metric.mem_ball_self` ✓, and importantly LiContour line 489 shows the exact final pattern: `(hd.analyticOnNhd Metric.isOpen_ball) (-2) (Metric.mem_ball_self zero_lt_one)` — AnalyticOnNhd applied to point + membership gives AnalyticAt ✓. And `Metric.isOpen_ball` is the right qualified name.
Now I have everything. Write the file.
All names verified (including the exact `hd.analyticOnNhd Metric.isOpen_ball ... mem_ball_self` closing pattern from LiContour). Writing the file now.
tool: Write
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSeries.lean",
"content": "/-\nNguyenRH1/LiSeries.lean \u2014 tier ii\u2032 sub-stage ii\u2032-5e-iii (D-068 \u00a73):\nthe zero-side partial-fraction series\n\n seriesFun s := \u2211' \u03c1 : {\u03c1 // IsNontrivialZero \u03c1}, (zeroMult \u03c1 : \u2102)\u00b7(1/(s\u2212\u03c1) + 1/\u03c1)\n\nand its three structural properties:\n\n(\u00a71\u20132) ABSOLUTE SUMMABILITY at every s (`seriesSummable`): the tail bound\n \u20161/(s\u2212\u03c1) + 1/\u03c1\u2016 = \u2016s\u2016/(\u2016\u03c1\u2016\u00b7\u2016s\u2212\u03c1\u2016) \u2264 2\u2016s\u2016/\u2016\u03c1\u2016\u00b2 (for 2 \u2264 \u2016\u03c1\u2016, 2\u2016s\u2016 \u2264 \u2016\u03c1\u2016)\n feeds the ii\u2032-1a dominator chain (the comparison\n 1 + \u2016\u03b3_\u03c1\u2016\u00b2 \u2264 (17/12)\u00b7\u2016\u03c1\u2016\u00b2 on the tail, then Zeta23\n `WeilEF.zero_sum_inv_sq`); the head is a finite subtype sum\n (`finite_subtype_norm_lt`, the ii\u2032-1a compact-finiteness pattern).\n\n(\u00a73\u20134) ANALYTICITY off the zeros (`seriesFun_analyticOnNhd`): around any\n s\u2080 that is not a nontrivial zero there is a ball avoiding the\n nontrivial zeros (`exists_ball_avoid_nontrivialZeros`: continuity of \u03b6\n where \u03b6 s\u2080 \u2260 0; the order normal form where \u03b6 s\u2080 = 0, s\u2080 \u2260 1; the\n zetaA factorization at s\u2080 = 1), and on that ball the series converges\n UNIFORMLY (Weierstrass M-test,\n `HasSumUniformlyOn.of_norm_le_summable_eventually`) with analytic\n partial sums \u2014 the journal-020/021-banked locally-uniform \u27f9 analytic\n pattern.\n\n(\u00a75) ISOLATION (`nontrivialZero_isolated`: minimum-distance over the\n finite ball) and the reduced series `seriesFunSub \u03c1\u2080` (the \u03c1\u2080-term\n zeroed out): analytic AT \u03c1\u2080 (`seriesFunSub_analyticAt`), so both the\n term subtraction s \u21a6 seriesFun s \u2212 seriesTerm s \u03c1\u2080 and the polar\n subtraction s \u21a6 seriesFun s \u2212 mult(\u03c1\u2080)/(s\u2212\u03c1\u2080) are analytic at \u03c1\u2080\n (`seriesFun_sub_self_term_analyticAt`,\n `seriesFun_sub_polar_analyticAt`) \u2014 the inputs 5e-iv needs for the\n residue cancellation at the nontrivial zeros.\n\nArchive references: D-068 \u00a73, journal-015 (ii\u2032-1a dominator chain),\njournal-020/021 (Weierstrass-convergence pattern), journal-024 (the\ncompact-finiteness ball pattern).\n-/\nimport Mathlib\nimport Zeta23.Statement\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/-! ## 0. The series -/\n\n/-- The zero-series summand: mult(\u03c1)\u00b7(1/(s\u2212\u03c1) + 1/\u03c1) over the nontrivial\nzero subtype (the ii\u2032-1a encoding; D-068 \u00a73). -/\ndef seriesTerm (s : \u2102) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) : \u2102 :=\n (zeroMult \u03c1 : \u2102) * (1 / (s - (\u03c1 : \u2102)) + 1 / (\u03c1 : \u2102))\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 : \u2102) : \u2102 := \u2211' \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}, seriesTerm s \u03c1\n\n/-! ## 1. The norm comparison and the tail bound -/\n\n/-- For a nontrivial zero with 2 \u2264 \u2016\u03c1\u2016: 1 + \u2016\u03b3_\u03c1\u2016\u00b2 \u2264 (17/12)\u00b7\u2016\u03c1\u2016\u00b2.\nOn re \u03c1 \u2208 (0, 1): \u2016\u03b3\u2016\u00b2 = im\u00b2 + (1/2\u2212re)\u00b2 \u2264 im\u00b2 + 1/4, and\nim\u00b2 = \u2016\u03c1\u2016\u00b2 \u2212 re\u00b2 \u2265 4 \u2212 1 = 3 gives 5/4 \u2264 (5/12)\u00b7im\u00b2. -/\nlemma one_add_normSq_gammaOf_le (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1})\n (h\u03c1 : (2 : \u211d) \u2264 \u2016(\u03c1 : \u2102)\u2016) :\n 1 + Complex.normSq (gammaOf (\u03c1 : \u2102)) \u2264 17 / 12 * \u2016(\u03c1 : \u2102)\u2016 ^ 2 := by\n have hz := \u03c1.2\n have hre0 : 0 < (\u03c1 : \u2102).re := hz.2.1\n have hre1 : (\u03c1 : \u2102).re < 1 := hz.2.2\n have hnorm : \u2016(\u03c1 : \u2102)\u2016 ^ 2 = (\u03c1 : \u2102).re ^ 2 + (\u03c1 : \u2102).im ^ 2 := by\n rw [\u2190 Complex.normSq_eq_norm_sq, Complex.normSq_apply]\n ring\n have hgam : Complex.normSq (gammaOf (\u03c1 : \u2102))\n = (\u03c1 : \u2102).im ^ 2 + (1 / 2 - (\u03c1 : \u2102).re) ^ 2 := by\n rw [Complex.normSq_apply, WeilEF.gammaOf_re, WeilEF.gammaOf_im]\n ring\n have h\u03c1sq : 4 \u2264 \u2016(\u03c1 : \u2102)\u2016 ^ 2 := by nlinarith [h\u03c1, norm_nonneg (\u03c1 : \u2102)]\n have hre2 : (\u03c1 : \u2102).re ^ 2 \u2264 1 := by nlinarith [hre0, hre1]\n have him2 : 3 \u2264 (\u03c1 : \u2102).im ^ 2 := by nlinarith [h\u03c1sq, hre2]\n have hquarter : (1 / 2 - (\u03c1 : \u2102).re) ^ 2 \u2264 1 / 4 := by nlinarith [hre0, hre1]\n rw [hgam, hnorm]\n nlinarith [him2, hquarter, sq_nonneg (\u03c1 : \u2102).re]\n\n/-- The key algebra: 1/(s\u2212\u03c1) + 1/\u03c1 = s/(\u03c1\u00b7(s\u2212\u03c1)). -/\nlemma one_div_sub_add_one_div {s \u03c1 : \u2102} (h0 : \u03c1 \u2260 0) (h1 : s - \u03c1 \u2260 0) :\n 1 / (s - \u03c1) + 1 / \u03c1 = s / (\u03c1 * (s - \u03c1)) := by\n have h2 : \u03c1 * (s - \u03c1) \u2260 0 := mul_ne_zero h0 h1\n field_simp\n ring\n\n/-- Tail bound: for 2 \u2264 \u2016\u03c1\u2016 and 2\u2016s\u2016 \u2264 \u2016\u03c1\u2016,\n\u2016seriesTerm s \u03c1\u2016 \u2264 (17/6)\u00b7\u2016s\u2016\u00b7mult/(1+\u2016\u03b3_\u03c1\u2016\u00b2). -/\nlemma seriesTerm_norm_le {s : \u2102} (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1})\n (h\u03c12 : (2 : \u211d) \u2264 \u2016(\u03c1 : \u2102)\u2016) (hs\u03c1 : 2 * \u2016s\u2016 \u2264 \u2016(\u03c1 : \u2102)\u2016) :\n \u2016seriesTerm s \u03c1\u2016 \u2264\n 17 / 6 * \u2016s\u2016 * ((zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102)))) := by\n have h0 : (\u03c1 : \u2102) \u2260 0 := by\n intro h; rw [h, norm_zero] at h\u03c12; norm_num at h\u03c12\n have h\u03c1pos : (0 : \u211d) < \u2016(\u03c1 : \u2102)\u2016 := norm_pos_iff.mpr h0\n have hsr : \u2016(\u03c1 : \u2102)\u2016 / 2 \u2264 \u2016s - (\u03c1 : \u2102)\u2016 := by\n have h := abs_norm_sub_norm_le s (\u03c1 : \u2102)\n rw [abs_le] at h\n linarith [h.1]\n have h1 : s - (\u03c1 : \u2102) \u2260 0 := by\n intro h; rw [h, norm_zero] at hsr; linarith\n have hcomp := one_add_normSq_gammaOf_le \u03c1 h\u03c12\n have hg0 : (0 : \u211d) < 1 + Complex.normSq (gammaOf (\u03c1 : \u2102)) := by\n have h := Complex.normSq_nonneg (gammaOf (\u03c1 : \u2102)); linarith\n have halg := one_div_sub_add_one_div h0 h1\n have hden : \u2016(\u03c1 : \u2102)\u2016 ^ 2 / 2 \u2264 \u2016(\u03c1 : \u2102)\u2016 * \u2016s - (\u03c1 : \u2102)\u2016 := by\n nlinarith [mul_le_mul_of_nonneg_left hsr h\u03c1pos.le]\n have hden0 : (0 : \u211d) < \u2016(\u03c1 : \u2102)\u2016 * \u2016s - (\u03c1 : \u2102)\u2016 :=\n mul_pos h\u03c1pos (by linarith [hsr, h\u03c1pos])\n have h\u03c1sq0 : (0 : \u211d) < \u2016(\u03c1 : \u2102)\u2016 ^ 2 := pow_pos h\u03c1pos 2\n have hfrac : \u2016s\u2016 / (\u2016(\u03c1 : \u2102)\u2016 * \u2016s - (\u03c1 : \u2102)\u2016) \u2264 2 * \u2016s\u2016 / \u2016(\u03c1 : \u2102)\u2016 ^ 2 := by\n rw [div_le_div_iff\u2080 hden0 h\u03c1sq0]\n nlinarith [hden, norm_nonneg s, h\u03c1pos]\n have hmul0 : (0 : \u211d) \u2264 (zeroMult \u03c1 : \u211d) := Nat.cast_nonneg _\n simp only [seriesTerm]\n rw [halg, norm_mul, RCLike.norm_natCast, norm_div, norm_mul]\n calc (zeroMult \u03c1 : \u211d) * (\u2016s\u2016 / (\u2016(\u03c1 : \u2102)\u2016 * \u2016s - (\u03c1 : \u2102)\u2016))\n \u2264 (zeroMult \u03c1 : \u211d) * (2 * \u2016s\u2016 / \u2016(\u03c1 : \u2102)\u2016 ^ 2) :=\n mul_le_mul_of_nonneg_left hfrac hmul0\n _ = 2 * \u2016s\u2016 * (zeroMult \u03c1 : \u211d) / \u2016(\u03c1 : \u2102)\u2016 ^ 2 := by ring\n _ \u2264 17 / 6 * \u2016s\u2016 * ((zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102)))) := by\n have hR : 17 / 6 * \u2016s\u2016 * ((zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102))))\n = (17 / 6 * \u2016s\u2016 * (zeroMult \u03c1 : \u211d)) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102))) := by\n ring\n rw [hR, div_le_div_iff\u2080 h\u03c1sq0 hg0]\n have hkey : 2 * (1 + Complex.normSq (gammaOf (\u03c1 : \u2102)))\n \u2264 17 / 6 * \u2016(\u03c1 : \u2102)\u2016 ^ 2 := by linarith [hcomp]\n calc 2 * \u2016s\u2016 * (zeroMult \u03c1 : \u211d) * (1 + Complex.normSq (gammaOf (\u03c1 : \u2102)))\n = (\u2016s\u2016 * (zeroMult \u03c1 : \u211d)) * (2 * (1 + Complex.normSq (gammaOf (\u03c1 : \u2102)))) := by\n ring\n _ \u2264 (\u2016s\u2016 * (zeroMult \u03c1 : \u211d)) * (17 / 6 * \u2016(\u03c1 : \u2102)\u2016 ^ 2) :=\n mul_le_mul_of_nonneg_left hkey (by positivity)\n _ = 17 / 6 * \u2016s\u2016 * (zeroMult \u03c1 : \u211d) * \u2016(\u03c1 : \u2102)\u2016 ^ 2 := by ring\n\n/-! ## 2. Summability -/\n\n/-- The subtype elements in a closed ball form a finite set (the ii\u2032-1a\ncompact-finiteness pattern: nontrivial zeros \u2286 `riemannZetaZeros`,\nfinite in compacts by Mathlib's discreteness of the zero set). -/\nlemma finite_subtype_norm_lt (R : \u211d) :\n {\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} | \u2016(\u03c1 : \u2102)\u2016 < R}.Finite := by\n have hcomp : IsCompact (Metric.closedBall (0 : \u2102) R) := isCompact_closedBall _ _\n have hzeros : (Metric.closedBall (0 : \u2102) R) \u2229 {\u03c1 : \u2102 | IsNontrivialZero \u03c1}\n \u2286 (Metric.closedBall (0 : \u2102) R) \u2229 riemannZetaZeros := by\n intro z hz\n exact \u27e8hz.1, hz.2.1\u27e9\n have hfin2 := (hcomp.inter_riemannZetaZeros_finite).subset hzeros\n have himg : (Subtype.val '' {\u03c1 : {\u03c1 // IsNontrivialZero \u03c1} | \u2016(\u03c1 : \u2102)\u2016 < R}).Finite := by\n apply hfin2.subset\n rintro z \u27e8\u03c1, h\u03c1, rfl\u27e9\n refine \u27e8?_, \u03c1.2\u27e9\n simp only [Metric.mem_closedBall, dist_zero_right]\n exact le_of_lt h\u03c1\n exact Set.Finite.of_finite_image himg (Subtype.val_injective.injOn)\n\n/-- The M-test majorant family, summable by Zeta23's `zero_sum_inv_sq`. -/\nlemma seriesTerm_summable_majorant (M : \u211d) :\n Summable (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} =>\n 17 / 6 * M * ((zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102))))) :=\n (WeilEF.zero_sum_inv_sq zetaSeam).mul_left _\n\n/-- The series is absolutely summable at every s (the ii\u2032-1a D-trick:\ndominator (17/6)(\u2016s\u2016+1)\u00b7mult/(1+\u2016\u03b3\u2016\u00b2) on the tail \u2016\u03c1\u2016 \u2265 max 2 (2\u2016s\u2016),\nfinite head by `finite_subtype_norm_lt`). -/\ntheorem seriesSummable (s : \u2102) :\n Summable (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => seriesTerm s \u03c1) := by\n set R\u2080 : \u211d := max 2 (2 * \u2016s\u2016) with hR\u2080\n have hR\u20802 : (2 : \u211d) \u2264 R\u2080 := le_max_left _ _\n have hR\u2080s : 2 * \u2016s\u2016 \u2264 R\u2080 := le_max_right _ _\n set C : \u211d := 17 / 6 * (\u2016s\u2016 + 1) with hC\n have hbase : Summable (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} =>\n C * ((zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102))))) :=\n (WeilEF.zero_sum_inv_sq zetaSeam).mul_left C\n set D : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} \u2192 \u211d := fun \u03c1 =>\n if R\u2080 \u2264 \u2016(\u03c1 : \u2102)\u2016 then\n C * ((zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102))))\n else \u2016seriesTerm s \u03c1\u2016 with hDdef\n have hfin : {\u03c1 : {\u03c1 // IsNontrivialZero \u03c1} | \u00ac (R\u2080 \u2264 \u2016(\u03c1 : \u2102)\u2016)}.Finite := by\n apply (finite_subtype_norm_lt R\u2080).subset\n intro \u03c1 h\u03c1\n exact not_le.mp h\u03c1\n have hE : Summable (fun \u03c1 : {\u03c1 // IsNontrivialZero \u03c1} =>\n D \u03c1 - C * ((zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102))))) := by\n apply summable_of_hasFiniteSupport\n apply hfin.subset\n intro \u03c1 h\u03c1\n simp only [Function.mem_support, ne_eq] at h\u03c1\n by_contra hball\n apply h\u03c1\n have hball' : R\u2080 \u2264 \u2016(\u03c1 : \u2102)\u2016 := 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 \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} =>\n C * ((zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102)))) +\n (D \u03c1 - C * ((zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102)))))) = D := by\n funext \u03c1\n ring\n rw [heq] at hsum\n exact hsum\n refine Summable.of_norm_bounded hD (fun \u03c1 => ?_)\n by_cases h\u03c1 : R\u2080 \u2264 \u2016(\u03c1 : \u2102)\u2016\n \u00b7 simp only [D, if_pos h\u03c1]\n have h2 : (2 : \u211d) \u2264 \u2016(\u03c1 : \u2102)\u2016 := hR\u20802.trans h\u03c1\n have hs2 : 2 * \u2016s\u2016 \u2264 \u2016(\u03c1 : \u2102)\u2016 := hR\u2080s.trans h\u03c1\n have h := seriesTerm_norm_le \u03c1 h2 hs2\n apply h.trans\n have hg0 : (0 : \u211d) \u2264 (zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102))) := by\n have hnn := Complex.normSq_nonneg (gammaOf (\u03c1 : \u2102))\n positivity\n have hC' : 17 / 6 * \u2016s\u2016 \u2264 C := by\n rw [hC]\n nlinarith [norm_nonneg s]\n exact mul_le_mul_of_nonneg_right hC' hg0\n \u00b7 simp only [D, if_neg h\u03c1, le_refl]\n\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 of \u03b6 where \u03b6 s\u2080 \u2260 0; the order\nnormal form (zeros isolated among \u03b6-zeros) where \u03b6 s\u2080 = 0, s\u2080 \u2260 1; the\nzetaA factorization (pole neighbourhood) at s\u2080 = 1. -/\nlemma exists_ball_avoid_nontrivialZeros (s\u2080 : \u2102) (hs\u2080 : \u00ac IsNontrivialZero s\u2080) :\n \u2203 \u03b4 : \u211d, 0 < \u03b4 \u2227 \u2200 \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}, (\u03c1 : \u2102) \u2209 Metric.ball s\u2080 \u03b4 := by\n by_cases h1 : s\u2080 = 1\n \u00b7 subst h1\n obtain \u27e8\u03b5, h\u03b5, hball\u27e9 := Metric.eventually_nhds_iff_ball.mp zetaA_ne_zero_near_one\n refine \u27e8\u03b5, h\u03b5, fun \u03c1 h\u03c1 => ?_\u27e9\n have h\u03c11 : (\u03c1 : \u2102) \u2260 1 := by\n intro h\n have hlt : (\u03c1 : \u2102).re < 1 := \u03c1.2.2.2\n rw [h, Complex.one_re] at hlt\n exact lt_irrefl 1 hlt\n have hz := hball (\u03c1 : \u2102) h\u03c1\n rw [zetaA_apply h\u03c11, \u03c1.2.1, mul_zero] at hz\n exact hz rfl\n \u00b7 by_cases h0 : riemannZeta s\u2080 = 0\n \u00b7 obtain \u27e8h, hh, hh0, hfh\u27e9 :=\n (analyticAt_riemannZeta h1).analyticOrderAt_ne_top.mp (zeta_order_ne_top_of_ne h1)\n obtain \u27e8\u03b5\u2081, h\u03b5\u2081, hball\u2081\u27e9 := Metric.eventually_nhds_iff_ball.mp\n (hh.continuousAt.eventually_ne hh0)\n obtain \u27e8\u03b5\u2082, h\u03b5\u2082, hball\u2082\u27e9 := Metric.eventually_nhds_iff_ball.mp hfh\n refine \u27e8min \u03b5\u2081 \u03b5\u2082, lt_min h\u03b5\u2081 h\u03b5\u2082, fun \u03c1 h\u03c1 => ?_\u27e9\n have hmem1 : (\u03c1 : \u2102) \u2208 Metric.ball s\u2080 \u03b5\u2081 := Metric.ball_subset_ball (min_le_left _ _) h\u03c1\n have hmem2 : (\u03c1 : \u2102) \u2208 Metric.ball s\u2080 \u03b5\u2082 := Metric.ball_subset_ball (min_le_right _ _) h\u03c1\n have heq := hball\u2082 (\u03c1 : \u2102) hmem2\n have hne : h (\u03c1 : \u2102) \u2260 0 := hball\u2081 (\u03c1 : \u2102) hmem1\n by_cases h\u03c1s : (\u03c1 : \u2102) = s\u2080\n \u00b7 exact hs\u2080 (h\u03c1s \u25b8 \u03c1.2)\n \u00b7 have hpow : ((\u03c1 : \u2102) - s\u2080) ^ analyticOrderNatAt riemannZeta s\u2080 \u2260 0 :=\n pow_ne_zero _ (sub_ne_zero.mpr h\u03c1s)\n have hz : riemannZeta (\u03c1 : \u2102) \u2260 0 := by\n rw [heq, smul_eq_mul]\n exact mul_ne_zero hpow hne\n exact hz \u03c1.2.1\n \u00b7 obtain \u27e8\u03b5, h\u03b5, hball\u27e9 := Metric.eventually_nhds_iff_ball.mp\n ((analyticAt_riemannZeta h1).continuousAt.eventually_ne h0)\n refine \u27e8\u03b5, h\u03b5, fun \u03c1 h\u03c1 => ?_\u27e9\n exact hball (\u03c1 : \u2102) h\u03c1 \u03c1.2.1\n\n/-! ## 4. Analyticity off the zeros -/\n\n/-- The series is analytic at every point that is not a nontrivial zero\n(Weierstrass M-test on an avoiding ball; the journal-020/021 pattern). -/\ntheorem seriesFun_analyticAt {s\u2080 : \u2102} (hs\u2080 : \u00ac IsNontrivialZero s\u2080) :\n AnalyticAt \u2102 seriesFun s\u2080 := by\n obtain \u27e8\u03b4, h\u03b4, hball\u27e9 := exists_ball_avoid_nontrivialZeros s\u2080 hs\u2080\n set M : \u211d := \u2016s\u2080\u2016 + \u03b4 with hM\n have hM0 : (0 : \u211d) \u2264 M := by rw [hM]; linarith [norm_nonneg s\u2080, h\u03b4.le]\n set R\u2080 : \u211d := max 2 (2 * M) with hR\u2080\n set u : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} \u2192 \u211d := fun \u03c1 =>\n 17 / 6 * M * ((zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102)))) with hu\n have hsum_u : Summable u := seriesTerm_summable_majorant M\n have hfu : \u2200\u1da0 \u03c1 in cofinite, \u2200 s \u2208 Metric.ball s\u2080 \u03b4, \u2016seriesTerm s \u03c1\u2016 \u2264 u \u03c1 := by\n rw [eventually_cofinite]\n apply (finite_subtype_norm_lt R\u2080).subset\n intro \u03c1 h\u03c1\n simp only [Set.mem_setOf_eq, not_forall] at h\u03c1\n by_contra hlt\n rw [not_lt] at hlt\n apply h\u03c1\n intro s hs\n have hsM : \u2016s\u2016 \u2264 M := by\n have hlt2 : \u2016s\u2016 < M := by\n calc \u2016s\u2016 \u2264 \u2016s - s\u2080\u2016 + \u2016s\u2080\u2016 := by\n nth_rewrite 1 [show s = (s - s\u2080) + s\u2080 from by ring]\n exact norm_add_le _ _\n _ < \u03b4 + \u2016s\u2080\u2016 := by\n have hmem := Metric.mem_ball.mp hs\n rw [dist_eq_norm] at hmem\n linarith\n _ = M := by rw [hM]; ring\n exact le_of_lt hlt2\n have h2 : (2 : \u211d) \u2264 \u2016(\u03c1 : \u2102)\u2016 := (le_max_left _ _).trans hlt\n have hs2 : 2 * \u2016s\u2016 \u2264 \u2016(\u03c1 : \u2102)\u2016 := by\n have h2M : 2 * \u2016s\u2016 \u2264 2 * M := by linarith\n exact (h2M.trans (le_max_right _ _)).trans hlt\n have h := seriesTerm_norm_le \u03c1 h2 hs2\n apply h.trans\n have hg0 : (0 : \u211d) \u2264 (zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102))) := by\n have hnn := Complex.normSq_nonneg (gammaOf (\u03c1 : \u2102))\n positivity\n have hle : 17 / 6 * \u2016s\u2016 \u2264 17 / 6 * M := by nlinarith [hsM, hM0, norm_nonneg s]\n exact mul_le_mul_of_nonneg_right hle hg0\n have hu' : HasSumUniformlyOn (fun \u03c1 => fun s : \u2102 => seriesTerm s \u03c1)\n (fun s => \u2211' \u03c1, seriesTerm s \u03c1) (Metric.ball s\u2080 \u03b4) :=\n HasSumUniformlyOn.of_norm_le_summable_eventually hsum_u hfu\n have htend : TendstoLocallyUniformlyOn\n (fun t : Finset {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => fun s => \u2211 \u03c1 \u2208 t, seriesTerm s \u03c1)\n (fun s => \u2211' \u03c1, seriesTerm s \u03c1) atTop (Metric.ball s\u2080 \u03b4) :=\n TendstoUniformlyOn.tendstoLocallyUniformlyOn\n (hasSumUniformlyOn_iff_tendstoUniformlyOn.mp hu')\n have hdiff : DifferentiableOn \u2102 (fun s => \u2211' \u03c1, seriesTerm s \u03c1)\n (Metric.ball s\u2080 \u03b4) := by\n apply htend.differentiableOn _ Metric.isOpen_ball\n apply Filter.Eventually.of_forall\n intro t s hs\n rw [show (fun s => \u2211 \u03c1 \u2208 t, seriesTerm s \u03c1) = \u2211 \u03c1 \u2208 t, (fun s => seriesTerm s \u03c1) from by\n funext s; simp [Finset.sum_apply]]\n apply DifferentiableAt.differentiableWithinAt\n apply DifferentiableAt.sum\n intro \u03c1 h\u03c1t\n have hs\u03c1 : s - (\u03c1 : \u2102) \u2260 0 := by\n have h\u03c1out : (\u03c1 : \u2102) \u2209 Metric.ball s\u2080 \u03b4 := hball \u03c1\n intro h\n apply h\u03c1out\n have heq : (\u03c1 : \u2102) = s := (sub_eq_zero.mp h).symm\n rw [heq]\n exact hs\n have h\u03c10 : (\u03c1 : \u2102) \u2260 0 := by\n intro h\n have hlt := \u03c1.2.2.1\n rw [h] at hlt\n simp at hlt\n have h1 : DifferentiableAt \u2102 (fun s : \u2102 => 1 / (s - (\u03c1 : \u2102))) s :=\n (differentiableAt_const (1 : \u2102)).div\n (differentiableAt_id.sub (differentiableAt_const _)) hs\u03c1\n have h2 : DifferentiableAt \u2102 (fun s : \u2102 => 1 / (\u03c1 : \u2102)) s := differentiableAt_const _\n show DifferentiableAt \u2102 (fun s => (zeroMult \u03c1 : \u2102) * (1 / (s - (\u03c1 : \u2102)) + 1 / (\u03c1 : \u2102))) s\n exact (h1.add h2).const_mul _\n have han : AnalyticOnNhd \u2102 (fun s => \u2211' \u03c1, seriesTerm s \u03c1) (Metric.ball s\u2080 \u03b4) :=\n hdiff.analyticOnNhd Metric.isOpen_ball\n exact han s\u2080 (Metric.mem_ball_self h\u03b4)\n\n/-- The series is analytic on the complement of the nontrivial zeros. -/\ntheorem seriesFun_analyticOnNhd :\n AnalyticOnNhd \u2102 seriesFun {s : \u2102 | \u00ac IsNontrivialZero s} :=\n fun s\u2080 hs\u2080 => seriesFun_analyticAt hs\u2080\n\n/-! ## 5. Isolation and the reduced series -/\n\n/-- Each nontrivial zero is isolated from the others (finiteness of the\nzero set in the unit ball + minimum distance). -/\ntheorem nontrivialZero_isolated (\u03c1\u2080 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) :\n \u2203 \u03b4 : \u211d, 0 < \u03b4 \u2227 \u2200 \u03c1\u2081 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}, \u03c1\u2081 \u2260 \u03c1\u2080 \u2192\n \u03b4 \u2264 \u2016(\u03c1\u2081 : \u2102) - (\u03c1\u2080 : \u2102)\u2016 := by\n have hcomp : IsCompact (Metric.closedBall (\u03c1\u2080 : \u2102) 1) := isCompact_closedBall _ _\n have hzeros : (Metric.closedBall (\u03c1\u2080 : \u2102) 1) \u2229 {\u03c1 : \u2102 | IsNontrivialZero \u03c1}\n \u2286 (Metric.closedBall (\u03c1\u2080 : \u2102) 1) \u2229 riemannZetaZeros := by\n intro z hz\n exact \u27e8hz.1, hz.2.1\u27e9\n have hfin : ((Metric.closedBall (\u03c1\u2080 : \u2102) 1) \u2229 {\u03c1 : \u2102 | IsNontrivialZero \u03c1}).Finite :=\n (hcomp.inter_riemannZetaZeros_finite).subset hzeros\n set S : Set {\u03c1 : \u2102 // IsNontrivialZero \u03c1} :=\n {\u03c1 | (\u03c1 : \u2102) \u2208 Metric.closedBall (\u03c1\u2080 : \u2102) 1 \u2227 \u03c1 \u2260 \u03c1\u2080} with hS\n have hSfin : S.Finite := by\n have himg : (Subtype.val '' S).Finite := by\n apply hfin.subset\n rintro z \u27e8\u03c1, \u27e8h\u03c1, -\u27e9, rfl\u27e9\n exact \u27e8h\u03c1, \u03c1.2\u27e9\n exact Set.Finite.of_finite_image himg (Subtype.val_injective.injOn)\n by_cases hne : S.Nonempty\n \u00b7 set d : Finset \u211d := hSfin.toFinset.image (fun \u03c1 => \u2016(\u03c1 : \u2102) - (\u03c1\u2080 : \u2102)\u2016) with hd\n have hdne : d.Nonempty := by\n obtain \u27e8\u03c1, h\u03c1\u27e9 := hne\n refine \u27e8\u2016(\u03c1 : \u2102) - (\u03c1\u2080 : \u2102)\u2016, ?_\u27e9\n rw [hd]\n exact Finset.mem_image.mpr \u27e8\u03c1, (Set.Finite.mem_toFinset hSfin).mpr h\u03c1, rfl\u27e9\n have hdpos : \u2200 x \u2208 d, 0 < x := by\n intro x hx\n rw [hd] at hx\n obtain \u27e8\u03c1, h\u03c1, rfl\u27e9 := Finset.mem_image.mp hx\n rw [Set.Finite.mem_toFinset] at h\u03c1\n have h1 : (\u03c1 : \u2102) \u2260 (\u03c1\u2080 : \u2102) := fun h => h\u03c1.2 (Subtype.ext h)\n exact norm_pos_iff.mpr (sub_ne_zero.mpr h1)\n have hmin0 : 0 < d.min' hdne := hdpos _ (Finset.min'_mem _ _)\n have hmin1 : d.min' hdne \u2264 1 := by\n have hm := Finset.min'_mem d hdne\n rw [hd] at hm\n obtain \u27e8\u03c1, h\u03c1, rfl\u27e9 := Finset.mem_image.mp hm\n rw [Set.Finite.mem_toFinset] at h\u03c1\n rw [Metric.mem_closedBall, dist_eq_norm] at h\u03c1\n exact h\u03c1.1\n refine \u27e8d.min' hdne / 2, half_pos hmin0, fun \u03c1\u2081 h\u03c1\u2081 => ?_\u27e9\n by_cases hmem : (\u03c1\u2081 : \u2102) \u2208 Metric.closedBall (\u03c1\u2080 : \u2102) 1\n \u00b7 have h1 : \u03c1\u2081 \u2208 S := \u27e8hmem, h\u03c1\u2081\u27e9\n have h2 : \u2016(\u03c1\u2081 : \u2102) - (\u03c1\u2080 : \u2102)\u2016 \u2208 d := by\n rw [hd]\n exact Finset.mem_image.mpr \u27e8\u03c1\u2081, (Set.Finite.mem_toFinset hSfin).mpr h1, rfl\u27e9\n have h3 : d.min' hdne \u2264 \u2016(\u03c1\u2081 : \u2102) - (\u03c1\u2080 : \u2102)\u2016 := Finset.min'_le _ _ h2\n linarith\n \u00b7 have h4 : 1 \u2264 \u2016(\u03c1\u2081 : \u2102) - (\u03c1\u2080 : \u2102)\u2016 := by\n by_contra h\n apply hmem\n rw [Metric.mem_closedBall, dist_eq_norm]\n exact le_of_lt (not_le.mp h)\n linarith\n \u00b7 refine \u27e81 / 2, by norm_num, fun \u03c1\u2081 h\u03c1\u2081 => ?_\u27e9\n by_contra h\n push_neg at h\n apply hne\n exact \u27e8\u03c1\u2081, \u27e8by\n rw [Metric.mem_closedBall, dist_eq_norm]\n linarith, h\u03c1\u2081\u27e9\u27e9\n\n/-- The reduced summand: the \u03c1\u2080-term zeroed out. -/\ndef seriesTermSub (\u03c1\u2080 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) (s : \u2102)\n (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) : \u2102 :=\n if \u03c1 = \u03c1\u2080 then 0 else seriesTerm s \u03c1\n\n/-- The reduced series (the \u03c1\u2080 polar term removed): analytic AT \u03c1\u2080\n(`seriesFunSub_analyticAt`). -/\ndef seriesFunSub (\u03c1\u2080 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) (s : \u2102) : \u2102 :=\n \u2211' \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}, seriesTermSub \u03c1\u2080 s \u03c1\n\nlemma seriesTermSub_norm_le (\u03c1\u2080 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) (s : \u2102)\n (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) : \u2016seriesTermSub \u03c1\u2080 s \u03c1\u2016 \u2264 \u2016seriesTerm s \u03c1\u2016 := by\n by_cases h : \u03c1 = \u03c1\u2080 <;> simp [seriesTermSub, h]\n\ntheorem seriesTermSub_summable (\u03c1\u2080 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) (s : \u2102) :\n Summable (seriesTermSub \u03c1\u2080 s) :=\n Summable.of_norm_bounded (seriesSummable s).norm (fun \u03c1 => seriesTermSub_norm_le \u03c1\u2080 s \u03c1)\n\nlemma single_summable (\u03c1\u2080 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) (s : \u2102) :\n Summable (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} =>\n if \u03c1 = \u03c1\u2080 then seriesTerm s \u03c1 else (0 : \u2102)) := by\n apply summable_of_hasFiniteSupport ((Set.finite_singleton \u03c1\u2080).subset ?_)\n intro \u03c1 h\u03c1\n rw [Function.mem_support, ne_eq] at h\u03c1\n by_contra h\n apply h\u03c1\n rw [if_neg (fun he => h (Set.mem_singleton_iff.mpr he))]\n\n/-- Pointwise split: seriesFun = seriesFunSub + the \u03c1\u2080-term (everywhere). -/\nlemma seriesFun_eq_sub_add (\u03c1\u2080 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) (s : \u2102) :\n seriesFun s = seriesFunSub \u03c1\u2080 s + seriesTerm s \u03c1\u2080 := by\n have hsingle : \u2211' \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1},\n (if \u03c1 = \u03c1\u2080 then seriesTerm s \u03c1 else (0 : \u2102)) = seriesTerm s \u03c1\u2080 := by\n rw [tsum_eq_single \u03c1\u2080 (fun \u03c1 h\u03c1 => if_neg h\u03c1)]\n exact if_pos rfl\n calc seriesFun s = \u2211' \u03c1, seriesTerm s \u03c1 := rfl\n _ = \u2211' \u03c1, (seriesTermSub \u03c1\u2080 s \u03c1 + (if \u03c1 = \u03c1\u2080 then seriesTerm s \u03c1 else (0 : \u2102))) := by\n apply tsum_congr\n intro \u03c1\n by_cases h : \u03c1 = \u03c1\u2080 <;> simp [seriesTermSub, h]\n _ = \u2211' \u03c1, seriesTermSub \u03c1\u2080 s \u03c1 + \u2211' \u03c1, (if \u03c1 = \u03c1\u2080 then seriesTerm s \u03c1 else (0 : \u2102)) :=\n Summable.tsum_add (seriesTermSub_summable \u03c1\u2080 s) (single_summable \u03c1\u2080 s)\n _ = seriesFunSub \u03c1\u2080 s + seriesTerm s \u03c1\u2080 := by rw [hsingle]\n\n/-- The series minus its \u03c1\u2080-term equals the reduced series (everywhere). -/\ntheorem seriesFun_sub_term (\u03c1\u2080 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) (s : \u2102) :\n seriesFun s - seriesTerm s \u03c1\u2080 = seriesFunSub \u03c1\u2080 s := by\n have h := seriesFun_eq_sub_add \u03c1\u2080 s\n rw [h]\n ring\n\n/-- The reduced series is analytic at \u03c1\u2080 (the other terms have no pole\nin the isolation ball; Weierstrass M-test as in \u00a74). -/\ntheorem seriesFunSub_analyticAt (\u03c1\u2080 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) :\n AnalyticAt \u2102 (seriesFunSub \u03c1\u2080) (\u03c1\u2080 : \u2102) := by\n obtain \u27e8\u03b4, h\u03b4, hiso\u27e9 := nontrivialZero_isolated \u03c1\u2080\n set \u03b4' : \u211d := \u03b4 / 2 with h\u03b4'\n have h\u03b4'0 : 0 < \u03b4' := half_pos h\u03b4\n set M : \u211d := \u2016(\u03c1\u2080 : \u2102)\u2016 + \u03b4' with hM\n have hM0 : (0 : \u211d) \u2264 M := by rw [hM]; linarith [norm_nonneg (\u03c1\u2080 : \u2102), h\u03b4'0.le]\n set R\u2080 : \u211d := max 2 (2 * M) with hR\u2080\n set u : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} \u2192 \u211d := fun \u03c1 =>\n 17 / 6 * M * ((zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102)))) with hu\n have hsum_u : Summable u := seriesTerm_summable_majorant M\n have hfu : \u2200\u1da0 \u03c1 in cofinite, \u2200 s \u2208 Metric.ball (\u03c1\u2080 : \u2102) \u03b4',\n \u2016seriesTermSub \u03c1\u2080 s \u03c1\u2016 \u2264 u \u03c1 := by\n rw [eventually_cofinite]\n apply (finite_subtype_norm_lt R\u2080).subset\n intro \u03c1 h\u03c1\n simp only [Set.mem_setOf_eq, not_forall] at h\u03c1\n by_contra hlt\n rw [not_lt] at hlt\n apply h\u03c1\n intro s hs\n have hsM : \u2016s\u2016 \u2264 M := by\n have hlt2 : \u2016s\u2016 < M := by\n calc \u2016s\u2016 \u2264 \u2016s - (\u03c1\u2080 : \u2102)\u2016 + \u2016(\u03c1\u2080 : \u2102)\u2016 := by\n nth_rewrite 1 [show s = (s - (\u03c1\u2080 : \u2102)) + (\u03c1\u2080 : \u2102) from by ring]\n exact norm_add_le _ _\n _ < \u03b4' + \u2016(\u03c1\u2080 : \u2102)\u2016 := by\n have hmem := Metric.mem_ball.mp hs\n rw [dist_eq_norm] at hmem\n linarith\n _ = M := by rw [hM]; ring\n exact le_of_lt hlt2\n by_cases h0 : \u03c1 = \u03c1\u2080\n \u00b7 rw [seriesTermSub, if_pos h0, norm_zero]\n have hg0 : (0 : \u211d) \u2264 (zeroMult \u03c1\u2080 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1\u2080 : \u2102))) := by\n have hnn := Complex.normSq_nonneg (gammaOf (\u03c1\u2080 : \u2102))\n positivity\n exact mul_nonneg (mul_nonneg (by norm_num) hM0) hg0\n \u00b7 have h2 : (2 : \u211d) \u2264 \u2016(\u03c1 : \u2102)\u2016 := (le_max_left _ _).trans hlt\n have hs2 : 2 * \u2016s\u2016 \u2264 \u2016(\u03c1 : \u2102)\u2016 := by\n have h2M : 2 * \u2016s\u2016 \u2264 2 * M := by linarith\n exact (h2M.trans (le_max_right _ _)).trans hlt\n rw [seriesTermSub, if_neg h0]\n have h := seriesTerm_norm_le \u03c1 h2 hs2\n apply h.trans\n have hg0 : (0 : \u211d) \u2264 (zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102))) := by\n have hnn := Complex.normSq_nonneg (gammaOf (\u03c1 : \u2102))\n positivity\n have hle : 17 / 6 * \u2016s\u2016 \u2264 17 / 6 * M := by nlinarith [hsM, hM0, norm_nonneg s]\n exact mul_le_mul_of_nonneg_right hle hg0\n have hu' : HasSumUniformlyOn (fun \u03c1 => fun s : \u2102 => seriesTermSub \u03c1\u2080 s \u03c1)\n (fun s => \u2211' \u03c1, seriesTermSub \u03c1\u2080 s \u03c1) (Metric.ball (\u03c1\u2080 : \u2102) \u03b4') :=\n HasSumUniformlyOn.of_norm_le_summable_eventually hsum_u hfu\n have htend : TendstoLocallyUniformlyOn\n (fun t : Finset {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => fun s => \u2211 \u03c1 \u2208 t, seriesTermSub \u03c1\u2080 s \u03c1)\n (fun s => \u2211' \u03c1, seriesTermSub \u03c1\u2080 s \u03c1) atTop (Metric.ball (\u03c1\u2080 : \u2102) \u03b4') :=\n TendstoUniformlyOn.tendstoLocallyUniformlyOn\n (hasSumUniformlyOn_iff_tendstoUniformlyOn.mp hu')\n have hdiff : DifferentiableOn \u2102 (fun s => \u2211' \u03c1, seriesTermSub \u03c1\u2080 s \u03c1)\n (Metric.ball (\u03c1\u2080 : \u2102) \u03b4') := by\n apply htend.differentiableOn _ Metric.isOpen_ball\n apply Filter.Eventually.of_forall\n intro t s hs\n rw [show (fun s => \u2211 \u03c1 \u2208 t, seriesTermSub \u03c1\u2080 s \u03c1)\n = \u2211 \u03c1 \u2208 t, (fun s => seriesTermSub \u03c1\u2080 s \u03c1) from by\n funext s; simp [Finset.sum_apply]]\n apply DifferentiableAt.differentiableWithinAt\n apply DifferentiableAt.sum\n intro \u03c1 h\u03c1t\n by_cases h0 : \u03c1 = \u03c1\u2080\n \u00b7 show DifferentiableAt \u2102 (fun s => if \u03c1 = \u03c1\u2080 then (0 : \u2102) else seriesTerm s \u03c1) s\n rw [if_pos h0]\n exact differentiableAt_const 0\n \u00b7 have hs\u03c1 : s - (\u03c1 : \u2102) \u2260 0 := by\n have hle : \u03b4 \u2264 \u2016(\u03c1 : \u2102) - (\u03c1\u2080 : \u2102)\u2016 := hiso \u03c1 h0\n have hlt : \u2016s - (\u03c1\u2080 : \u2102)\u2016 < \u03b4' := by\n have hmem := Metric.mem_ball.mp hs\n rwa [dist_eq_norm] at hmem\n intro hzero\n have h1 : \u2016(\u03c1 : \u2102) - (\u03c1\u2080 : \u2102)\u2016 \u2264 \u2016(\u03c1 : \u2102) - s\u2016 + \u2016s - (\u03c1\u2080 : \u2102)\u2016 := by\n nth_rewrite 1 [show (\u03c1 : \u2102) - (\u03c1\u2080 : \u2102) = ((\u03c1 : \u2102) - s) + (s - (\u03c1\u2080 : \u2102)) from by ring]\n exact norm_add_le _ _\n have h2 : \u2016(\u03c1 : \u2102) - s\u2016 = 0 := by\n have heq : s = (\u03c1 : \u2102) := sub_eq_zero.mp hzero\n rw [\u2190 heq, sub_self, norm_zero]\n rw [h2] at h1\n linarith [hle, hlt, h\u03b4, h\u03b4']\n have h\u03c10 : (\u03c1 : \u2102) \u2260 0 := by\n intro h\n have hlt := \u03c1.2.2.1\n rw [h] at hlt\n simp at hlt\n show DifferentiableAt \u2102 (fun s => if \u03c1 = \u03c1\u2080 then (0 : \u2102) else seriesTerm s \u03c1) s\n rw [if_neg h0]\n show DifferentiableAt \u2102\n (fun s => (zeroMult \u03c1 : \u2102) * (1 / (s - (\u03c1 : \u2102)) + 1 / (\u03c1 : \u2102))) s\n exact (((differentiableAt_const (1 : \u2102)).div\n (differentiableAt_id.sub (differentiableAt_const _)) hs\u03c1).add\n (differentiableAt_const _)).const_mul _\n have han : AnalyticOnNhd \u2102 (fun s => \u2211' \u03c1, seriesTermSub \u03c1\u2080 s \u03c1) (Metric.ball (\u03c1\u2080 : \u2102) \u03b4') :=\n hdiff.analyticOnNhd Metric.isOpen_ball\n exact han (\u03c1\u2080 : \u2102) (Metric.mem_ball_self h\u03b4'0)\n\n/-- The series with its \u03c1\u2080-term subtracted is analytic at \u03c1\u2080. -/\ntheorem seriesFun_sub_self_term_analyticAt (\u03c1\u2080 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) :\n AnalyticAt \u2102 (fun s => seriesFun s - seriesTerm s \u03c1\u2080) (\u03c1\u2080 : \u2102) := by\n apply AnalyticAt.congr (seriesFunSub_analyticAt \u03c1\u2080)\n exact Filter.Eventually.of_forall (fun s => (seriesFun_sub_term \u03c1\u2080 s).symm)\n\n/-- The polar subtraction form consumed by 5e-iv: the series minus\nmult(\u03c1\u2080)/(s\u2212\u03c1\u2080) is analytic at \u03c1\u2080 (the +mult/\u03c1\u2080 part is a constant). -/\ntheorem seriesFun_sub_polar_analyticAt (\u03c1\u2080 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) :\n AnalyticAt \u2102 (fun s => seriesFun s - (zeroMult (\u03c1\u2080 : \u2102) : \u2102) / (s - (\u03c1\u2080 : \u2102)))\n (\u03c1\u2080 : \u2102) := by\n have h := seriesFun_sub_self_term_analyticAt \u03c1\u2080\n have heq : (fun s => seriesFun s - (zeroMult (\u03c1\u2080 : \u2102) : \u2102) / (s - (\u03c1\u2080 : \u2102)))\n = (fun s => (seriesFun s - seriesTerm s \u03c1\u2080) + (zeroMult (\u03c1\u2080 : \u2102) : \u2102) / (\u03c1\u2080 : \u2102)) := by\n funext s\n simp only [seriesTerm]\n ring\n rw [heq]\n exact h.add analyticAt_const\n\nend\n\nend NguyenRH1\n"
}
raw content_json (database row)
[{"type":"thinking","thinking":"`Metric.mem_ball_self` ✓, and importantly LiContour line 489 shows the exact final pattern: `(hd.analyticOnNhd Metric.isOpen_ball) (-2) (Metric.mem_ball_self zero_lt_one)` — AnalyticOnNhd applied to point + membership gives AnalyticAt ✓. And `Metric.isOpen_ball` is the right qualified name.\n\nNow I have everything. Write the file.","signature":""},{"type":"text","text":"All names verified (including the exact `hd.analyticOnNhd Metric.isOpen_ball ... mem_ball_self` closing pattern from LiContour). Writing the file now."},{"type":"tool_use","id":"Write_47","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSeries.lean","content":"/-\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\n(§1–2) ABSOLUTE SUMMABILITY at every s (`seriesSummable`): the tail bound\n ‖1/(s−ρ) + 1/ρ‖ = ‖s‖/(‖ρ‖·‖s−ρ‖) ≤ 2‖s‖/‖ρ‖² (for 2 ≤ ‖ρ‖, 2‖s‖ ≤ ‖ρ‖)\n feeds the ii′-1a dominator chain (the comparison\n 1 + ‖γ_ρ‖² ≤ (17/12)·‖ρ‖² on the tail, then Zeta23\n `WeilEF.zero_sum_inv_sq`); the head is a finite subtype sum\n (`finite_subtype_norm_lt`, the ii′-1a compact-finiteness pattern).\n\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 (`exists_ball_avoid_nontrivialZeros`: continuity of ζ\n where ζ s₀ ≠ 0; the order normal form where ζ s₀ = 0, s₀ ≠ 1; the\n zetaA factorization at s₀ = 1), and on that ball the series converges\n UNIFORMLY (Weierstrass M-test,\n `HasSumUniformlyOn.of_norm_le_summable_eventually`) with analytic\n partial sums — the journal-020/021-banked locally-uniform ⟹ analytic\n pattern.\n\n(§5) ISOLATION (`nontrivialZero_isolated`: minimum-distance over the\n finite ball) and the reduced series `seriesFunSub ρ₀` (the ρ₀-term\n zeroed out): analytic AT ρ₀ (`seriesFunSub_analyticAt`), so both the\n term subtraction s ↦ seriesFun s − seriesTerm s ρ₀ and the polar\n subtraction s ↦ seriesFun s − mult(ρ₀)/(s−ρ₀) are analytic at ρ₀\n (`seriesFun_sub_self_term_analyticAt`,\n `seriesFun_sub_polar_analyticAt`) — the inputs 5e-iv needs for the\n residue cancellation at the nontrivial zeros.\n\nArchive references: D-068 §3, journal-015 (ii′-1a dominator chain),\njournal-020/021 (Weierstrass-convergence pattern), journal-024 (the\ncompact-finiteness ball pattern).\n-/\nimport Mathlib\nimport Zeta23.Statement\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/-! ## 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/-! ## 1. The norm comparison and the tail bound -/\n\n/-- For a nontrivial zero with 2 ≤ ‖ρ‖: 1 + ‖γ_ρ‖² ≤ (17/12)·‖ρ‖².\nOn re ρ ∈ (0, 1): ‖γ‖² = im² + (1/2−re)² ≤ im² + 1/4, and\nim² = ‖ρ‖² − re² ≥ 4 − 1 = 3 gives 5/4 ≤ (5/12)·im². -/\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 (ρ : ℂ))\n = (ρ : ℂ).im ^ 2 + (1 / 2 - (ρ : ℂ).re) ^ 2 := by\n rw [Complex.normSq_apply, WeilEF.gammaOf_re, WeilEF.gammaOf_im]\n ring\n have hρsq : 4 ≤ ‖(ρ : ℂ)‖ ^ 2 := by nlinarith [hρ, norm_nonneg (ρ : ℂ)]\n have hre2 : (ρ : ℂ).re ^ 2 ≤ 1 := by nlinarith [hre0, hre1]\n have him2 : 3 ≤ (ρ : ℂ).im ^ 2 := by nlinarith [hρsq, hre2]\n have hquarter : (1 / 2 - (ρ : ℂ).re) ^ 2 ≤ 1 / 4 := by nlinarith [hre0, hre1]\n rw [hgam, hnorm]\n nlinarith [him2, hquarter, sq_nonneg (ρ : ℂ).re]\n\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 have h2 : ρ * (s - ρ) ≠ 0 := mul_ne_zero h0 h1\n field_simp\n ring\n\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; norm_num at hρ2\n have hρpos : (0 : ℝ) < ‖(ρ : ℂ)‖ := norm_pos_iff.mpr h0\n have hsr : ‖(ρ : ℂ)‖ / 2 ≤ ‖s - (ρ : ℂ)‖ := by\n have h := abs_norm_sub_norm_le s (ρ : ℂ)\n rw [abs_le] at h\n linarith [h.1]\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 h := Complex.normSq_nonneg (gammaOf (ρ : ℂ)); linarith\n have halg := one_div_sub_add_one_div h0 h1\n have hden : ‖(ρ : ℂ)‖ ^ 2 / 2 ≤ ‖(ρ : ℂ)‖ * ‖s - (ρ : ℂ)‖ := by\n nlinarith [mul_le_mul_of_nonneg_left hsr hρpos.le]\n have hden0 : (0 : ℝ) < ‖(ρ : ℂ)‖ * ‖s - (ρ : ℂ)‖ :=\n mul_pos hρpos (by linarith [hsr, hρpos])\n have hρsq0 : (0 : ℝ) < ‖(ρ : ℂ)‖ ^ 2 := pow_pos hρpos 2\n have hfrac : ‖s‖ / (‖(ρ : ℂ)‖ * ‖s - (ρ : ℂ)‖) ≤ 2 * ‖s‖ / ‖(ρ : ℂ)‖ ^ 2 := by\n rw [div_le_div_iff₀ hden0 hρsq0]\n nlinarith [hden, norm_nonneg s, hρpos]\n have hmul0 : (0 : ℝ) ≤ (zeroMult ρ : ℝ) := Nat.cast_nonneg _\n simp only [seriesTerm]\n rw [halg, norm_mul, RCLike.norm_natCast, norm_div, norm_mul]\n calc (zeroMult ρ : ℝ) * (‖s‖ / (‖(ρ : ℂ)‖ * ‖s - (ρ : ℂ)‖))\n ≤ (zeroMult ρ : ℝ) * (2 * ‖s‖ / ‖(ρ : ℂ)‖ ^ 2) :=\n 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 have hR : 17 / 6 * ‖s‖ * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ))))\n = (17 / 6 * ‖s‖ * (zeroMult ρ : ℝ)) / (1 + Complex.normSq (gammaOf (ρ : ℂ))) := by\n ring\n rw [hR, div_le_div_iff₀ hρsq0 hg0]\n have hkey : 2 * (1 + Complex.normSq (gammaOf (ρ : ℂ)))\n ≤ 17 / 6 * ‖(ρ : ℂ)‖ ^ 2 := by linarith [hcomp]\n calc 2 * ‖s‖ * (zeroMult ρ : ℝ) * (1 + Complex.normSq (gammaOf (ρ : ℂ)))\n = (‖s‖ * (zeroMult ρ : ℝ)) * (2 * (1 + Complex.normSq (gammaOf (ρ : ℂ)))) := by\n 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\n/-! ## 2. Summability -/\n\n/-- The subtype elements in a closed ball form a finite set (the ii′-1a\ncompact-finiteness pattern: nontrivial zeros ⊆ `riemannZetaZeros`,\nfinite in compacts by Mathlib's discreteness of the zero set). -/\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/-- The M-test majorant family, summable by Zeta23's `zero_sum_inv_sq`. -/\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\n/-- The series is absolutely summable at every s (the ii′-1a D-trick:\ndominator (17/6)(‖s‖+1)·mult/(1+‖γ‖²) on the tail ‖ρ‖ ≥ max 2 (2‖s‖),\nfinite head by `finite_subtype_norm_lt`). -/\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 apply (finite_subtype_norm_lt R₀).subset\n intro ρ hρ\n exact not_le.mp hρ\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 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 refine Summable.of_norm_bounded 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 have hg0 : (0 : ℝ) ≤ (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ))) := by\n have hnn := Complex.normSq_nonneg (gammaOf (ρ : ℂ))\n positivity\n have hC' : 17 / 6 * ‖s‖ ≤ C := by\n rw [hC]\n nlinarith [norm_nonneg s]\n exact mul_le_mul_of_nonneg_right hC' hg0\n · simp only [D, if_neg hρ, le_refl]\n\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 of ζ where ζ s₀ ≠ 0; the order\nnormal form (zeros isolated among ζ-zeros) where ζ s₀ = 0, s₀ ≠ 1; the\nzetaA factorization (pole neighbourhood) 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 have hρ1 : (ρ : ℂ) ≠ 1 := by\n intro h\n have hlt : (ρ : ℂ).re < 1 := ρ.2.2.2\n rw [h, Complex.one_re] at hlt\n exact lt_irrefl 1 hlt\n have hz := hball (ρ : ℂ) hρ\n rw [zetaA_apply hρ1, ρ.2.1, mul_zero] at hz\n exact hz rfl\n · by_cases h0 : riemannZeta s₀ = 0\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 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\n have hne : h (ρ : ℂ) ≠ 0 := hball₁ (ρ : ℂ) hmem1\n by_cases hρs : (ρ : ℂ) = s₀\n · 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]\n exact mul_ne_zero hpow hne\n exact hz ρ.2.1\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/-! ## 4. Analyticity off the zeros -/\n\n/-- The series is analytic at every point that is not a nontrivial zero\n(Weierstrass M-test on an avoiding ball; the journal-020/021 pattern). -/\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 have hM0 : (0 : ℝ) ≤ M := by rw [hM]; linarith [norm_nonneg s₀, hδ.le]\n set R₀ : ℝ := max 2 (2 * M) with hR₀\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 s₀ δ, ‖seriesTerm s ρ‖ ≤ u ρ := by\n rw [eventually_cofinite]\n apply (finite_subtype_norm_lt R₀).subset\n intro ρ hρ\n simp only [Set.mem_setOf_eq, not_forall] at hρ\n by_contra hlt\n rw [not_lt] at hlt\n apply hρ\n intro s hs\n have hsM : ‖s‖ ≤ M := by\n have hlt2 : ‖s‖ < M := by\n calc ‖s‖ ≤ ‖s - s₀‖ + ‖s₀‖ := by\n nth_rewrite 1 [show s = (s - s₀) + s₀ from by ring]\n exact norm_add_le _ _\n _ < δ + ‖s₀‖ := by\n have hmem := Metric.mem_ball.mp hs\n rw [dist_eq_norm] at hmem\n linarith\n _ = M := by rw [hM]; ring\n exact le_of_lt hlt2\n have h2 : (2 : ℝ) ≤ ‖(ρ : ℂ)‖ := (le_max_left _ _).trans hlt\n have hs2 : 2 * ‖s‖ ≤ ‖(ρ : ℂ)‖ := by\n have h2M : 2 * ‖s‖ ≤ 2 * M := by linarith\n exact (h2M.trans (le_max_right _ _)).trans hlt\n have h := seriesTerm_norm_le ρ h2 hs2\n apply h.trans\n have hg0 : (0 : ℝ) ≤ (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ))) := by\n have hnn := Complex.normSq_nonneg (gammaOf (ρ : ℂ))\n positivity\n have hle : 17 / 6 * ‖s‖ ≤ 17 / 6 * M := by nlinarith [hsM, hM0, norm_nonneg s]\n exact mul_le_mul_of_nonneg_right hle hg0\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 ρ)\n (Metric.ball s₀ δ) := by\n apply htend.differentiableOn _ Metric.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ρt\n have hsρ : s - (ρ : ℂ) ≠ 0 := by\n have hρout : (ρ : ℂ) ∉ Metric.ball s₀ δ := hball ρ\n intro h\n apply hρout\n have heq : (ρ : ℂ) = s := (sub_eq_zero.mp h).symm\n rw [heq]\n exact hs\n have hρ0 : (ρ : ℂ) ≠ 0 := by\n intro h\n have hlt := ρ.2.2.1\n rw [h] at hlt\n simp at hlt\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 have han : AnalyticOnNhd ℂ (fun s => ∑' ρ, seriesTerm s ρ) (Metric.ball s₀ δ) :=\n hdiff.analyticOnNhd Metric.isOpen_ball\n exact han s₀ (Metric.mem_ball_self hδ)\n\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/-! ## 5. Isolation and the reduced series -/\n\n/-- Each nontrivial zero is isolated from the others (finiteness of the\nzero set in the unit ball + minimum distance). -/\ntheorem nontrivialZero_isolated (ρ₀ : {ρ : ℂ // IsNontrivialZero ρ}) :\n ∃ δ : ℝ, 0 < δ ∧ ∀ ρ₁ : {ρ : ℂ // IsNontrivialZero ρ}, ρ₁ ≠ ρ₀ →\n δ ≤ ‖(ρ₁ : ℂ) - (ρ₀ : ℂ)‖ := by\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 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 · set d : Finset ℝ := hSfin.toFinset.image (fun ρ => ‖(ρ : ℂ) - (ρ₀ : ℂ)‖) with hd\n have hdne : d.Nonempty := by\n obtain ⟨ρ, hρ⟩ := hne\n refine ⟨‖(ρ : ℂ) - (ρ₀ : ℂ)‖, ?_⟩\n rw [hd]\n exact Finset.mem_image.mpr ⟨ρ, (Set.Finite.mem_toFinset hSfin).mpr hρ, rfl⟩\n have hdpos : ∀ x ∈ d, 0 < x := by\n intro x hx\n rw [hd] at hx\n obtain ⟨ρ, hρ, rfl⟩ := Finset.mem_image.mp hx\n rw [Set.Finite.mem_toFinset] at hρ\n have h1 : (ρ : ℂ) ≠ (ρ₀ : ℂ) := fun h => hρ.2 (Subtype.ext h)\n exact norm_pos_iff.mpr (sub_ne_zero.mpr h1)\n have hmin0 : 0 < d.min' hdne := hdpos _ (Finset.min'_mem _ _)\n have hmin1 : d.min' hdne ≤ 1 := by\n have hm := Finset.min'_mem d hdne\n rw [hd] at hm\n obtain ⟨ρ, hρ, rfl⟩ := Finset.mem_image.mp hm\n rw [Set.Finite.mem_toFinset] at hρ\n rw [Metric.mem_closedBall, dist_eq_norm] at hρ\n exact hρ.1\n refine ⟨d.min' hdne / 2, half_pos hmin0, fun ρ₁ hρ₁ => ?_⟩\n by_cases hmem : (ρ₁ : ℂ) ∈ Metric.closedBall (ρ₀ : ℂ) 1\n · have h1 : ρ₁ ∈ S := ⟨hmem, hρ₁⟩\n have h2 : ‖(ρ₁ : ℂ) - (ρ₀ : ℂ)‖ ∈ d := by\n rw [hd]\n exact Finset.mem_image.mpr ⟨ρ₁, (Set.Finite.mem_toFinset hSfin).mpr h1, rfl⟩\n have h3 : d.min' hdne ≤ ‖(ρ₁ : ℂ) - (ρ₀ : ℂ)‖ := Finset.min'_le _ _ h2\n linarith\n · have h4 : 1 ≤ ‖(ρ₁ : ℂ) - (ρ₀ : ℂ)‖ := by\n by_contra h\n apply hmem\n rw [Metric.mem_closedBall, dist_eq_norm]\n exact le_of_lt (not_le.mp h)\n linarith\n · refine ⟨1 / 2, by norm_num, fun ρ₁ hρ₁ => ?_⟩\n by_contra h\n push_neg at h\n apply hne\n exact ⟨ρ₁, ⟨by\n rw [Metric.mem_closedBall, dist_eq_norm]\n linarith, hρ₁⟩⟩\n\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 ρ₀\n(`seriesFunSub_analyticAt`). -/\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).norm (fun ρ => seriesTermSub_norm_le ρ₀ s ρ)\n\nlemma single_summable (ρ₀ : {ρ : ℂ // IsNontrivialZero ρ}) (s : ℂ) :\n Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n if ρ = ρ₀ then seriesTerm s ρ else (0 : ℂ)) := by\n apply summable_of_hasFiniteSupport ((Set.finite_singleton ρ₀).subset ?_)\n intro ρ hρ\n rw [Function.mem_support, ne_eq] at hρ\n by_contra h\n apply hρ\n rw [if_neg (fun he => h (Set.mem_singleton_iff.mpr he))]\n\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 hsingle : ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},\n (if ρ = ρ₀ then seriesTerm s ρ else (0 : ℂ)) = seriesTerm s ρ₀ := by\n rw [tsum_eq_single ρ₀ (fun ρ hρ => if_neg hρ)]\n exact if_pos rfl\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]\n\n/-- The series minus its ρ₀-term equals the reduced series (everywhere). -/\ntheorem seriesFun_sub_term (ρ₀ : {ρ : ℂ // IsNontrivialZero ρ}) (s : ℂ) :\n seriesFun s - seriesTerm s ρ₀ = seriesFunSub ρ₀ s := by\n have h := seriesFun_eq_sub_add ρ₀ s\n rw [h]\n ring\n\n/-- The reduced series is analytic at ρ₀ (the other terms have no pole\nin the isolation ball; Weierstrass M-test as in §4). -/\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 have hM0 : (0 : ℝ) ≤ M := by rw [hM]; linarith [norm_nonneg (ρ₀ : ℂ), hδ'0.le]\n set R₀ : ℝ := max 2 (2 * M) with hR₀\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 (ρ₀ : ℂ) δ',\n ‖seriesTermSub ρ₀ s ρ‖ ≤ u ρ := by\n rw [eventually_cofinite]\n apply (finite_subtype_norm_lt R₀).subset\n intro ρ hρ\n simp only [Set.mem_setOf_eq, not_forall] at hρ\n by_contra hlt\n rw [not_lt] at hlt\n apply hρ\n intro s hs\n have hsM : ‖s‖ ≤ M := by\n have hlt2 : ‖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 hmem := Metric.mem_ball.mp hs\n rw [dist_eq_norm] at hmem\n linarith\n _ = M := by rw [hM]; ring\n exact le_of_lt hlt2\n by_cases h0 : ρ = ρ₀\n · rw [seriesTermSub, if_pos h0, norm_zero]\n have hg0 : (0 : ℝ) ≤ (zeroMult ρ₀ : ℝ) / (1 + Complex.normSq (gammaOf (ρ₀ : ℂ))) := by\n have hnn := Complex.normSq_nonneg (gammaOf (ρ₀ : ℂ))\n positivity\n exact mul_nonneg (mul_nonneg (by norm_num) hM0) hg0\n · have h2 : (2 : ℝ) ≤ ‖(ρ : ℂ)‖ := (le_max_left _ _).trans hlt\n have hs2 : 2 * ‖s‖ ≤ ‖(ρ : ℂ)‖ := by\n have h2M : 2 * ‖s‖ ≤ 2 * M := by linarith\n exact (h2M.trans (le_max_right _ _)).trans hlt\n rw [seriesTermSub, if_neg h0]\n have h := seriesTerm_norm_le ρ h2 hs2\n apply h.trans\n have hg0 : (0 : ℝ) ≤ (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ))) := by\n have hnn := Complex.normSq_nonneg (gammaOf (ρ : ℂ))\n positivity\n have hle : 17 / 6 * ‖s‖ ≤ 17 / 6 * M := by nlinarith [hsM, hM0, norm_nonneg s]\n exact mul_le_mul_of_nonneg_right hle hg0\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 : TendstoLocallyUniformlyOn\n (fun t : Finset {ρ : ℂ // IsNontrivialZero ρ} => fun s => ∑ ρ ∈ t, seriesTermSub ρ₀ s ρ)\n (fun s => ∑' ρ, seriesTermSub ρ₀ s ρ) atTop (Metric.ball (ρ₀ : ℂ) δ') :=\n TendstoUniformlyOn.tendstoLocallyUniformlyOn\n (hasSumUniformlyOn_iff_tendstoUniformlyOn.mp hu')\n have hdiff : DifferentiableOn ℂ (fun s => ∑' ρ, seriesTermSub ρ₀ s ρ)\n (Metric.ball (ρ₀ : ℂ) δ') := by\n apply htend.differentiableOn _ Metric.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 hmem := Metric.mem_ball.mp hs\n rwa [dist_eq_norm] at hmem\n intro hzero\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 heq : s = (ρ : ℂ) := sub_eq_zero.mp hzero\n rw [← heq, sub_self, norm_zero]\n rw [h2] at h1\n linarith [hle, hlt, hδ, hδ']\n have hρ0 : (ρ : ℂ) ≠ 0 := by\n intro h\n have hlt := ρ.2.2.1\n rw [h] at hlt\n simp at hlt\n show DifferentiableAt ℂ (fun s => if ρ = ρ₀ then (0 : ℂ) else seriesTerm s ρ) s\n rw [if_neg h0]\n show DifferentiableAt ℂ\n (fun s => (zeroMult ρ : ℂ) * (1 / (s - (ρ : ℂ)) + 1 / (ρ : ℂ))) s\n exact (((differentiableAt_const (1 : ℂ)).div\n (differentiableAt_id.sub (differentiableAt_const _)) hsρ).add\n (differentiableAt_const _)).const_mul _\n have han : AnalyticOnNhd ℂ (fun s => ∑' ρ, seriesTermSub ρ₀ s ρ) (Metric.ball (ρ₀ : ℂ) δ') :=\n hdiff.analyticOnNhd Metric.isOpen_ball\n exact han (ρ₀ : ℂ) (Metric.mem_ball_self hδ'0)\n\n/-- The series with its ρ₀-term subtracted is analytic at ρ₀. -/\ntheorem seriesFun_sub_self_term_analyticAt (ρ₀ : {ρ : ℂ // IsNontrivialZero ρ}) :\n AnalyticAt ℂ (fun s => seriesFun s - seriesTerm s ρ₀) (ρ₀ : ℂ) := by\n apply AnalyticAt.congr (seriesFunSub_analyticAt ρ₀)\n exact Filter.Eventually.of_forall (fun s => (seriesFun_sub_term ρ₀ s).symm)\n\n/-- The polar subtraction form consumed by 5e-iv: the series minus\nmult(ρ₀)/(s−ρ₀) is analytic at ρ₀ (the +mult/ρ₀ part is a constant). -/\ntheorem seriesFun_sub_polar_analyticAt (ρ₀ : {ρ : ℂ // IsNontrivialZero ρ}) :\n AnalyticAt ℂ (fun s => seriesFun s - (zeroMult (ρ₀ : ℂ) : ℂ) / (s - (ρ₀ : ℂ)))\n (ρ₀ : ℂ) := 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 simp only [seriesTerm]\n ring\n rw [heq]\n exact h.add analyticAt_const\n\nend\n\nend NguyenRH1\n"},"extra_content":null}]