← Session 28 — ii′-5e: partial-fraction identity (zero series + F entire)
thinking (416 chars)
- `zeroMult_neg_two_mul (n : ℕ) (hn : 1 ≤ n) : zeroMult (-2 * (n : ℂ)) = 1` ✓ — matches my badPoint form `-2 * (n : ℂ)` ✓.
- `summable_digamma_series (hz : z ∈ integerComplement) : Summable (fun n : ℕ => 1/((n:ℂ)+1) − 1/(z+n+1))` ✓ exact form match.
Also useful spotted: `Nat.cast_add_one_ne_zero n : ((n:ℂ)+1) ≠ 0` ✓ banked for my term algebra.
Now write §5–§6. This is a lot of code; let me write it and iterate.
All confirmed. Writing §5–§6 (digamma series parts + the 0 and −2n witnesses).
tool: Edit
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiFEntire.lean",
"old_string": " \u00b7 filter_upwards [logDeriv_zeta_eq_logDeriv_zetaA_sub] with s hs\n show logDeriv riemannZeta s - seriesFun s + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : \u2102) / 2 + Complex.digamma (s / 2) / 2\n = logDeriv zetaA s - seriesFun s + 1 / s - (Real.log Real.pi : \u2102) / 2\n + Complex.digamma (s / 2) / 2\n rw [hs]\n ring\n\nend NguyenRH1\n\nend",
"new_string": " \u00b7 filter_upwards [logDeriv_zeta_eq_logDeriv_zetaA_sub] with s hs\n show logDeriv riemannZeta s - seriesFun s + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : \u2102) / 2 + Complex.digamma (s / 2) / 2\n = logDeriv zetaA s - seriesFun s + 1 / s - (Real.log Real.pi : \u2102) / 2\n + Complex.digamma (s / 2) / 2\n rw [hs]\n ring\n\n/-! ## 5. The digamma series part and the witness at s = 0 -/\n\n/-- The series part of the digamma partial-fraction expansion\n\u03a3'_j (1/(j+1) \u2212 1/(w+j+1)); analytic on ball(0, 1/2). -/\ndef digammaSeriesPart (w : \u2102) : \u2102 :=\n \u2211' j : \u2115, (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))\n\n/-- Pole avoidance on ball(0, 1/2): w + j + 1 \u2260 0. -/\nlemma add_nat_add_one_ne_zero_of_mem_ball {w : \u2102} (hw : w \u2208 Metric.ball 0 (1 / 2)) (j : \u2115) :\n w + (j : \u2102) + 1 \u2260 0 := by\n have hwn : \u2016w\u2016 < 1 / 2 := by\n have h := Metric.mem_ball.mp hw\n rwa [dist_zero_right] at this\n intro h\n have h1 : (w + (j : \u2102) + 1).re = w.re + (j : \u211d) + 1 := by\n simp [Complex.add_re, Complex.natCast_re, Complex.one_re]\n rw [h] at h1\n simp at h1\n have h2 : -\u2016w\u2016 \u2264 w.re := (abs_le.mp (Complex.abs_re_le_norm w)).1\n have hj0 : (0 : \u211d) \u2264 (j : \u211d) := Nat.cast_nonneg j\n linarith\n\n/-- The digamma series part is analytic on ball(0, 1/2) (M-test,\n\u03a3 1/(j+1)\u00b2 majorant). -/\nlemma digammaSeriesPart_analyticOn :\n AnalyticOnNhd \u2102 digammaSeriesPart (Metric.ball 0 (1 / 2)) := by\n have hsum : Summable (fun j : \u2115 => (1 : \u211d) / ((j : \u211d) + 1) ^ 2) :=\n summable_div_add_one_sq 1\n have hu : HasSumUniformlyOn (fun j => fun w : \u2102 => 1 / ((j : \u2102) + 1) - 1 / (w + j + 1))\n digammaSeriesPart (Metric.ball 0 (1 / 2)) := by\n apply HasSumUniformlyOn.of_norm_le_summable hsum\n intro j w hw\n have hwn : \u2016w\u2016 < 1 / 2 := by\n have h := Metric.mem_ball.mp hw\n rwa [dist_zero_right] at this\n have hj1 : (0 : \u211d) < (j : \u211d) + 1 := by positivity\n have hwj : w + (j : \u2102) + 1 \u2260 0 := add_nat_add_one_ne_zero_of_mem_ball hw j\n have hj0 : ((j : \u2102) + 1) \u2260 0 := Nat.cast_add_one_ne_zero j\n have halg : 1 / ((j : \u2102) + 1) - 1 / (w + j + 1)\n = w / (((j : \u2102) + 1) * (w + j + 1)) := by\n field_simp\n ring\n have hnorm1 : \u2016((j : \u2102) + 1)\u2016 = (j : \u211d) + 1 := by\n have e : ((j : \u2102) + 1) = ((j + 1 : \u2115) : \u2102) := by push_cast; ring\n rw [e, RCLike.norm_natCast, Nat.cast_add, Nat.cast_one]\n have hnorm2 : ((j : \u211d) + 1) / 2 \u2264 \u2016w + (j : \u2102) + 1\u2016 := by\n have h2 : (w + (j : \u2102) + 1).re \u2264 \u2016w + (j : \u2102) + 1\u2016 := Complex.re_le_norm _\n have h3 : (w + (j : \u2102) + 1).re = w.re + (j : \u211d) + 1 := by\n simp [Complex.add_re, Complex.natCast_re, Complex.one_re]\n have h4 : -\u2016w\u2016 \u2264 w.re := (abs_le.mp (Complex.abs_re_le_norm w)).1\n linarith\n rw [halg, norm_div, norm_mul, hnorm1]\n have hA2 : (0 : \u211d) < ((j : \u211d) + 1) ^ 2 := by positivity\n have hden0 : (0 : \u211d) < ((j : \u211d) + 1) * \u2016w + (j : \u2102) + 1\u2016 :=\n mul_pos hj1 (by linarith [hnorm2, hj1])\n rw [div_le_div_iff\u2080 hden0 hA2]\n nlinarith [hwn.le, hnorm2, hj1.le, sq_nonneg ((j : \u211d) + 1)]\n have htend : TendstoLocallyUniformlyOn\n (fun t : Finset \u2115 => fun w => \u2211 j \u2208 t, (1 / ((j : \u2102) + 1) - 1 / (w + j + 1)))\n digammaSeriesPart atTop (Metric.ball 0 (1 / 2)) :=\n TendstoUniformlyOn.tendstoLocallyUniformlyOn\n (hasSumUniformlyOn_iff_tendstoUniformlyOn.mp hu)\n have hdiff : DifferentiableOn \u2102 digammaSeriesPart (Metric.ball 0 (1 / 2)) := by\n apply htend.differentiableOn _ Metric.isOpen_ball\n apply Filter.Eventually.of_forall\n intro t w hw\n rw [show (fun w => \u2211 j \u2208 t, (1 / ((j : \u2102) + 1) - 1 / (w + j + 1)))\n = \u2211 j \u2208 t, (fun w => 1 / ((j : \u2102) + 1) - 1 / (w + j + 1)) from by\n funext w; simp [Finset.sum_apply]]\n apply DifferentiableAt.differentiableWithinAt\n apply DifferentiableAt.sum\n intro j _\n have hwj : w + (j : \u2102) + 1 \u2260 0 := add_nat_add_one_ne_zero_of_mem_ball hw j\n have h2 : DifferentiableAt \u2102 (fun w : \u2102 => 1 / (w + (j : \u2102) + 1)) w :=\n (differentiableAt_const (1 : \u2102)).div\n ((differentiableAt_id.add (differentiableAt_const _)).add (differentiableAt_const _))\n hwj\n exact (differentiableAt_const _).sub h2\n exact hdiff.analyticOnNhd Metric.isOpen_ball\n\n/-- The digamma series evaluation near 0 (punctured): for\nw \u2208 ball(0, 1/2), w \u2260 0. -/\nlemma digamma_eq_seriesPart_near_zero {w : \u2102}\n (hw : w \u2208 Metric.ball 0 (1 / 2)) (hw0 : w \u2260 0) :\n Complex.digamma w = -(Real.eulerMascheroniConstant : \u2102) - 1 / w + digammaSeriesPart w := by\n have hZ : w \u2208 Complex.integerComplement := by\n intro k hk\n -- w = (k : \u2124): |k| < 1/2 forces k = 0\n have hmem := Metric.mem_ball.mp hw\n rw [dist_zero_right] at hmem\n rw [hk] at hmem\n have hk0 : (1 : \u211d) \u2264 \u2016(k : \u2102)\u2016 \u2228 k = 0 := by\n by_cases hkz : k = 0\n \u00b7 exact Or.inr hkz\n \u00b7 left\n have h1 : (1 : \u2124) \u2264 |k| := Int.one_le_abs hkz\n have h2 : \u2016(k : \u2102)\u2016 = |(k : \u211d)| := by\n rw [show ((k : \u2102)) = (((k : \u211d)) : \u2102) by push_cast; ring, Complex.norm_ofReal]\n rw [h2]\n have h3 : (1 : \u211d) \u2264 |(k : \u211d)| := by exact_mod_cast h1\n exact h3\n rcases hk0 with habs | hk0\n \u00b7 linarith\n \u00b7 exact hw0 (by rw [hk, hk0]; simp)\n have h := Zeta23.DigammaSeries.digamma_series hZ\n rw [h]\n rfl\n\n/-- The witness at s = 0: Fexpr agrees punctured with\nlogDeriv \u03b6 \u2212 seriesFun + 1/(s\u22121) \u2212 (log \u03c0)/2 + (\u2212\u03b3 + digammaSeriesPart(s/2))/2,\nanalytic at 0. -/\nlemma Fexpr_eventually_zero :\n \u2203 W : \u2102 \u2192 \u2102, AnalyticAt \u2102 W 0 \u2227 \u2200\u1da0 s in \ud835\udcdd[\u2260] (0 : \u2102), Fexpr s = W s := by\n have hA : AnalyticAt \u2102 (logDeriv riemannZeta) 0 := by\n have hz : riemannZeta 0 \u2260 0 := by rw [riemannZeta_zero]; norm_num\n exact ((analyticAt_riemannZeta (by norm_num)).deriv).div\n (analyticAt_riemannZeta (by norm_num)) hz\n have hB : AnalyticAt \u2102 seriesFun 0 := seriesFun_analyticAt (by\n intro h\n have hpos := h.2.1\n rw [Complex.zero_re] at hpos\n exact lt_irrefl 0 hpos)\n have hC : AnalyticAt \u2102 (fun s : \u2102 => 1 / (s - 1)) 0 := by\n apply AnalyticAt.div analyticAt_const _ (by norm_num : (0 : \u2102) - 1 \u2260 0)\n exact analyticAt_id.sub analyticAt_const\n have hD : AnalyticAt \u2102 (fun _ : \u2102 => (Real.log Real.pi : \u2102) / 2) 0 := analyticAt_const\n have hE : AnalyticAt \u2102\n (fun s => (-(Real.eulerMascheroniConstant : \u2102) + digammaSeriesPart (s / 2)) / 2) 0 := by\n apply AnalyticAt.div _ analyticAt_const (by norm_num : (2 : \u2102) \u2260 0)\n apply AnalyticAt.add analyticAt_const\n have h1 : AnalyticAt \u2102 (fun s : \u2102 => s / 2) 0 := by\n apply AnalyticAt.div analyticAt_id analyticAt_const (by norm_num)\n exact AnalyticAt.comp (f := fun s : \u2102 => s / 2)\n (digammaSeriesPart_analyticOn 0 (Metric.mem_ball_self (by norm_num))) h1\n refine \u27e8fun s => logDeriv riemannZeta s - seriesFun s + 1 / (s - 1)\n - (Real.log Real.pi : \u2102) / 2\n + (-(Real.eulerMascheroniConstant : \u2102) + digammaSeriesPart (s / 2)) / 2, ?_, ?_\u27e9\n \u00b7 exact ((((hA.sub hB).add hC).sub hD).add hE)\n \u00b7 -- punctured agreement on ball(0, 1/2)\n rw [Metric.eventually_nhdsWithin_iff]\n refine \u27e81 / 2, by norm_num, fun s hs => ?_\u27e9\n have hs0 : s \u2260 0 := hs.2\n have hsball : s \u2208 Metric.ball 0 (1 / 2) := hs.1\n have hs2ball : s / 2 \u2208 Metric.ball 0 (1 / 2) := by\n rw [Metric.mem_ball, dist_zero_right] at hsball \u22a2\n rw [norm_div, RCLike.norm_ofNat]\n linarith\n have hs20 : s / 2 \u2260 0 := by\n intro h\n exact hs0 (by linear_combination 2 * h)\n have hdig := digamma_eq_seriesPart_near_zero hs2ball hs20\n show logDeriv riemannZeta s - seriesFun s + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : \u2102) / 2 + Complex.digamma (s / 2) / 2\n = logDeriv riemannZeta s - seriesFun s + 1 / (s - 1)\n - (Real.log Real.pi : \u2102) / 2\n + (-(Real.eulerMascheroniConstant : \u2102) + digammaSeriesPart (s / 2)) / 2\n rw [hdig]\n ring\n\n/-! ## 6. The digamma series minus a pole term, and the witness at s = \u22122n -/\n\n/-- \u03b6(\u22122n) = 0 for n \u2265 1 (from `zeroMult_neg_two_mul`: the order is 1). -/\nlemma riemannZeta_neg_two_mul {n : \u2115} (hn : 1 \u2264 n) :\n riemannZeta (-2 * (n : \u2102)) = 0 := by\n by_contra h\n have hord := zeroMult_neg_two_mul n hn\n have hne1 : (-2 * (n : \u2102)) \u2260 1 := by\n intro hh\n have hre := congrArg Complex.re hh\n simp at hre\n have hn1 : (1 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n linarith\n have h0 : analyticOrderAt riemannZeta (-2 * (n : \u2102)) = 0 :=\n (analyticAt_riemannZeta hne1).analyticOrderAt_eq_zero.mpr h\n have hmz : zeroMult (-2 * (n : \u2102)) = analyticOrderNatAt riemannZeta (-2 * (n : \u2102)) := rfl\n rw [hmz] at hord\n rw [h0] at hord\n simp at hord\n\n/-- Pole avoidance on ball(\u2212n, 1/2) for j \u2260 n\u22121: w + j + 1 \u2260 0. -/\nlemma add_nat_add_one_ne_zero_of_mem_ball_neg {n : \u2115} (hn : 1 \u2264 n) {w : \u2102}\n (hw : w \u2208 Metric.ball (-(n : \u2102)) (1 / 2)) {j : \u2115} (hj : j \u2260 n - 1) :\n w + (j : \u2102) + 1 \u2260 0 := by\n intro h\n have h1 : w = -((j : \u2102) + 1) := by linear_combination h\n have h2 : dist w (-(n : \u2102)) < 1 / 2 := Metric.mem_ball.mp hw\n rw [h1, Complex.dist_eq] at h2\n have h3 : -((j : \u2102) + 1) - -(n : \u2102) = ((n : \u2102) - ((j : \u2102) + 1)) := by ring\n rw [h3] at h2\n have h4 : \u2016((n : \u2102) - ((j : \u2102) + 1))\u2016 = |(n : \u211d) - ((j : \u211d) + 1)| := by\n rw [show (n : \u2102) - ((j : \u2102) + 1) = (((n : \u211d) - ((j : \u211d) + 1)) : \u2102) by push_cast; ring,\n Complex.norm_ofReal]\n rw [h4] at h2\n have hne : n \u2260 j + 1 := by\n intro hc\n apply hj\n omega\n have h5 : (1 : \u211d) \u2264 |(n : \u211d) - ((j : \u211d) + 1)| := by\n rcases lt_or_gt_of_ne hne with hlt | hgt\n \u00b7 have h6 : (n : \u211d) + 1 \u2264 (j : \u211d) + 1 := by\n exact_mod_cast Nat.succ_le_of_lt hlt\n rw [abs_of_neg (by linarith : (n : \u211d) - ((j : \u211d) + 1) < 0)]\n linarith\n \u00b7 have h6 : (j : \u211d) + 1 + 1 \u2264 (n : \u211d) := by\n exact_mod_cast Nat.succ_le_of_lt hgt\n rw [abs_of_pos (by linarith : 0 < (n : \u211d) - ((j : \u211d) + 1))]\n linarith\n linarith\n\n/-- The digamma series with the j = n\u22121 term dropped; analytic on\nball(\u2212n, 1/2). -/\ndef digammaSeriesPartSub (n : \u2115) (w : \u2102) : \u2102 :=\n \u2211' j : \u2115, (if j = n - 1 then 0 else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1)))\n\n/-- The dropped-term series is analytic on ball(\u2212n, 1/2) (the eventually\nM-test with majorant (2n+1)/(j+1)\u00b2 for j \u2265 2n+1). -/\nlemma digammaSeriesPartSub_analyticOn {n : \u2115} (hn : 1 \u2264 n) :\n AnalyticOnNhd \u2102 (digammaSeriesPartSub n) (Metric.ball (-(n : \u2102)) (1 / 2)) := by\n have hsum : Summable (fun j : \u2115 => (2 * (n : \u211d) + 1) / ((j : \u211d) + 1) ^ 2) :=\n summable_div_add_one_sq _\n have hu : HasSumUniformlyOn\n (fun j => fun w : \u2102 => (if j = n - 1 then 0 else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))))\n (digammaSeriesPartSub n) (Metric.ball (-(n : \u2102)) (1 / 2)) := by\n apply HasSumUniformlyOn.of_norm_le_summable_eventually hsum\n rw [eventually_cofinite]\n apply (Set.finite_Iio (2 * n + 1)).subset\n intro j hj\n show j < 2 * n + 1\n by_contra hj2\n push Not at hj2\n apply hj\n intro w hw\n have hwn : \u2016w\u2016 < (n : \u211d) + 1 / 2 := by\n have h := Metric.mem_ball.mp hw\n rw [Complex.dist_eq] at h\n have htri : \u2016w\u2016 \u2264 \u2016w - -(n : \u2102)\u2016 + \u2016-(n : \u2102)\u2016 := by\n calc \u2016w\u2016 = \u2016(w - -(n : \u2102)) + -(n : \u2102)\u2016 := by congr 1; ring\n _ \u2264 _ := norm_add_le _ _\n have hnnorm : \u2016(-(n : \u2102))\u2016 = (n : \u211d) := by\n rw [norm_neg, RCLike.norm_natCast]\n linarith\n have hjne : j \u2260 n - 1 := by omega\n rw [if_neg hjne]\n have hwj : w + (j : \u2102) + 1 \u2260 0 :=\n add_nat_add_one_ne_zero_of_mem_ball_neg hn hw hjne\n have hj0 : ((j : \u2102) + 1) \u2260 0 := Nat.cast_add_one_ne_zero j\n have halg : 1 / ((j : \u2102) + 1) - 1 / (w + j + 1)\n = w / (((j : \u2102) + 1) * (w + j + 1)) := by\n field_simp\n ring\n have hnorm1 : \u2016((j : \u2102) + 1)\u2016 = (j : \u211d) + 1 := by\n have e : ((j : \u2102) + 1) = ((j + 1 : \u2115) : \u2102) := by push_cast; ring\n rw [e, RCLike.norm_natCast, Nat.cast_add, Nat.cast_one]\n have hj1 : (0 : \u211d) < (j : \u211d) + 1 := by positivity\n -- for j \u2265 2n+1: \u2016w + j + 1\u2016 \u2265 (j+1)/2\n have hnorm2 : ((j : \u211d) + 1) / 2 \u2264 \u2016w + (j : \u2102) + 1\u2016 := by\n have h2 : (w + (j : \u2102) + 1).re \u2264 \u2016w + (j : \u2102) + 1\u2016 := Complex.re_le_norm _\n have h3 : (w + (j : \u2102) + 1).re = w.re + (j : \u211d) + 1 := by\n simp [Complex.add_re, Complex.natCast_re, Complex.one_re]\n have h4 : -\u2016w\u2016 \u2264 w.re := (abs_le.mp (Complex.abs_re_le_norm w)).1\n have hj2' : 2 * ((n : \u211d) + 1) \u2264 (j : \u211d) + 1 := by\n have h5 : 2 * n + 2 \u2264 j + 1 := by omega\n have h6 : (2 * n + 2 : \u2115) \u2264 j + 1 := h5\n have h7 : ((2 * n + 2 : \u2115) : \u211d) \u2264 ((j + 1 : \u2115) : \u211d) := by exact_mod_cast h6\n push_cast at h7\n linarith\n nlinarith [hwn]\n rw [halg, norm_div, norm_mul, hnorm1]\n have hA2 : (0 : \u211d) < ((j : \u211d) + 1) ^ 2 := by positivity\n have hden0 : (0 : \u211d) < ((j : \u211d) + 1) * \u2016w + (j : \u2102) + 1\u2016 :=\n mul_pos hj1 (by linarith [hnorm2, hj1])\n rw [div_le_div_iff\u2080 hden0 hA2]\n have hn0 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n nlinarith [hwn.le, hnorm2, hj1.le, sq_nonneg ((j : \u211d) + 1), hn0]\n have htend : TendstoLocallyUniformlyOn\n (fun t : Finset \u2115 => fun w =>\n \u2211 j \u2208 t, (if j = n - 1 then 0 else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))))\n (digammaSeriesPartSub n) atTop (Metric.ball (-(n : \u2102)) (1 / 2)) :=\n TendstoUniformlyOn.tendstoLocallyUniformlyOn\n (hasSumUniformlyOn_iff_tendstoUniformlyOn.mp hu)\n have hdiff : DifferentiableOn \u2102 (digammaSeriesPartSub n)\n (Metric.ball (-(n : \u2102)) (1 / 2)) := by\n apply htend.differentiableOn _ Metric.isOpen_ball\n apply Filter.Eventually.of_forall\n intro t w hw\n rw [show (fun w => \u2211 j \u2208 t, (if j = n - 1 then 0\n else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))))\n = \u2211 j \u2208 t, (fun w => if j = n - 1 then 0\n else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))) from by\n funext w; simp [Finset.sum_apply]]\n apply DifferentiableAt.differentiableWithinAt\n apply DifferentiableAt.sum\n intro j _\n by_cases hj : j = n - 1\n \u00b7 show DifferentiableAt \u2102 (fun w => if j = n - 1 then (0 : \u2102)\n else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))) w\n simp only [if_pos hj]\n exact differentiableAt_const 0\n \u00b7 have hwj : w + (j : \u2102) + 1 \u2260 0 :=\n add_nat_add_one_ne_zero_of_mem_ball_neg hn hw hj\n show DifferentiableAt \u2102 (fun w => if j = n - 1 then (0 : \u2102)\n else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))) w\n simp only [if_neg hj]\n have h2 : DifferentiableAt \u2102 (fun w : \u2102 => 1 / (w + (j : \u2102) + 1)) w :=\n (differentiableAt_const (1 : \u2102)).div\n ((differentiableAt_id.add (differentiableAt_const _)).add (differentiableAt_const _))\n hwj\n exact (differentiableAt_const _).sub h2\n exact hdiff.analyticOnNhd Metric.isOpen_ball\n\n/-- The single-term split: for w \u2208 ball(\u2212n, 1/2), w \u2260 \u2212n,\ndigammaSeriesPart w = digammaSeriesPartSub n w + (1/n \u2212 1/(w+n)). -/\nlemma digammaSeriesPart_eq_sub_add_single {n : \u2115} (hn : 1 \u2264 n) {w : \u2102}\n (hw : w \u2208 Metric.ball (-(n : \u2102)) (1 / 2)) (hwn : w \u2260 -(n : \u2102)) :\n digammaSeriesPart w\n = digammaSeriesPartSub n w + (1 / (n : \u2102) - 1 / (w + (n : \u2102))) := by\n have hZ : w \u2208 Complex.integerComplement := by\n intro k hk\n -- w = (k:\u2124) with dist w (\u2212n) < 1/2 forces k = \u2212n\n have h2 : dist w (-(n : \u2102)) < 1 / 2 := Metric.mem_ball.mp hw\n rw [hk, Complex.dist_eq] at h2\n have h3 : (k : \u2102) - -(n : \u2102) = ((k + (n : \u2124)) : \u2102) := by push_cast; ring\n rw [h3, show (((k + (n : \u2124)) : \u2102)) = (((k + (n : \u2124) : \u2124) : \u211d) : \u2102) by push_cast; ring,\n Complex.norm_ofReal] at h2\n have h4 : |(k : \u211d) + (n : \u211d)| < 1 / 2 := by\n have : |(k + (n : \u2124) : \u211d)| < 1 / 2 := by\n have h5 : (((k + (n : \u2124) : \u2124) : \u211d) : \u2102) = ((k + (n : \u2124) : \u2124) : \u211d) := rfl\n -- h2 : \u2016\u2191(\u2191(k + \u2191n))\u2016 < 1/2 after the rws; normalize\n convert h2 using 2\n push_cast\n ring\n rwa [show ((k + (n : \u2124)) : \u211d) = (k : \u211d) + (n : \u211d) by push_cast; ring] at this\n have hk0 : k = -(n : \u2124) := by\n by_contra hkne\n have h1 : (1 : \u2124) \u2264 |k + (n : \u2124)| := Int.one_le_abs (by\n intro hh\n exact hkne (neg_eq_of_add_eq_zero_left (by linear_combination hh)))\n have h1r : (1 : \u211d) \u2264 |(k : \u211d) + (n : \u211d)| := by\n have e : |(k : \u211d) + (n : \u211d)| = (|k + (n : \u2124)| : \u211d) := by\n rw [show (k : \u211d) + (n : \u211d) = ((k + (n : \u2124) : \u2124) : \u211d) by push_cast; ring,\n RCLike.norm_natCast]\n rw [e]\n exact_mod_cast h1\n linarith\n exact hwn (by rw [hk, hk0]; push_cast; ring)\n have hfull : Summable (fun j : \u2115 => 1 / ((j : \u2102) + 1) - 1 / (w + j + 1)) :=\n Zeta23.DigammaSeries.summable_digamma_series hZ\n have hsub : Summable (fun j : \u2115 => if j = n - 1 then (0 : \u2102)\n else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))) := by\n apply Summable.of_norm_bounded hfull.norm\n intro j\n by_cases hjj : j = n - 1 <;> simp [hjj]\n have hsingle : Summable (fun j : \u2115 => if j = n - 1\n then (1 / ((j : \u2102) + 1) - 1 / (w + j + 1)) else (0 : \u2102)) := by\n apply summable_of_hasFiniteSupport ((Set.finite_singleton (n - 1)).subset ?_)\n intro j hj\n rw [Function.mem_support, ne_eq] at hj\n by_contra h\n apply hj\n rw [if_neg (fun he => h (Set.mem_singleton_iff.mpr he))]\n have htsum : \u2211' j, (if j = n - 1 then (1 / ((j : \u2102) + 1) - 1 / (w + j + 1)) else (0 : \u2102))\n = 1 / (n : \u2102) - 1 / (w + (n : \u2102)) := by\n rw [tsum_eq_single (n - 1) (fun j hj => if_neg hj)]\n rw [if_pos rfl]\n congr 1\n \u00b7 rw [Nat.cast_sub hn, Nat.cast_one]\n ring\n \u00b7 congr 1\n rw [Nat.cast_sub hn, Nat.cast_one]\n ring\n calc digammaSeriesPart w\n = \u2211' j, (1 / ((j : \u2102) + 1) - 1 / (w + j + 1)) := rfl\n _ = \u2211' j, ((if j = n - 1 then (0 : \u2102) else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1)))\n + (if j = n - 1 then (1 / ((j : \u2102) + 1) - 1 / (w + j + 1)) else (0 : \u2102))) := by\n apply tsum_congr\n intro j\n by_cases hjj : j = n - 1 <;> simp [hjj]\n _ = digammaSeriesPartSub n w\n + \u2211' j, (if j = n - 1 then (1 / ((j : \u2102) + 1) - 1 / (w + j + 1)) else (0 : \u2102)) :=\n Summable.tsum_add hsub hsingle\n _ = digammaSeriesPartSub n w + (1 / (n : \u2102) - 1 / (w + (n : \u2102))) := by rw [htsum]\n\n/-- H_n: digamma plus its pole term at \u2212n, minus the pole \u2014 analytic on\nball(\u2212n, 1/2). -/\ndef Hsub (n : \u2115) (w : \u2102) : \u2102 :=\n -(Real.eulerMascheroniConstant : \u2102) - 1 / w + digammaSeriesPartSub n w + 1 / (n : \u2102)\n\n/-- The punctured digamma split at \u2212n: digamma w = \u22121/(w+n) + H_n w. -/\nlemma digamma_eq_neg_inv_add_Hsub {n : \u2115} (hn : 1 \u2264 n) {w : \u2102}\n (hw : w \u2208 Metric.ball (-(n : \u2102)) (1 / 2)) (hwn : w \u2260 -(n : \u2102)) :\n Complex.digamma w = -1 / (w + (n : \u2102)) + Hsub n w := by\n have hZ : w \u2208 Complex.integerComplement := by\n intro k hk\n have h2 : dist w (-(n : \u2102)) < 1 / 2 := Metric.mem_ball.mp hw\n rw [hk, Complex.dist_eq] at h2\n have h3 : (k : \u2102) - -(n : \u2102) = ((k + (n : \u2124)) : \u2102) := by push_cast; ring\n rw [h3, show (((k + (n : \u2124)) : \u2102)) = (((k + (n : \u2124) : \u2124) : \u211d) : \u2102) by push_cast; ring,\n Complex.norm_ofReal] at h2\n have h4 : |(k : \u211d) + (n : \u211d)| < 1 / 2 := by\n have h5 : |(k + (n : \u2124) : \u211d)| < 1 / 2 := by\n convert h2 using 2\n push_cast\n ring\n rwa [show ((k + (n : \u2124)) : \u211d) = (k : \u211d) + (n : \u211d) by push_cast; ring] at h5\n have hk0 : k = -(n : \u2124) := by\n by_contra hkne\n have h1 : (1 : \u2124) \u2264 |k + (n : \u2124)| := Int.one_le_abs (by\n intro hh\n exact hkne (neg_eq_of_add_eq_zero_left (by linear_combination hh)))\n have h1r : (1 : \u211d) \u2264 |(k : \u211d) + (n : \u211d)| := by\n have e : |(k : \u211d) + (n : \u211d)| = (|k + (n : \u2124)| : \u211d) := by\n rw [show (k : \u211d) + (n : \u211d) = ((k + (n : \u2124) : \u2124) : \u211d) by push_cast; ring,\n RCLike.norm_natCast]\n rw [e]\n exact_mod_cast h1\n linarith\n exact hwn (by rw [hk, hk0]; push_cast; ring)\n have hdig := Zeta23.DigammaSeries.digamma_series hZ\n have hsplit := digammaSeriesPart_eq_sub_add_single hn hw hwn\n rw [hdig, Hsub, hsplit]\n ring\n\n/-- H_n is analytic at \u2212n. -/\nlemma Hsub_analyticAt {n : \u2115} (hn : 1 \u2264 n) :\n AnalyticAt \u2102 (Hsub n) (-(n : \u2102)) := by\n have hA : AnalyticAt \u2102 (fun _ : \u2102 => -(Real.eulerMascheroniConstant : \u2102)) _ := analyticAt_const\n have hB : AnalyticAt \u2102 (fun w : \u2102 => 1 / w) (-(n : \u2102)) := by\n apply AnalyticAt.div analyticAt_const analyticAt_id\n simp\n positivity\n have hC : AnalyticAt \u2102 (digammaSeriesPartSub n) (-(n : \u2102)) :=\n digammaSeriesPartSub_analyticOn hn (-(n : \u2102)) (Metric.mem_ball_self (by norm_num))\n have hD : AnalyticAt \u2102 (fun _ : \u2102 => 1 / (n : \u2102)) _ := analyticAt_const\n show AnalyticAt \u2102 (fun w => -(Real.eulerMascheroniConstant : \u2102) - 1 / w\n + digammaSeriesPartSub n w + 1 / (n : \u2102)) (-(n : \u2102))\n exact (((hA.sub hB).add hC).add hD)\n\n/-- The witness at s = \u22122n (n \u2265 1): Fexpr agrees punctured with\nWtriv \u2212 seriesFun + 1/s + 1/(s\u22121) \u2212 (log \u03c0)/2 + H_n(s/2)/2. -/\nlemma Fexpr_eventually_neg_two_mul {n : \u2115} (hn : 1 \u2264 n) :\n \u2203 W : \u2102 \u2192 \u2102, AnalyticAt \u2102 W (-2 * (n : \u2102)) \u2227\n \u2200\u1da0 s in \ud835\udcdd[\u2260] (-2 * (n : \u2102)), Fexpr s = W s := by\n have h\u03b6 := riemannZeta_neg_two_mul hn\n have hne1 : (-2 * (n : \u2102)) \u2260 1 := by\n intro hh\n have hre := congrArg Complex.re hh\n simp at hre\n have hn1 : (1 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n linarith\n obtain \u27e8Wtriv, hWtriv, hWtrivEq\u27e9 := logDeriv_zeta_sub_mult_div_eventually h\u03b6 hne1\n have hmult : zeroMult (-2 * (n : \u2102)) = 1 := zeroMult_neg_two_mul n hn\n -- the pieces\n have hB : AnalyticAt \u2102 seriesFun (-2 * (n : \u2102)) := seriesFun_analyticAt (by\n intro h\n have hpos := h.2.1\n have hre : (-2 * (n : \u2102)).re = -2 * (n : \u211d) := by simp\n rw [hre] at hpos\n have hn1 : (1 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n linarith)\n have hC : AnalyticAt \u2102 (fun s : \u2102 => 1 / s) (-2 * (n : \u2102)) := by\n apply AnalyticAt.div analyticAt_const analyticAt_id\n simp\n positivity\n have hC1 : AnalyticAt \u2102 (fun s : \u2102 => 1 / (s - 1)) (-2 * (n : \u2102)) := by\n apply AnalyticAt.div analyticAt_const _ (by\n have hn1 : (1 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n intro hh\n have hre := congrArg Complex.re hh\n simp at hre\n linarith)\n exact analyticAt_id.sub analyticAt_const\n have hD : AnalyticAt \u2102 (fun _ : \u2102 => (Real.log Real.pi : \u2102) / 2) _ := analyticAt_const\n have hE : AnalyticAt \u2102 (fun s => Hsub n (s / 2) / 2) (-2 * (n : \u2102)) := by\n apply AnalyticAt.div _ analyticAt_const (by norm_num : (2 : \u2102) \u2260 0)\n have h1 : AnalyticAt \u2102 (fun s : \u2102 => s / 2) (-2 * (n : \u2102)) := by\n apply AnalyticAt.div analyticAt_id analyticAt_const (by norm_num)\n have hval : (-2 * (n : \u2102)) / 2 = -(n : \u2102) := by ring\n rw [\u2190 hval]\n exact AnalyticAt.comp (f := fun s : \u2102 => s / 2) (Hsub_analyticAt hn) h1\n refine \u27e8fun s => Wtriv s - seriesFun s + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : \u2102) / 2 + Hsub n (s / 2) / 2, ?_, ?_\u27e9\n \u00b7 exact ((((hWtriv.sub hB).add hC).add hC1).sub hD).add hE\n \u00b7 -- punctured agreement on ball(\u22122n, 1) (then s/2 \u2208 ball(\u2212n, 1/2))\n rw [Metric.eventually_nhdsWithin_iff]\n refine \u27e81, by norm_num, fun s hs => ?_\u27e9\n have hs0 : s \u2260 -2 * (n : \u2102) := hs.2\n have hsball : s \u2208 Metric.ball (-2 * (n : \u2102)) 1 := hs.1\n have hs2ball : s / 2 \u2208 Metric.ball (-(n : \u2102)) (1 / 2) := by\n rw [Metric.mem_ball, Complex.dist_eq] at hsball \u22a2\n have e : s / 2 - -(n : \u2102) = (s - -2 * (n : \u2102)) / 2 := by ring\n rw [e, norm_div, RCLike.norm_ofNat]\n linarith\n have hs20 : s / 2 \u2260 -(n : \u2102) := by\n intro h\n exact hs0 (by linear_combination 2 * h)\n have hdig := digamma_eq_neg_inv_add_Hsub hn hs2ball hs20\n -- logDeriv split: logDeriv \u03b6 s = Wtriv s + 1/(s + 2n)\n have hlog : logDeriv riemannZeta s = Wtriv s + 1 / (s + 2 * (n : \u2102)) := by\n have h := hWtrivEq\n rw [Metric.eventually_nhdsWithin_iff] at h\n obtain \u27e8\u03b5, h\u03b5, hball\u27e9 := h\n have hmem : s \u2208 Metric.ball (-2 * (n : \u2102)) \u03b5 \u2227 s \u2260 -2 * (n : \u2102) := by\n have h1 : dist s (-2 * (n : \u2102)) < 1 := Metric.mem_ball.mp hs.1\n have h2 : dist s (-2 * (n : \u2102)) < \u03b5 \u2228 \u03b5 \u2264 dist s (-2 * (n : \u2102)) := lt_or_ge _ _\n rcases h2 with h2 | h2\n \u00b7 exact \u27e8Metric.mem_ball.mpr h2, hs0\u27e9\n \u00b7 -- if \u03b5 \u2264 dist, shrink: use min form \u2014 but we need the point bound;\n -- the punctured ball from hball covers dist < \u03b5 only; handle by\n -- noting dist < 1 and re-deriving with min \u03b5 1 below\n exfalso\n -- \u03b5 \u2264 dist s (\u22122n) < 1; the punctured agreement at s is not\n -- available \u2014 instead use the eventually form directly\n exact absurd h2 (not_le.mpr h1)\n have h3 := hball s hmem.1 hmem.2\n rw [hmult] at h3\n have e : s - -2 * (n : \u2102) = s + 2 * (n : \u2102) := by ring\n rw [e] at h3\n -- h3 : logDeriv \u03b6 s \u2212 (1:\u2102)/(s + 2n) = Wtriv s\n rw [show (1 : \u2102) = ((1 : \u2115) : \u2102) from by simp] at h3\n rw [\u2190 Nat.cast_one] at h3\n have h3' : logDeriv riemannZeta s - (1 : \u2102) / (s + 2 * (n : \u2102)) = Wtriv s := by\n convert h3 using 2\n simp\n linear_combination h3'\n show logDeriv riemannZeta s - seriesFun s + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : \u2102) / 2 + Complex.digamma (s / 2) / 2\n = Wtriv s - seriesFun s + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : \u2102) / 2 + Hsub n (s / 2) / 2\n rw [hlog, hdig]\n have h1 : -1 / (s / 2 + (n : \u2102)) / 2 = -1 / (s + 2 * (n : \u2102)) := by\n have e : s / 2 + (n : \u2102) = (s + 2 * (n : \u2102)) / 2 := by ring\n rw [e]\n field_simp\n ring\n linear_combination h1\n\nend NguyenRH1\n\nend"
}
raw content_json (database row)
[{"type":"thinking","thinking":"- `zeroMult_neg_two_mul (n : ℕ) (hn : 1 ≤ n) : zeroMult (-2 * (n : ℂ)) = 1` ✓ — matches my badPoint form `-2 * (n : ℂ)` ✓.\n- `summable_digamma_series (hz : z ∈ integerComplement) : Summable (fun n : ℕ => 1/((n:ℂ)+1) − 1/(z+n+1))` ✓ exact form match.\n\nAlso useful spotted: `Nat.cast_add_one_ne_zero n : ((n:ℂ)+1) ≠ 0` ✓ banked for my term algebra.\n\nNow write §5–§6. This is a lot of code; let me write it and iterate.","signature":""},{"type":"text","text":"All confirmed. Writing §5–§6 (digamma series parts + the 0 and −2n witnesses)."},{"type":"tool_use","id":"Edit_133","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiFEntire.lean","old_string":" · filter_upwards [logDeriv_zeta_eq_logDeriv_zetaA_sub] with s hs\n show logDeriv riemannZeta s - seriesFun s + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : ℂ) / 2 + Complex.digamma (s / 2) / 2\n = logDeriv zetaA s - seriesFun s + 1 / s - (Real.log Real.pi : ℂ) / 2\n + Complex.digamma (s / 2) / 2\n rw [hs]\n ring\n\nend NguyenRH1\n\nend","new_string":" · filter_upwards [logDeriv_zeta_eq_logDeriv_zetaA_sub] with s hs\n show logDeriv riemannZeta s - seriesFun s + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : ℂ) / 2 + Complex.digamma (s / 2) / 2\n = logDeriv zetaA s - seriesFun s + 1 / s - (Real.log Real.pi : ℂ) / 2\n + Complex.digamma (s / 2) / 2\n rw [hs]\n ring\n\n/-! ## 5. The digamma series part and the witness at s = 0 -/\n\n/-- The series part of the digamma partial-fraction expansion\nΣ'_j (1/(j+1) − 1/(w+j+1)); analytic on ball(0, 1/2). -/\ndef digammaSeriesPart (w : ℂ) : ℂ :=\n ∑' j : ℕ, (1 / ((j : ℂ) + 1) - 1 / (w + j + 1))\n\n/-- Pole avoidance on ball(0, 1/2): w + j + 1 ≠ 0. -/\nlemma add_nat_add_one_ne_zero_of_mem_ball {w : ℂ} (hw : w ∈ Metric.ball 0 (1 / 2)) (j : ℕ) :\n w + (j : ℂ) + 1 ≠ 0 := by\n have hwn : ‖w‖ < 1 / 2 := by\n have h := Metric.mem_ball.mp hw\n rwa [dist_zero_right] at this\n intro h\n have h1 : (w + (j : ℂ) + 1).re = w.re + (j : ℝ) + 1 := by\n simp [Complex.add_re, Complex.natCast_re, Complex.one_re]\n rw [h] at h1\n simp at h1\n have h2 : -‖w‖ ≤ w.re := (abs_le.mp (Complex.abs_re_le_norm w)).1\n have hj0 : (0 : ℝ) ≤ (j : ℝ) := Nat.cast_nonneg j\n linarith\n\n/-- The digamma series part is analytic on ball(0, 1/2) (M-test,\nΣ 1/(j+1)² majorant). -/\nlemma digammaSeriesPart_analyticOn :\n AnalyticOnNhd ℂ digammaSeriesPart (Metric.ball 0 (1 / 2)) := by\n have hsum : Summable (fun j : ℕ => (1 : ℝ) / ((j : ℝ) + 1) ^ 2) :=\n summable_div_add_one_sq 1\n have hu : HasSumUniformlyOn (fun j => fun w : ℂ => 1 / ((j : ℂ) + 1) - 1 / (w + j + 1))\n digammaSeriesPart (Metric.ball 0 (1 / 2)) := by\n apply HasSumUniformlyOn.of_norm_le_summable hsum\n intro j w hw\n have hwn : ‖w‖ < 1 / 2 := by\n have h := Metric.mem_ball.mp hw\n rwa [dist_zero_right] at this\n have hj1 : (0 : ℝ) < (j : ℝ) + 1 := by positivity\n have hwj : w + (j : ℂ) + 1 ≠ 0 := add_nat_add_one_ne_zero_of_mem_ball hw j\n have hj0 : ((j : ℂ) + 1) ≠ 0 := Nat.cast_add_one_ne_zero j\n have halg : 1 / ((j : ℂ) + 1) - 1 / (w + j + 1)\n = w / (((j : ℂ) + 1) * (w + j + 1)) := by\n field_simp\n ring\n have hnorm1 : ‖((j : ℂ) + 1)‖ = (j : ℝ) + 1 := by\n have e : ((j : ℂ) + 1) = ((j + 1 : ℕ) : ℂ) := by push_cast; ring\n rw [e, RCLike.norm_natCast, Nat.cast_add, Nat.cast_one]\n have hnorm2 : ((j : ℝ) + 1) / 2 ≤ ‖w + (j : ℂ) + 1‖ := by\n have h2 : (w + (j : ℂ) + 1).re ≤ ‖w + (j : ℂ) + 1‖ := Complex.re_le_norm _\n have h3 : (w + (j : ℂ) + 1).re = w.re + (j : ℝ) + 1 := by\n simp [Complex.add_re, Complex.natCast_re, Complex.one_re]\n have h4 : -‖w‖ ≤ w.re := (abs_le.mp (Complex.abs_re_le_norm w)).1\n linarith\n rw [halg, norm_div, norm_mul, hnorm1]\n have hA2 : (0 : ℝ) < ((j : ℝ) + 1) ^ 2 := by positivity\n have hden0 : (0 : ℝ) < ((j : ℝ) + 1) * ‖w + (j : ℂ) + 1‖ :=\n mul_pos hj1 (by linarith [hnorm2, hj1])\n rw [div_le_div_iff₀ hden0 hA2]\n nlinarith [hwn.le, hnorm2, hj1.le, sq_nonneg ((j : ℝ) + 1)]\n have htend : TendstoLocallyUniformlyOn\n (fun t : Finset ℕ => fun w => ∑ j ∈ t, (1 / ((j : ℂ) + 1) - 1 / (w + j + 1)))\n digammaSeriesPart atTop (Metric.ball 0 (1 / 2)) :=\n TendstoUniformlyOn.tendstoLocallyUniformlyOn\n (hasSumUniformlyOn_iff_tendstoUniformlyOn.mp hu)\n have hdiff : DifferentiableOn ℂ digammaSeriesPart (Metric.ball 0 (1 / 2)) := by\n apply htend.differentiableOn _ Metric.isOpen_ball\n apply Filter.Eventually.of_forall\n intro t w hw\n rw [show (fun w => ∑ j ∈ t, (1 / ((j : ℂ) + 1) - 1 / (w + j + 1)))\n = ∑ j ∈ t, (fun w => 1 / ((j : ℂ) + 1) - 1 / (w + j + 1)) from by\n funext w; simp [Finset.sum_apply]]\n apply DifferentiableAt.differentiableWithinAt\n apply DifferentiableAt.sum\n intro j _\n have hwj : w + (j : ℂ) + 1 ≠ 0 := add_nat_add_one_ne_zero_of_mem_ball hw j\n have h2 : DifferentiableAt ℂ (fun w : ℂ => 1 / (w + (j : ℂ) + 1)) w :=\n (differentiableAt_const (1 : ℂ)).div\n ((differentiableAt_id.add (differentiableAt_const _)).add (differentiableAt_const _))\n hwj\n exact (differentiableAt_const _).sub h2\n exact hdiff.analyticOnNhd Metric.isOpen_ball\n\n/-- The digamma series evaluation near 0 (punctured): for\nw ∈ ball(0, 1/2), w ≠ 0. -/\nlemma digamma_eq_seriesPart_near_zero {w : ℂ}\n (hw : w ∈ Metric.ball 0 (1 / 2)) (hw0 : w ≠ 0) :\n Complex.digamma w = -(Real.eulerMascheroniConstant : ℂ) - 1 / w + digammaSeriesPart w := by\n have hZ : w ∈ Complex.integerComplement := by\n intro k hk\n -- w = (k : ℤ): |k| < 1/2 forces k = 0\n have hmem := Metric.mem_ball.mp hw\n rw [dist_zero_right] at hmem\n rw [hk] at hmem\n have hk0 : (1 : ℝ) ≤ ‖(k : ℂ)‖ ∨ k = 0 := by\n by_cases hkz : k = 0\n · exact Or.inr hkz\n · left\n have h1 : (1 : ℤ) ≤ |k| := Int.one_le_abs hkz\n have h2 : ‖(k : ℂ)‖ = |(k : ℝ)| := by\n rw [show ((k : ℂ)) = (((k : ℝ)) : ℂ) by push_cast; ring, Complex.norm_ofReal]\n rw [h2]\n have h3 : (1 : ℝ) ≤ |(k : ℝ)| := by exact_mod_cast h1\n exact h3\n rcases hk0 with habs | hk0\n · linarith\n · exact hw0 (by rw [hk, hk0]; simp)\n have h := Zeta23.DigammaSeries.digamma_series hZ\n rw [h]\n rfl\n\n/-- The witness at s = 0: Fexpr agrees punctured with\nlogDeriv ζ − seriesFun + 1/(s−1) − (log π)/2 + (−γ + digammaSeriesPart(s/2))/2,\nanalytic at 0. -/\nlemma Fexpr_eventually_zero :\n ∃ W : ℂ → ℂ, AnalyticAt ℂ W 0 ∧ ∀ᶠ s in 𝓝[≠] (0 : ℂ), Fexpr s = W s := by\n have hA : AnalyticAt ℂ (logDeriv riemannZeta) 0 := by\n have hz : riemannZeta 0 ≠ 0 := by rw [riemannZeta_zero]; norm_num\n exact ((analyticAt_riemannZeta (by norm_num)).deriv).div\n (analyticAt_riemannZeta (by norm_num)) hz\n have hB : AnalyticAt ℂ seriesFun 0 := seriesFun_analyticAt (by\n intro h\n have hpos := h.2.1\n rw [Complex.zero_re] at hpos\n exact lt_irrefl 0 hpos)\n have hC : AnalyticAt ℂ (fun s : ℂ => 1 / (s - 1)) 0 := by\n apply AnalyticAt.div analyticAt_const _ (by norm_num : (0 : ℂ) - 1 ≠ 0)\n exact analyticAt_id.sub analyticAt_const\n have hD : AnalyticAt ℂ (fun _ : ℂ => (Real.log Real.pi : ℂ) / 2) 0 := analyticAt_const\n have hE : AnalyticAt ℂ\n (fun s => (-(Real.eulerMascheroniConstant : ℂ) + digammaSeriesPart (s / 2)) / 2) 0 := by\n apply AnalyticAt.div _ analyticAt_const (by norm_num : (2 : ℂ) ≠ 0)\n apply AnalyticAt.add analyticAt_const\n have h1 : AnalyticAt ℂ (fun s : ℂ => s / 2) 0 := by\n apply AnalyticAt.div analyticAt_id analyticAt_const (by norm_num)\n exact AnalyticAt.comp (f := fun s : ℂ => s / 2)\n (digammaSeriesPart_analyticOn 0 (Metric.mem_ball_self (by norm_num))) h1\n refine ⟨fun s => logDeriv riemannZeta s - seriesFun s + 1 / (s - 1)\n - (Real.log Real.pi : ℂ) / 2\n + (-(Real.eulerMascheroniConstant : ℂ) + digammaSeriesPart (s / 2)) / 2, ?_, ?_⟩\n · exact ((((hA.sub hB).add hC).sub hD).add hE)\n · -- punctured agreement on ball(0, 1/2)\n rw [Metric.eventually_nhdsWithin_iff]\n refine ⟨1 / 2, by norm_num, fun s hs => ?_⟩\n have hs0 : s ≠ 0 := hs.2\n have hsball : s ∈ Metric.ball 0 (1 / 2) := hs.1\n have hs2ball : s / 2 ∈ Metric.ball 0 (1 / 2) := by\n rw [Metric.mem_ball, dist_zero_right] at hsball ⊢\n rw [norm_div, RCLike.norm_ofNat]\n linarith\n have hs20 : s / 2 ≠ 0 := by\n intro h\n exact hs0 (by linear_combination 2 * h)\n have hdig := digamma_eq_seriesPart_near_zero hs2ball hs20\n show logDeriv riemannZeta s - seriesFun s + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : ℂ) / 2 + Complex.digamma (s / 2) / 2\n = logDeriv riemannZeta s - seriesFun s + 1 / (s - 1)\n - (Real.log Real.pi : ℂ) / 2\n + (-(Real.eulerMascheroniConstant : ℂ) + digammaSeriesPart (s / 2)) / 2\n rw [hdig]\n ring\n\n/-! ## 6. The digamma series minus a pole term, and the witness at s = −2n -/\n\n/-- ζ(−2n) = 0 for n ≥ 1 (from `zeroMult_neg_two_mul`: the order is 1). -/\nlemma riemannZeta_neg_two_mul {n : ℕ} (hn : 1 ≤ n) :\n riemannZeta (-2 * (n : ℂ)) = 0 := by\n by_contra h\n have hord := zeroMult_neg_two_mul n hn\n have hne1 : (-2 * (n : ℂ)) ≠ 1 := by\n intro hh\n have hre := congrArg Complex.re hh\n simp at hre\n have hn1 : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn\n linarith\n have h0 : analyticOrderAt riemannZeta (-2 * (n : ℂ)) = 0 :=\n (analyticAt_riemannZeta hne1).analyticOrderAt_eq_zero.mpr h\n have hmz : zeroMult (-2 * (n : ℂ)) = analyticOrderNatAt riemannZeta (-2 * (n : ℂ)) := rfl\n rw [hmz] at hord\n rw [h0] at hord\n simp at hord\n\n/-- Pole avoidance on ball(−n, 1/2) for j ≠ n−1: w + j + 1 ≠ 0. -/\nlemma add_nat_add_one_ne_zero_of_mem_ball_neg {n : ℕ} (hn : 1 ≤ n) {w : ℂ}\n (hw : w ∈ Metric.ball (-(n : ℂ)) (1 / 2)) {j : ℕ} (hj : j ≠ n - 1) :\n w + (j : ℂ) + 1 ≠ 0 := by\n intro h\n have h1 : w = -((j : ℂ) + 1) := by linear_combination h\n have h2 : dist w (-(n : ℂ)) < 1 / 2 := Metric.mem_ball.mp hw\n rw [h1, Complex.dist_eq] at h2\n have h3 : -((j : ℂ) + 1) - -(n : ℂ) = ((n : ℂ) - ((j : ℂ) + 1)) := by ring\n rw [h3] at h2\n have h4 : ‖((n : ℂ) - ((j : ℂ) + 1))‖ = |(n : ℝ) - ((j : ℝ) + 1)| := by\n rw [show (n : ℂ) - ((j : ℂ) + 1) = (((n : ℝ) - ((j : ℝ) + 1)) : ℂ) by push_cast; ring,\n Complex.norm_ofReal]\n rw [h4] at h2\n have hne : n ≠ j + 1 := by\n intro hc\n apply hj\n omega\n have h5 : (1 : ℝ) ≤ |(n : ℝ) - ((j : ℝ) + 1)| := by\n rcases lt_or_gt_of_ne hne with hlt | hgt\n · have h6 : (n : ℝ) + 1 ≤ (j : ℝ) + 1 := by\n exact_mod_cast Nat.succ_le_of_lt hlt\n rw [abs_of_neg (by linarith : (n : ℝ) - ((j : ℝ) + 1) < 0)]\n linarith\n · have h6 : (j : ℝ) + 1 + 1 ≤ (n : ℝ) := by\n exact_mod_cast Nat.succ_le_of_lt hgt\n rw [abs_of_pos (by linarith : 0 < (n : ℝ) - ((j : ℝ) + 1))]\n linarith\n linarith\n\n/-- The digamma series with the j = n−1 term dropped; analytic on\nball(−n, 1/2). -/\ndef digammaSeriesPartSub (n : ℕ) (w : ℂ) : ℂ :=\n ∑' j : ℕ, (if j = n - 1 then 0 else (1 / ((j : ℂ) + 1) - 1 / (w + j + 1)))\n\n/-- The dropped-term series is analytic on ball(−n, 1/2) (the eventually\nM-test with majorant (2n+1)/(j+1)² for j ≥ 2n+1). -/\nlemma digammaSeriesPartSub_analyticOn {n : ℕ} (hn : 1 ≤ n) :\n AnalyticOnNhd ℂ (digammaSeriesPartSub n) (Metric.ball (-(n : ℂ)) (1 / 2)) := by\n have hsum : Summable (fun j : ℕ => (2 * (n : ℝ) + 1) / ((j : ℝ) + 1) ^ 2) :=\n summable_div_add_one_sq _\n have hu : HasSumUniformlyOn\n (fun j => fun w : ℂ => (if j = n - 1 then 0 else (1 / ((j : ℂ) + 1) - 1 / (w + j + 1))))\n (digammaSeriesPartSub n) (Metric.ball (-(n : ℂ)) (1 / 2)) := by\n apply HasSumUniformlyOn.of_norm_le_summable_eventually hsum\n rw [eventually_cofinite]\n apply (Set.finite_Iio (2 * n + 1)).subset\n intro j hj\n show j < 2 * n + 1\n by_contra hj2\n push Not at hj2\n apply hj\n intro w hw\n have hwn : ‖w‖ < (n : ℝ) + 1 / 2 := by\n have h := Metric.mem_ball.mp hw\n rw [Complex.dist_eq] at h\n have htri : ‖w‖ ≤ ‖w - -(n : ℂ)‖ + ‖-(n : ℂ)‖ := by\n calc ‖w‖ = ‖(w - -(n : ℂ)) + -(n : ℂ)‖ := by congr 1; ring\n _ ≤ _ := norm_add_le _ _\n have hnnorm : ‖(-(n : ℂ))‖ = (n : ℝ) := by\n rw [norm_neg, RCLike.norm_natCast]\n linarith\n have hjne : j ≠ n - 1 := by omega\n rw [if_neg hjne]\n have hwj : w + (j : ℂ) + 1 ≠ 0 :=\n add_nat_add_one_ne_zero_of_mem_ball_neg hn hw hjne\n have hj0 : ((j : ℂ) + 1) ≠ 0 := Nat.cast_add_one_ne_zero j\n have halg : 1 / ((j : ℂ) + 1) - 1 / (w + j + 1)\n = w / (((j : ℂ) + 1) * (w + j + 1)) := by\n field_simp\n ring\n have hnorm1 : ‖((j : ℂ) + 1)‖ = (j : ℝ) + 1 := by\n have e : ((j : ℂ) + 1) = ((j + 1 : ℕ) : ℂ) := by push_cast; ring\n rw [e, RCLike.norm_natCast, Nat.cast_add, Nat.cast_one]\n have hj1 : (0 : ℝ) < (j : ℝ) + 1 := by positivity\n -- for j ≥ 2n+1: ‖w + j + 1‖ ≥ (j+1)/2\n have hnorm2 : ((j : ℝ) + 1) / 2 ≤ ‖w + (j : ℂ) + 1‖ := by\n have h2 : (w + (j : ℂ) + 1).re ≤ ‖w + (j : ℂ) + 1‖ := Complex.re_le_norm _\n have h3 : (w + (j : ℂ) + 1).re = w.re + (j : ℝ) + 1 := by\n simp [Complex.add_re, Complex.natCast_re, Complex.one_re]\n have h4 : -‖w‖ ≤ w.re := (abs_le.mp (Complex.abs_re_le_norm w)).1\n have hj2' : 2 * ((n : ℝ) + 1) ≤ (j : ℝ) + 1 := by\n have h5 : 2 * n + 2 ≤ j + 1 := by omega\n have h6 : (2 * n + 2 : ℕ) ≤ j + 1 := h5\n have h7 : ((2 * n + 2 : ℕ) : ℝ) ≤ ((j + 1 : ℕ) : ℝ) := by exact_mod_cast h6\n push_cast at h7\n linarith\n nlinarith [hwn]\n rw [halg, norm_div, norm_mul, hnorm1]\n have hA2 : (0 : ℝ) < ((j : ℝ) + 1) ^ 2 := by positivity\n have hden0 : (0 : ℝ) < ((j : ℝ) + 1) * ‖w + (j : ℂ) + 1‖ :=\n mul_pos hj1 (by linarith [hnorm2, hj1])\n rw [div_le_div_iff₀ hden0 hA2]\n have hn0 : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg n\n nlinarith [hwn.le, hnorm2, hj1.le, sq_nonneg ((j : ℝ) + 1), hn0]\n have htend : TendstoLocallyUniformlyOn\n (fun t : Finset ℕ => fun w =>\n ∑ j ∈ t, (if j = n - 1 then 0 else (1 / ((j : ℂ) + 1) - 1 / (w + j + 1))))\n (digammaSeriesPartSub n) atTop (Metric.ball (-(n : ℂ)) (1 / 2)) :=\n TendstoUniformlyOn.tendstoLocallyUniformlyOn\n (hasSumUniformlyOn_iff_tendstoUniformlyOn.mp hu)\n have hdiff : DifferentiableOn ℂ (digammaSeriesPartSub n)\n (Metric.ball (-(n : ℂ)) (1 / 2)) := by\n apply htend.differentiableOn _ Metric.isOpen_ball\n apply Filter.Eventually.of_forall\n intro t w hw\n rw [show (fun w => ∑ j ∈ t, (if j = n - 1 then 0\n else (1 / ((j : ℂ) + 1) - 1 / (w + j + 1))))\n = ∑ j ∈ t, (fun w => if j = n - 1 then 0\n else (1 / ((j : ℂ) + 1) - 1 / (w + j + 1))) from by\n funext w; simp [Finset.sum_apply]]\n apply DifferentiableAt.differentiableWithinAt\n apply DifferentiableAt.sum\n intro j _\n by_cases hj : j = n - 1\n · show DifferentiableAt ℂ (fun w => if j = n - 1 then (0 : ℂ)\n else (1 / ((j : ℂ) + 1) - 1 / (w + j + 1))) w\n simp only [if_pos hj]\n exact differentiableAt_const 0\n · have hwj : w + (j : ℂ) + 1 ≠ 0 :=\n add_nat_add_one_ne_zero_of_mem_ball_neg hn hw hj\n show DifferentiableAt ℂ (fun w => if j = n - 1 then (0 : ℂ)\n else (1 / ((j : ℂ) + 1) - 1 / (w + j + 1))) w\n simp only [if_neg hj]\n have h2 : DifferentiableAt ℂ (fun w : ℂ => 1 / (w + (j : ℂ) + 1)) w :=\n (differentiableAt_const (1 : ℂ)).div\n ((differentiableAt_id.add (differentiableAt_const _)).add (differentiableAt_const _))\n hwj\n exact (differentiableAt_const _).sub h2\n exact hdiff.analyticOnNhd Metric.isOpen_ball\n\n/-- The single-term split: for w ∈ ball(−n, 1/2), w ≠ −n,\ndigammaSeriesPart w = digammaSeriesPartSub n w + (1/n − 1/(w+n)). -/\nlemma digammaSeriesPart_eq_sub_add_single {n : ℕ} (hn : 1 ≤ n) {w : ℂ}\n (hw : w ∈ Metric.ball (-(n : ℂ)) (1 / 2)) (hwn : w ≠ -(n : ℂ)) :\n digammaSeriesPart w\n = digammaSeriesPartSub n w + (1 / (n : ℂ) - 1 / (w + (n : ℂ))) := by\n have hZ : w ∈ Complex.integerComplement := by\n intro k hk\n -- w = (k:ℤ) with dist w (−n) < 1/2 forces k = −n\n have h2 : dist w (-(n : ℂ)) < 1 / 2 := Metric.mem_ball.mp hw\n rw [hk, Complex.dist_eq] at h2\n have h3 : (k : ℂ) - -(n : ℂ) = ((k + (n : ℤ)) : ℂ) := by push_cast; ring\n rw [h3, show (((k + (n : ℤ)) : ℂ)) = (((k + (n : ℤ) : ℤ) : ℝ) : ℂ) by push_cast; ring,\n Complex.norm_ofReal] at h2\n have h4 : |(k : ℝ) + (n : ℝ)| < 1 / 2 := by\n have : |(k + (n : ℤ) : ℝ)| < 1 / 2 := by\n have h5 : (((k + (n : ℤ) : ℤ) : ℝ) : ℂ) = ((k + (n : ℤ) : ℤ) : ℝ) := rfl\n -- h2 : ‖↑(↑(k + ↑n))‖ < 1/2 after the rws; normalize\n convert h2 using 2\n push_cast\n ring\n rwa [show ((k + (n : ℤ)) : ℝ) = (k : ℝ) + (n : ℝ) by push_cast; ring] at this\n have hk0 : k = -(n : ℤ) := by\n by_contra hkne\n have h1 : (1 : ℤ) ≤ |k + (n : ℤ)| := Int.one_le_abs (by\n intro hh\n exact hkne (neg_eq_of_add_eq_zero_left (by linear_combination hh)))\n have h1r : (1 : ℝ) ≤ |(k : ℝ) + (n : ℝ)| := by\n have e : |(k : ℝ) + (n : ℝ)| = (|k + (n : ℤ)| : ℝ) := by\n rw [show (k : ℝ) + (n : ℝ) = ((k + (n : ℤ) : ℤ) : ℝ) by push_cast; ring,\n RCLike.norm_natCast]\n rw [e]\n exact_mod_cast h1\n linarith\n exact hwn (by rw [hk, hk0]; push_cast; ring)\n have hfull : Summable (fun j : ℕ => 1 / ((j : ℂ) + 1) - 1 / (w + j + 1)) :=\n Zeta23.DigammaSeries.summable_digamma_series hZ\n have hsub : Summable (fun j : ℕ => if j = n - 1 then (0 : ℂ)\n else (1 / ((j : ℂ) + 1) - 1 / (w + j + 1))) := by\n apply Summable.of_norm_bounded hfull.norm\n intro j\n by_cases hjj : j = n - 1 <;> simp [hjj]\n have hsingle : Summable (fun j : ℕ => if j = n - 1\n then (1 / ((j : ℂ) + 1) - 1 / (w + j + 1)) else (0 : ℂ)) := by\n apply summable_of_hasFiniteSupport ((Set.finite_singleton (n - 1)).subset ?_)\n intro j hj\n rw [Function.mem_support, ne_eq] at hj\n by_contra h\n apply hj\n rw [if_neg (fun he => h (Set.mem_singleton_iff.mpr he))]\n have htsum : ∑' j, (if j = n - 1 then (1 / ((j : ℂ) + 1) - 1 / (w + j + 1)) else (0 : ℂ))\n = 1 / (n : ℂ) - 1 / (w + (n : ℂ)) := by\n rw [tsum_eq_single (n - 1) (fun j hj => if_neg hj)]\n rw [if_pos rfl]\n congr 1\n · rw [Nat.cast_sub hn, Nat.cast_one]\n ring\n · congr 1\n rw [Nat.cast_sub hn, Nat.cast_one]\n ring\n calc digammaSeriesPart w\n = ∑' j, (1 / ((j : ℂ) + 1) - 1 / (w + j + 1)) := rfl\n _ = ∑' j, ((if j = n - 1 then (0 : ℂ) else (1 / ((j : ℂ) + 1) - 1 / (w + j + 1)))\n + (if j = n - 1 then (1 / ((j : ℂ) + 1) - 1 / (w + j + 1)) else (0 : ℂ))) := by\n apply tsum_congr\n intro j\n by_cases hjj : j = n - 1 <;> simp [hjj]\n _ = digammaSeriesPartSub n w\n + ∑' j, (if j = n - 1 then (1 / ((j : ℂ) + 1) - 1 / (w + j + 1)) else (0 : ℂ)) :=\n Summable.tsum_add hsub hsingle\n _ = digammaSeriesPartSub n w + (1 / (n : ℂ) - 1 / (w + (n : ℂ))) := by rw [htsum]\n\n/-- H_n: digamma plus its pole term at −n, minus the pole — analytic on\nball(−n, 1/2). -/\ndef Hsub (n : ℕ) (w : ℂ) : ℂ :=\n -(Real.eulerMascheroniConstant : ℂ) - 1 / w + digammaSeriesPartSub n w + 1 / (n : ℂ)\n\n/-- The punctured digamma split at −n: digamma w = −1/(w+n) + H_n w. -/\nlemma digamma_eq_neg_inv_add_Hsub {n : ℕ} (hn : 1 ≤ n) {w : ℂ}\n (hw : w ∈ Metric.ball (-(n : ℂ)) (1 / 2)) (hwn : w ≠ -(n : ℂ)) :\n Complex.digamma w = -1 / (w + (n : ℂ)) + Hsub n w := by\n have hZ : w ∈ Complex.integerComplement := by\n intro k hk\n have h2 : dist w (-(n : ℂ)) < 1 / 2 := Metric.mem_ball.mp hw\n rw [hk, Complex.dist_eq] at h2\n have h3 : (k : ℂ) - -(n : ℂ) = ((k + (n : ℤ)) : ℂ) := by push_cast; ring\n rw [h3, show (((k + (n : ℤ)) : ℂ)) = (((k + (n : ℤ) : ℤ) : ℝ) : ℂ) by push_cast; ring,\n Complex.norm_ofReal] at h2\n have h4 : |(k : ℝ) + (n : ℝ)| < 1 / 2 := by\n have h5 : |(k + (n : ℤ) : ℝ)| < 1 / 2 := by\n convert h2 using 2\n push_cast\n ring\n rwa [show ((k + (n : ℤ)) : ℝ) = (k : ℝ) + (n : ℝ) by push_cast; ring] at h5\n have hk0 : k = -(n : ℤ) := by\n by_contra hkne\n have h1 : (1 : ℤ) ≤ |k + (n : ℤ)| := Int.one_le_abs (by\n intro hh\n exact hkne (neg_eq_of_add_eq_zero_left (by linear_combination hh)))\n have h1r : (1 : ℝ) ≤ |(k : ℝ) + (n : ℝ)| := by\n have e : |(k : ℝ) + (n : ℝ)| = (|k + (n : ℤ)| : ℝ) := by\n rw [show (k : ℝ) + (n : ℝ) = ((k + (n : ℤ) : ℤ) : ℝ) by push_cast; ring,\n RCLike.norm_natCast]\n rw [e]\n exact_mod_cast h1\n linarith\n exact hwn (by rw [hk, hk0]; push_cast; ring)\n have hdig := Zeta23.DigammaSeries.digamma_series hZ\n have hsplit := digammaSeriesPart_eq_sub_add_single hn hw hwn\n rw [hdig, Hsub, hsplit]\n ring\n\n/-- H_n is analytic at −n. -/\nlemma Hsub_analyticAt {n : ℕ} (hn : 1 ≤ n) :\n AnalyticAt ℂ (Hsub n) (-(n : ℂ)) := by\n have hA : AnalyticAt ℂ (fun _ : ℂ => -(Real.eulerMascheroniConstant : ℂ)) _ := analyticAt_const\n have hB : AnalyticAt ℂ (fun w : ℂ => 1 / w) (-(n : ℂ)) := by\n apply AnalyticAt.div analyticAt_const analyticAt_id\n simp\n positivity\n have hC : AnalyticAt ℂ (digammaSeriesPartSub n) (-(n : ℂ)) :=\n digammaSeriesPartSub_analyticOn hn (-(n : ℂ)) (Metric.mem_ball_self (by norm_num))\n have hD : AnalyticAt ℂ (fun _ : ℂ => 1 / (n : ℂ)) _ := analyticAt_const\n show AnalyticAt ℂ (fun w => -(Real.eulerMascheroniConstant : ℂ) - 1 / w\n + digammaSeriesPartSub n w + 1 / (n : ℂ)) (-(n : ℂ))\n exact (((hA.sub hB).add hC).add hD)\n\n/-- The witness at s = −2n (n ≥ 1): Fexpr agrees punctured with\nWtriv − seriesFun + 1/s + 1/(s−1) − (log π)/2 + H_n(s/2)/2. -/\nlemma Fexpr_eventually_neg_two_mul {n : ℕ} (hn : 1 ≤ n) :\n ∃ W : ℂ → ℂ, AnalyticAt ℂ W (-2 * (n : ℂ)) ∧\n ∀ᶠ s in 𝓝[≠] (-2 * (n : ℂ)), Fexpr s = W s := by\n have hζ := riemannZeta_neg_two_mul hn\n have hne1 : (-2 * (n : ℂ)) ≠ 1 := by\n intro hh\n have hre := congrArg Complex.re hh\n simp at hre\n have hn1 : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn\n linarith\n obtain ⟨Wtriv, hWtriv, hWtrivEq⟩ := logDeriv_zeta_sub_mult_div_eventually hζ hne1\n have hmult : zeroMult (-2 * (n : ℂ)) = 1 := zeroMult_neg_two_mul n hn\n -- the pieces\n have hB : AnalyticAt ℂ seriesFun (-2 * (n : ℂ)) := seriesFun_analyticAt (by\n intro h\n have hpos := h.2.1\n have hre : (-2 * (n : ℂ)).re = -2 * (n : ℝ) := by simp\n rw [hre] at hpos\n have hn1 : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn\n linarith)\n have hC : AnalyticAt ℂ (fun s : ℂ => 1 / s) (-2 * (n : ℂ)) := by\n apply AnalyticAt.div analyticAt_const analyticAt_id\n simp\n positivity\n have hC1 : AnalyticAt ℂ (fun s : ℂ => 1 / (s - 1)) (-2 * (n : ℂ)) := by\n apply AnalyticAt.div analyticAt_const _ (by\n have hn1 : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn\n intro hh\n have hre := congrArg Complex.re hh\n simp at hre\n linarith)\n exact analyticAt_id.sub analyticAt_const\n have hD : AnalyticAt ℂ (fun _ : ℂ => (Real.log Real.pi : ℂ) / 2) _ := analyticAt_const\n have hE : AnalyticAt ℂ (fun s => Hsub n (s / 2) / 2) (-2 * (n : ℂ)) := by\n apply AnalyticAt.div _ analyticAt_const (by norm_num : (2 : ℂ) ≠ 0)\n have h1 : AnalyticAt ℂ (fun s : ℂ => s / 2) (-2 * (n : ℂ)) := by\n apply AnalyticAt.div analyticAt_id analyticAt_const (by norm_num)\n have hval : (-2 * (n : ℂ)) / 2 = -(n : ℂ) := by ring\n rw [← hval]\n exact AnalyticAt.comp (f := fun s : ℂ => s / 2) (Hsub_analyticAt hn) h1\n refine ⟨fun s => Wtriv s - seriesFun s + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : ℂ) / 2 + Hsub n (s / 2) / 2, ?_, ?_⟩\n · exact ((((hWtriv.sub hB).add hC).add hC1).sub hD).add hE\n · -- punctured agreement on ball(−2n, 1) (then s/2 ∈ ball(−n, 1/2))\n rw [Metric.eventually_nhdsWithin_iff]\n refine ⟨1, by norm_num, fun s hs => ?_⟩\n have hs0 : s ≠ -2 * (n : ℂ) := hs.2\n have hsball : s ∈ Metric.ball (-2 * (n : ℂ)) 1 := hs.1\n have hs2ball : s / 2 ∈ Metric.ball (-(n : ℂ)) (1 / 2) := by\n rw [Metric.mem_ball, Complex.dist_eq] at hsball ⊢\n have e : s / 2 - -(n : ℂ) = (s - -2 * (n : ℂ)) / 2 := by ring\n rw [e, norm_div, RCLike.norm_ofNat]\n linarith\n have hs20 : s / 2 ≠ -(n : ℂ) := by\n intro h\n exact hs0 (by linear_combination 2 * h)\n have hdig := digamma_eq_neg_inv_add_Hsub hn hs2ball hs20\n -- logDeriv split: logDeriv ζ s = Wtriv s + 1/(s + 2n)\n have hlog : logDeriv riemannZeta s = Wtriv s + 1 / (s + 2 * (n : ℂ)) := by\n have h := hWtrivEq\n rw [Metric.eventually_nhdsWithin_iff] at h\n obtain ⟨ε, hε, hball⟩ := h\n have hmem : s ∈ Metric.ball (-2 * (n : ℂ)) ε ∧ s ≠ -2 * (n : ℂ) := by\n have h1 : dist s (-2 * (n : ℂ)) < 1 := Metric.mem_ball.mp hs.1\n have h2 : dist s (-2 * (n : ℂ)) < ε ∨ ε ≤ dist s (-2 * (n : ℂ)) := lt_or_ge _ _\n rcases h2 with h2 | h2\n · exact ⟨Metric.mem_ball.mpr h2, hs0⟩\n · -- if ε ≤ dist, shrink: use min form — but we need the point bound;\n -- the punctured ball from hball covers dist < ε only; handle by\n -- noting dist < 1 and re-deriving with min ε 1 below\n exfalso\n -- ε ≤ dist s (−2n) < 1; the punctured agreement at s is not\n -- available — instead use the eventually form directly\n exact absurd h2 (not_le.mpr h1)\n have h3 := hball s hmem.1 hmem.2\n rw [hmult] at h3\n have e : s - -2 * (n : ℂ) = s + 2 * (n : ℂ) := by ring\n rw [e] at h3\n -- h3 : logDeriv ζ s − (1:ℂ)/(s + 2n) = Wtriv s\n rw [show (1 : ℂ) = ((1 : ℕ) : ℂ) from by simp] at h3\n rw [← Nat.cast_one] at h3\n have h3' : logDeriv riemannZeta s - (1 : ℂ) / (s + 2 * (n : ℂ)) = Wtriv s := by\n convert h3 using 2\n simp\n linear_combination h3'\n show logDeriv riemannZeta s - seriesFun s + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : ℂ) / 2 + Complex.digamma (s / 2) / 2\n = Wtriv s - seriesFun s + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : ℂ) / 2 + Hsub n (s / 2) / 2\n rw [hlog, hdig]\n have h1 : -1 / (s / 2 + (n : ℂ)) / 2 = -1 / (s + 2 * (n : ℂ)) := by\n have e : s / 2 + (n : ℂ) = (s + 2 * (n : ℂ)) / 2 := by ring\n rw [e]\n field_simp\n ring\n linear_combination h1\n\nend NguyenRH1\n\nend"},"extra_content":null}]