LiFEntire.lean

Declarations

Source

/-
NguyenRH1/LiFEntire.lean — tier ii′ sub-stage ii′-5e-iv (D-068 §4):
the partial-fraction difference function

  Fexpr s := logDeriv ζ s − seriesFun s + 1/s + 1/(s−1) − (log π)/2 + ψ(s/2)/2

is ENTIRE. The excluded set is

  badPoint s := IsNontrivialZero s ∨ s = 0 ∨ s = 1 ∨ ∃ n ≥ 1, s = −2n;

at each bad point the principal parts cancel exactly (D-068 §0's residue
bookkeeping: +m vs +m at nontrivial zeros; −1 vs −1 at 1; 0 = −1+1 at 0;
+1 vs +1 at −2n). Since Mathlib lacks a general removable-singularity
theorem, entirety is packaged via the punctured-limit extension

  Gentire s := limUnder (𝓝[≠] s) Fexpr:

at GOOD points Fexpr is analytic (hence the punctured limit is the
value), at each BAD point an explicit analytic witness agrees with Fexpr
on a punctured neighbourhood (the principal-part splits), so Gentire is
everywhere analytic and agrees with Fexpr at every good point
(`gentire_analyticAt`, `gentire_eq_Fexpr`).

The witnesses:
* nontrivial zero ρ₀: [logDeriv ζ − m/(s−ρ₀)] analytic by the order
  normal form (`logDeriv_zeta_sub_mult_div_eventually`, the LiSides NF
  block) + [seriesFun − m/(s−ρ₀)] analytic by 5e-iii's
  `seriesFun_sub_polar_analyticAt`; the elementary terms analytic since
  re ρ₀ ∈ (0, 1) avoids 0, 1, −2n.
* s = 1: logDeriv ζ + 1/(s−1) = logDeriv zetaA punctured (zetaA
  analytic, zetaA 1 = 1 — ii′-1b).
* s = 0: ψ(s/2)/2 + 1/s = −γ/2 + ½·digammaSeriesPart(s/2) punctured
  (the digamma series, Zeta23 `DigammaSeries.digamma_series`; the series
  part analytic on ball(0, 1/2) by the M-test); logDeriv ζ analytic at
  0 (ζ(0) = −1/2 ≠ 0).
* s = −2n: logDeriv ζ − 1/(s+2n) analytic (NF + `zeroMult_neg_two_mul`,
  session 026); ψ(s/2)/2 + 1/(s+2n) = ½·H_n(s/2) punctured where H_n is
  the digamma series with the j = n−1 term dropped (analytic on
  ball(−n, 1/2) by the eventually M-test).

Also proved: `zeta_zero_classification` (every zero of ζ is nontrivial,
0, or −2n — from Zeta23's `completedRiemannZeta_eq_zero_iff` +
`Gammaℝ_eq_zero_iff`) and `analyticAt_digamma` (ψ analytic off
{0} ∪ −ℕ).

Archive references: D-068 §4, journal-028 (the series machinery),
journal-017 (the NF block), journal-026 (zeroMult(−2n)).
-/
import Mathlib
import Zeta23.Statement
import Zeta23.RvM.CountByIntegral
import Zeta23.GammaFacts.Series
import NguyenRH1.LiSeries
import NguyenRH1.LiTrivialZeros
import NguyenRH1.LiDigamma

open Zeta23 Complex Filter Topology

noncomputable section

namespace NguyenRH1

/-! ## 0. The difference function and the excluded set -/

/-- The partial-fraction difference function (D-068 §0):
ζ′/ζ − series + 1/s + 1/(s−1) − ½log π + ½ψ(s/2); entire after the
punctured-limit extension (`Gentire`). -/
def Fexpr (s : ℂ) : ℂ :=
  logDeriv riemannZeta s - seriesFun s + 1 / s + 1 / (s - 1)
    - (Real.log Real.pi : ℂ) / 2 + Complex.digamma (s / 2) / 2

/-- The excluded set of the partial-fraction identity: the nontrivial
zeros, 0, 1, and the trivial zeros −2n (n ≥ 1). -/
def badPoint (s : ℂ) : Prop :=
  IsNontrivialZero s ∨ s = 0 ∨ s = 1 ∨ ∃ n : ℕ, 1 ≤ n ∧ s = -2 * (n : ℂ)

/-! ## 1. Digamma is analytic off {0} ∪ −ℕ -/

/-- ψ = logDeriv Γ is analytic at any w ∉ {0} ∪ −ℕ (the finite-min ball
avoiding the poles; Γ analytic + nonzero there). -/
lemma analyticAt_digamma {w : ℂ} (hw : ∀ m : ℕ, w ≠ -(m : ℂ)) :
    AnalyticAt ℂ Complex.digamma w := by
  set M : ℕ := ⌈‖w‖⌉₊ with hM
  have hMle : ‖w‖ ≤ M := Nat.le_ceil _
  set d : Finset ℝ := (Finset.range (M + 2)).image (fun m : ℕ => ‖w + (m : ℂ)‖) with hd
  have hdne : d.Nonempty := by
    refine ⟨‖w‖, ?_⟩
    rw [hd]
    refine Finset.mem_image.mpr ⟨0, Finset.mem_range.mpr (by omega), ?_⟩
    simp
  have hdpos : ∀ x ∈ d, 0 < x := by
    intro x hx
    rw [hd] at hx
    obtain ⟨m, -, rfl⟩ := Finset.mem_image.mp hx
    rw [norm_pos_iff]
    intro hz
    exact hw m (eq_neg_of_add_eq_zero_left hz)
  have hmin0 : 0 < d.min' hdne := hdpos _ (Finset.min'_mem _ _)
  set δ : ℝ := min (1 / 2) (d.min' hdne / 2) with hδ
  have hδ0 : 0 < δ := lt_min (by norm_num) (half_pos hmin0)
  have hδ1 : δ ≤ 1 / 2 := min_le_left _ _
  have hδ2 : δ ≤ d.min' hdne / 2 := min_le_right _ _
  -- every point of ball(w, δ) avoids the poles
  have hball : ∀ y ∈ Metric.ball w δ, ∀ m : ℕ, y ≠ -(m : ℂ) := by
    intro y hy m hye
    have hdist : ‖y - w‖ < δ := by
      have := Metric.mem_ball.mp hy
      rwa [dist_eq_norm] at this
    by_cases hm : m < M + 2
    · have hmem : ‖w + (m : ℂ)‖ ∈ d := by
        rw [hd]
        exact Finset.mem_image.mpr ⟨m, Finset.mem_range.mpr hm, rfl⟩
      have hle : d.min' hdne ≤ ‖w + (m : ℂ)‖ := Finset.min'_le _ _ hmem
      have hnm : ‖y + (m : ℂ)‖ = 0 := by rw [hye]; simp
      have hnorm : ‖w + (m : ℂ)‖ ≤ ‖y + (m : ℂ)‖ + ‖y - w‖ := by
        calc ‖w + (m : ℂ)‖ = ‖(y + (m : ℂ)) - (y - w)‖ := by congr 1; ring
          _ ≤ ‖y + (m : ℂ)‖ + ‖y - w‖ := norm_sub_le _ _
      rw [hnm] at hnorm
      simp at hnorm
      linarith
    · push Not at hm
      have hnm : y + (m : ℂ) = 0 := by rw [hye]; simp
      have hnorm : (m : ℝ) ≤ ‖y + (m : ℂ)‖ + ‖y‖ := by
        calc (m : ℝ) = ‖(m : ℂ)‖ := (RCLike.norm_natCast m).symm
          _ = ‖(y + (m : ℂ)) - y‖ := by congr 1; ring
          _ ≤ ‖y + (m : ℂ)‖ + ‖y‖ := norm_sub_le _ _
      rw [hnm] at hnorm
      simp at hnorm
      have hyw : ‖y‖ ≤ ‖y - w‖ + ‖w‖ := by
        calc ‖y‖ = ‖(y - w) + w‖ := by congr 1; ring
          _ ≤ ‖y - w‖ + ‖w‖ := norm_add_le _ _
      have hmM : M + 2 ≤ m := by omega
      have hmre : (M : ℝ) + 2 ≤ (m : ℝ) := by exact_mod_cast hmM
      linarith [hMle, hdist, hδ1]
  -- Γ analytic on the ball
  have hGammaOn : DifferentiableOn ℂ Complex.Gamma (Metric.ball w δ) := by
    intro y hy
    exact Complex.differentiableAt_Gamma y (hball y hy) |>.differentiableWithinAt
  have hGammaAn : AnalyticOnNhd ℂ Complex.Gamma (Metric.ball w δ) :=
    hGammaOn.analyticOnNhd Metric.isOpen_ball
  have hAn : AnalyticOnNhd ℂ (fun z => deriv Complex.Gamma z / Complex.Gamma z)
      (Metric.ball w δ) := by
    intro y hy
    exact ((hGammaAn y hy).deriv).div (hGammaAn y hy)
      (Complex.Gamma_ne_zero (hball y hy))
  have heq : Complex.digamma = fun z => deriv Complex.Gamma z / Complex.Gamma z := by
    funext z
    rw [digamma_def, logDeriv_apply]
  rw [heq]
  exact hAn w (Metric.mem_ball_self hδ0)

/-- ψ(s/2)/2 is analytic wherever s/2 avoids the poles. -/
lemma analyticAt_digamma_div_two {s : ℂ} (h : ∀ m : ℕ, s / 2 ≠ -(m : ℂ)) :
    AnalyticAt ℂ (fun s => Complex.digamma (s / 2) / 2) s := by
  have h1 : AnalyticAt ℂ (fun s : ℂ => s / 2) s := by
    apply AnalyticAt.div analyticAt_id analyticAt_const (by norm_num)
  have h2 : AnalyticAt ℂ (Complex.digamma ∘ fun s : ℂ => s / 2) s :=
    AnalyticAt.comp (f := fun s : ℂ => s / 2) (analyticAt_digamma h) h1
  apply AnalyticAt.div _ analyticAt_const (by norm_num : (2 : ℂ) ≠ 0)
  exact h2

/-! ## 2. The zero classification -/

/-- Every zero of ζ is a nontrivial zero, 0, or a trivial zero −2n
(from Zeta23's `completedRiemannZeta_eq_zero_iff` via the ΓR-pole case
split; `riemannZeta_ne_zero_of_one_le_re` excludes re ≥ 1). -/
lemma zeta_zero_classification {s : ℂ} (hs : riemannZeta s = 0) :
    IsNontrivialZero s ∨ s = 0 ∨ ∃ n : ℕ, 1 ≤ n ∧ s = -2 * (n : ℂ) := by
  by_cases h1 : 1 ≤ s.re
  · exact absurd hs (riemannZeta_ne_zero_of_one_le_re h1)
  · push Not at h1
    by_cases h0 : 0 < s.re
    · exact Or.inl ⟨hs, h0, h1⟩
    · push Not at h0
      by_cases hs0 : s = 0
      · exact Or.inr (Or.inl hs0)
      · by_cases hG : Complex.Gammaℝ s = 0
        · rw [Complex.Gammaℝ_eq_zero_iff] at hG
          obtain ⟨n, hn⟩ := hG
          rcases Nat.eq_zero_or_pos n with hn0 | hnpos
          · subst hn0
            simp at hn
            exact absurd hn hs0
          · exact Or.inr (Or.inr ⟨n, hnpos, by rw [hn]; ring⟩)
        · have hΛ : completedRiemannZeta s = 0 := by
            rw [RvM.completedRiemannZeta_eq_Gammaℝ_mul hs0 hG, hs, mul_zero]
          have hpos := (RvM.completedRiemannZeta_eq_zero_iff.mp hΛ).2.1
          linarith

/-! ## 3. The logDeriv normal-form witness at a zero -/

/-- At a zero ρ₀ ≠ 1 of ζ, the subtraction of the polar term
mult(ρ₀)/(s−ρ₀) from logDeriv ζ agrees punctured with an analytic
function (the logDeriv of the NF factor h). Unified witness for the
nontrivial and the trivial zeros (the LiSides NF block). -/
lemma logDeriv_zeta_sub_mult_div_eventually {ρ₀ : ℂ} (_hζ : riemannZeta ρ₀ = 0)
    (hρ1 : ρ₀ ≠ 1) :
    ∃ W : ℂ → ℂ, AnalyticAt ℂ W ρ₀ ∧
      ∀ᶠ s in 𝓝[≠] ρ₀, logDeriv riemannZeta s - (zeroMult ρ₀ : ℂ) / (s - ρ₀) = W s := by
  have hρα : AnalyticAt ℂ riemannZeta ρ₀ := analyticAt_riemannZeta hρ1
  obtain ⟨h, hh, hh0, hfh⟩ := hρα.analyticOrderAt_ne_top.mp (zeta_order_ne_top_of_ne hρ1)
  refine ⟨logDeriv h, hh.deriv.div hh hh0, ?_⟩
  filter_upwards [self_mem_nhdsWithin,
    mem_nhdsWithin_of_mem_nhds hfh.eventually_nhds,
    mem_nhdsWithin_of_mem_nhds (hh.continuousAt.eventually_ne hh0),
    mem_nhdsWithin_of_mem_nhds hh.eventually_analyticAt] with s hsρ hfhs hhs hhas
  have hfhs' : riemannZeta =ᶠ[𝓝 s]
      (fun z => (z - ρ₀) ^ analyticOrderNatAt riemannZeta ρ₀ • h z) := hfhs
  have hsρ' : s - ρ₀ ≠ 0 := sub_ne_zero.mpr hsρ
  have hld : logDeriv riemannZeta s =
      (analyticOrderNatAt riemannZeta ρ₀ : ℂ) / (s - ρ₀) + logDeriv h s := by
    have e1 : logDeriv riemannZeta s =
        logDeriv (fun z => (z - ρ₀) ^ analyticOrderNatAt riemannZeta ρ₀ * h z) s := by
      simp only [logDeriv_apply, hfhs'.deriv_eq, hfhs'.self_of_nhds, smul_eq_mul]
    rw [e1, logDeriv_mul (f := fun z : ℂ => (z - ρ₀) ^ analyticOrderNatAt riemannZeta ρ₀)
      (g := h) s (pow_ne_zero _ hsρ') hhs (by fun_prop) hhas.differentiableAt]
    have e2 : logDeriv (fun z : ℂ => (z - ρ₀) ^ analyticOrderNatAt riemannZeta ρ₀) s
        = (analyticOrderNatAt riemannZeta ρ₀ : ℂ) / (s - ρ₀) := by
      rw [show (fun z : ℂ => (z - ρ₀) ^ analyticOrderNatAt riemannZeta ρ₀)
          = (fun x : ℂ => x ^ analyticOrderNatAt riemannZeta ρ₀) ∘ (fun z => z - ρ₀)
          from rfl,
        logDeriv_comp (by fun_prop) (by fun_prop), logDeriv_pow]
      simp
    rw [e2]
  have hmz : (zeroMult ρ₀ : ℂ) = (analyticOrderNatAt riemannZeta ρ₀ : ℂ) := rfl
  rw [hld, hmz]
  ring

/-! ## 4. The witness at s = 1 -/

/-- Near s = 1 (punctured): logDeriv ζ s = logDeriv zetaA s − 1/(s−1). -/
lemma logDeriv_zeta_eq_logDeriv_zetaA_sub :
    ∀ᶠ s in 𝓝[≠] (1 : ℂ),
      logDeriv riemannZeta s = logDeriv zetaA s - 1 / (s - 1) := by
  filter_upwards [self_mem_nhdsWithin,
    mem_nhdsWithin_of_mem_nhds zetaA_ne_zero_near_one] with s hs1 hZA
  have hs1' : s - 1 ≠ 0 := sub_ne_zero.mpr hs1
  have hζ : riemannZeta s ≠ 0 := by
    have e := zetaA_apply hs1
    intro hz
    rw [hz, mul_zero] at e
    exact hZA e
  have hcong : zetaA =ᶠ[𝓝 s] (fun w : ℂ => (w - 1) * riemannZeta w) := by
    filter_upwards [eventually_ne_nhds hs1] with z hz using zetaA_apply hz
  have hld : logDeriv zetaA s = 1 / (s - 1) + logDeriv riemannZeta s := by
    have e1 : logDeriv zetaA s = logDeriv (fun w : ℂ => (w - 1) * riemannZeta w) s := by
      simp only [logDeriv_apply, hcong.deriv_eq, hcong.self_of_nhds]
    rw [e1, logDeriv_mul (f := fun w : ℂ => w - 1) (g := riemannZeta) s hs1' hζ
      (differentiableAt_id.sub (differentiableAt_const 1))
      (analyticAt_riemannZeta hs1).differentiableAt]
    have e2 : logDeriv (fun w : ℂ => w - 1) s = 1 / (s - 1) := by
      have hd : deriv (fun w : ℂ => w - 1) s = 1 :=
        ((hasDerivAt_id s).sub_const (1 : ℂ)).deriv
      rw [logDeriv_apply, hd]
    rw [e2]
  rw [hld]
  ring

/-- The witness at s = 1: Fexpr agrees punctured with
logDeriv zetaA − seriesFun + 1/s − (log π)/2 + ψ(s/2)/2, analytic at 1. -/
lemma Fexpr_eventually_one :
    ∃ W : ℂ → ℂ, AnalyticAt ℂ W 1 ∧ ∀ᶠ s in 𝓝[≠] (1 : ℂ), Fexpr s = W s := by
  have h1dig : ∀ m : ℕ, (1 : ℂ) / 2 ≠ -(m : ℂ) := by
    intro m h
    have hre := congrArg Complex.re h
    simp at hre
    have hm : (0 : ℝ) ≤ (m : ℝ) := Nat.cast_nonneg m
    linarith
  refine ⟨fun s => logDeriv zetaA s - seriesFun s + 1 / s - (Real.log Real.pi : ℂ) / 2
      + Complex.digamma (s / 2) / 2, ?_, ?_⟩
  · have hA : AnalyticAt ℂ (logDeriv zetaA) 1 :=
      (zetaA_analyticAt_one.deriv).div zetaA_analyticAt_one (by rw [zetaA_one]; norm_num)
    have hB : AnalyticAt ℂ seriesFun 1 := seriesFun_analyticAt (by
      intro h
      have hlt := h.2.2
      rw [Complex.one_re] at hlt
      exact lt_irrefl 1 hlt)
    have hC : AnalyticAt ℂ (fun s : ℂ => 1 / s) 1 :=
      analyticAt_const.div analyticAt_id (by norm_num)
    have hD : AnalyticAt ℂ (fun s : ℂ => (Real.log Real.pi : ℂ) / 2) 1 := analyticAt_const
    have hE : AnalyticAt ℂ (fun s => Complex.digamma (s / 2) / 2) 1 :=
      analyticAt_digamma_div_two h1dig
    exact ((((hA.sub hB).add hC).sub hD).add hE)
  · filter_upwards [logDeriv_zeta_eq_logDeriv_zetaA_sub] with s hs
    show logDeriv riemannZeta s - seriesFun s + 1 / s + 1 / (s - 1)
        - (Real.log Real.pi : ℂ) / 2 + Complex.digamma (s / 2) / 2
      = logDeriv zetaA s - seriesFun s + 1 / s - (Real.log Real.pi : ℂ) / 2
        + Complex.digamma (s / 2) / 2
    rw [hs]
    ring

/-! ## 5. The digamma series part and the witness at s = 0 -/

/-- The series part of the digamma partial-fraction expansion
Σ'_j (1/(j+1) − 1/(w+j+1)); analytic on ball(0, 1/2). -/
def digammaSeriesPart (w : ℂ) : ℂ :=
  ∑' j : ℕ, (1 / ((j : ℂ) + 1) - 1 / (w + j + 1))

/-- A point of ball(−n, 1/2) other than −n is not an integer
(the integer lattice is 1-separated). -/
lemma integerComplement_of_mem_ball_neg_natCast {n : ℕ} {w : ℂ}
    (hw : w ∈ Metric.ball (-(n : ℂ)) (1 / 2)) (hwn : w ≠ -(n : ℂ)) :
    w ∈ Complex.integerComplement := by
  intro hk
  obtain ⟨k, rfl⟩ := hk
  have h2 : dist (k : ℂ) (-(n : ℂ)) < 1 / 2 := Metric.mem_ball.mp hw
  rw [Complex.dist_eq] at h2
  by_cases hk0 : k = -(n : ℤ)
  · exact hwn (by rw [hk0]; push_cast; ring)
  · have h1 : (1 : ℤ) ≤ |k + (n : ℤ)| := Int.one_le_abs (by
      intro hh
      exact hk0 (eq_neg_of_add_eq_zero_left hh))
    have h3 : (k : ℂ) - -(n : ℂ) = (k : ℂ) + ((n : ℤ) : ℂ) := by push_cast; ring
    rw [h3] at h2
    have h4 : (1 : ℝ) ≤ ‖(k : ℂ) + ((n : ℤ) : ℂ)‖ := by
      have h6 : |((k : ℂ) + ((n : ℤ) : ℂ)).re| ≤ ‖(k : ℂ) + ((n : ℤ) : ℂ)‖ :=
        Complex.abs_re_le_norm _
      have hre : ((k : ℂ) + ((n : ℤ) : ℂ)).re = (k : ℝ) + (n : ℝ) := by
        simp [Complex.add_re]
      rw [hre] at h6
      have h5 : (1 : ℝ) ≤ |(k : ℝ) + (n : ℝ)| := by
        have e : |(k : ℝ) + (n : ℝ)| = ((|k + (n : ℤ)| : ℤ) : ℝ) := by
          rw [show (k : ℝ) + (n : ℝ) = (((k + (n : ℤ)) : ℤ) : ℝ) by push_cast; ring,
            Int.cast_abs]
        rw [e]
        exact_mod_cast h1
      exact h5.trans h6
    linarith

/-- Pole avoidance on ball(0, 1/2): w + j + 1 ≠ 0. -/
lemma add_nat_add_one_ne_zero_of_mem_ball {w : ℂ} (hw : w ∈ Metric.ball 0 (1 / 2)) (j : ℕ) :
    w + (j : ℂ) + 1 ≠ 0 := by
  have hwn : ‖w‖ < 1 / 2 := by
    have h := Metric.mem_ball.mp hw
    rwa [dist_zero_right] at h
  intro h
  have h1 : (w + (j : ℂ) + 1).re = w.re + (j : ℝ) + 1 := by
    simp [Complex.add_re, Complex.natCast_re, Complex.one_re]
  rw [h] at h1
  simp at h1
  have h2 : -‖w‖ ≤ w.re := (abs_le.mp (Complex.abs_re_le_norm w)).1
  have hj0 : (0 : ℝ) ≤ (j : ℝ) := Nat.cast_nonneg j
  linarith

/-- The digamma series part is analytic on ball(0, 1/2) (M-test,
Σ 1/(j+1)² majorant). -/
lemma digammaSeriesPart_analyticOn :
    AnalyticOnNhd ℂ digammaSeriesPart (Metric.ball 0 (1 / 2)) := by
  have hsum : Summable (fun j : ℕ => (1 : ℝ) / ((j : ℝ) + 1) ^ 2) :=
    summable_div_add_one_sq 1
  have hu : HasSumUniformlyOn (fun (j : ℕ) => fun w : ℂ => 1 / ((j : ℂ) + 1) - 1 / (w + j + 1))
      (fun w => ∑' j : ℕ, (1 / ((j : ℂ) + 1) - 1 / (w + j + 1)))
      (Metric.ball 0 (1 / 2)) := by
    apply HasSumUniformlyOn.of_norm_le_summable hsum
    intro j w hw
    have hwn : ‖w‖ < 1 / 2 := by
      have h := Metric.mem_ball.mp hw
      rwa [dist_zero_right] at h
    have hj1 : (0 : ℝ) < (j : ℝ) + 1 := by positivity
    have hwj : w + (j : ℂ) + 1 ≠ 0 := add_nat_add_one_ne_zero_of_mem_ball hw j
    have hj0 : ((j : ℂ) + 1) ≠ 0 := Nat.cast_add_one_ne_zero j
    have halg : 1 / ((j : ℂ) + 1) - 1 / (w + j + 1)
        = w / (((j : ℂ) + 1) * (w + j + 1)) := by
      field_simp
      ring
    have hnorm1 : ‖((j : ℂ) + 1)‖ = (j : ℝ) + 1 := by
      have e : ((j : ℂ) + 1) = ((j + 1 : ℕ) : ℂ) := by push_cast; ring
      rw [e, RCLike.norm_natCast, Nat.cast_add, Nat.cast_one]
    have hnorm2 : ((j : ℝ) + 1) / 2 ≤ ‖w + (j : ℂ) + 1‖ := by
      have h2 : (w + (j : ℂ) + 1).re ≤ ‖w + (j : ℂ) + 1‖ := Complex.re_le_norm _
      have h3 : (w + (j : ℂ) + 1).re = w.re + (j : ℝ) + 1 := by
        simp [Complex.add_re, Complex.natCast_re, Complex.one_re]
      have h4 : -‖w‖ ≤ w.re := (abs_le.mp (Complex.abs_re_le_norm w)).1
      linarith
    rw [halg, norm_div, norm_mul, hnorm1]
    have hA2 : (0 : ℝ) < ((j : ℝ) + 1) ^ 2 := by positivity
    have hden0 : (0 : ℝ) < ((j : ℝ) + 1) * ‖w + (j : ℂ) + 1‖ :=
      mul_pos hj1 (by linarith [hnorm2, hj1])
    rw [div_le_div_iff₀ hden0 hA2]
    nlinarith [hwn.le, hnorm2, hj1.le, sq_nonneg ((j : ℝ) + 1)]
  have htend : TendstoLocallyUniformlyOn
      (fun t : Finset ℕ => fun w => ∑ j ∈ t, (1 / ((j : ℂ) + 1) - 1 / (w + j + 1)))
      (fun w => ∑' j : ℕ, (1 / ((j : ℂ) + 1) - 1 / (w + j + 1)))
      atTop (Metric.ball 0 (1 / 2)) :=
    TendstoUniformlyOn.tendstoLocallyUniformlyOn
      (hasSumUniformlyOn_iff_tendstoUniformlyOn.mp hu)
  have hdiff : DifferentiableOn ℂ (fun w => ∑' j : ℕ, (1 / ((j : ℂ) + 1) - 1 / (w + j + 1)))
      (Metric.ball 0 (1 / 2)) := by
    apply htend.differentiableOn _ Metric.isOpen_ball
    apply Filter.Eventually.of_forall
    intro t w hw
    rw [show (fun w => ∑ j ∈ t, (1 / ((j : ℂ) + 1) - 1 / (w + j + 1)))
        = ∑ j ∈ t, (fun w => 1 / ((j : ℂ) + 1) - 1 / (w + j + 1)) from by
      funext w; simp [Finset.sum_apply]]
    apply DifferentiableAt.differentiableWithinAt
    apply DifferentiableAt.sum
    intro j _
    have hwj : w + (j : ℂ) + 1 ≠ 0 := add_nat_add_one_ne_zero_of_mem_ball hw j
    have h2 : DifferentiableAt ℂ (fun w : ℂ => 1 / (w + (j : ℂ) + 1)) w :=
      (differentiableAt_const (1 : ℂ)).div
        ((differentiableAt_id.add (differentiableAt_const _)).add (differentiableAt_const _))
        hwj
    exact (differentiableAt_const _).sub h2
  have hdiff2 : DifferentiableOn ℂ digammaSeriesPart (Metric.ball 0 (1 / 2)) := hdiff
  exact hdiff2.analyticOnNhd Metric.isOpen_ball

/-- The digamma series evaluation near 0 (punctured): for
w ∈ ball(0, 1/2), w ≠ 0. -/
lemma digamma_eq_seriesPart_near_zero {w : ℂ}
    (hw : w ∈ Metric.ball 0 (1 / 2)) (hw0 : w ≠ 0) :
    Complex.digamma w = -(Real.eulerMascheroniConstant : ℂ) - 1 / w + digammaSeriesPart w := by
  have hZ : w ∈ Complex.integerComplement :=
    integerComplement_of_mem_ball_neg_natCast (n := 0) (by simpa using hw) (by simpa using hw0)
  have h := Zeta23.DigammaSeries.digamma_series hZ
  rw [h]
  rfl

/-- The witness at s = 0: Fexpr agrees punctured with
logDeriv ζ − seriesFun + 1/(s−1) − (log π)/2 + (−γ + digammaSeriesPart(s/2))/2,
analytic at 0. -/
lemma Fexpr_eventually_zero :
    ∃ W : ℂ → ℂ, AnalyticAt ℂ W 0 ∧ ∀ᶠ s in 𝓝[≠] (0 : ℂ), Fexpr s = W s := by
  have hA : AnalyticAt ℂ (logDeriv riemannZeta) 0 := by
    have hz : riemannZeta 0 ≠ 0 := by rw [riemannZeta_zero]; norm_num
    exact ((analyticAt_riemannZeta (by norm_num)).deriv).div
      (analyticAt_riemannZeta (by norm_num)) hz
  have hB : AnalyticAt ℂ seriesFun 0 := seriesFun_analyticAt (by
    intro h
    have hpos := h.2.1
    rw [Complex.zero_re] at hpos
    exact lt_irrefl 0 hpos)
  have hC : AnalyticAt ℂ (fun s : ℂ => 1 / (s - 1)) 0 := by
    apply AnalyticAt.div analyticAt_const (g := fun s : ℂ => s - 1) _ (by norm_num)
    exact analyticAt_id.sub analyticAt_const
  have hD : AnalyticAt ℂ (fun _ : ℂ => (Real.log Real.pi : ℂ) / 2) 0 := analyticAt_const
  have hE : AnalyticAt ℂ
      (fun s => (-(Real.eulerMascheroniConstant : ℂ) + digammaSeriesPart (s / 2)) / 2) 0 := by
    apply AnalyticAt.div _ analyticAt_const (by norm_num : (2 : ℂ) ≠ 0)
    apply AnalyticAt.add analyticAt_const
    have h1 : AnalyticAt ℂ (fun s : ℂ => s / 2) 0 := by
      apply AnalyticAt.div analyticAt_id analyticAt_const (by norm_num)
    have hdsp0 : AnalyticAt ℂ digammaSeriesPart ((0 : ℂ) / 2) := by
      rw [zero_div]
      exact digammaSeriesPart_analyticOn 0 (Metric.mem_ball_self (by norm_num))
    exact AnalyticAt.comp (f := fun s : ℂ => s / 2) hdsp0 h1
  refine ⟨fun s => logDeriv riemannZeta s - seriesFun s + 1 / (s - 1)
      - (Real.log Real.pi : ℂ) / 2
      + (-(Real.eulerMascheroniConstant : ℂ) + digammaSeriesPart (s / 2)) / 2, ?_, ?_⟩
  · exact ((((hA.sub hB).add hC).sub hD).add hE)
  · -- punctured agreement on ball(0, 1/2)
    rw [eventually_nhdsWithin_iff, Metric.eventually_nhds_iff_ball]
    refine ⟨1 / 2, by norm_num, fun s hsball hsne => ?_⟩
    have hs0 : s ≠ 0 := hsne
    have hs2ball : s / 2 ∈ Metric.ball 0 (1 / 2) := by
      rw [Metric.mem_ball, dist_zero_right] at hsball ⊢
      rw [norm_div, RCLike.norm_ofNat]
      linarith
    have hs20 : s / 2 ≠ 0 := by
      intro h
      exact hs0 (by linear_combination 2 * h)
    have hdig := digamma_eq_seriesPart_near_zero hs2ball hs20
    show logDeriv riemannZeta s - seriesFun s + 1 / s + 1 / (s - 1)
        - (Real.log Real.pi : ℂ) / 2 + Complex.digamma (s / 2) / 2
      = logDeriv riemannZeta s - seriesFun s + 1 / (s - 1)
        - (Real.log Real.pi : ℂ) / 2
        + (-(Real.eulerMascheroniConstant : ℂ) + digammaSeriesPart (s / 2)) / 2
    rw [hdig]
    ring

/-! ## 6. The digamma series minus a pole term, and the witness at s = −2n -/

/-- ζ(−2n) = 0 for n ≥ 1 (from `zeroMult_neg_two_mul`: the order is 1). -/
lemma riemannZeta_neg_two_mul {n : ℕ} (hn : 1 ≤ n) :
    riemannZeta (-2 * (n : ℂ)) = 0 := by
  by_contra h
  have hord := zeroMult_neg_two_mul n hn
  have hne1 : (-2 * (n : ℂ)) ≠ 1 := by
    intro hh
    have hre := congrArg Complex.re hh
    simp at hre
    have hn1 : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
    linarith
  have h0 : analyticOrderAt riemannZeta (-2 * (n : ℂ)) = 0 :=
    (analyticAt_riemannZeta hne1).analyticOrderAt_eq_zero.mpr h
  have hmz : zeroMult (-2 * (n : ℂ)) = analyticOrderNatAt riemannZeta (-2 * (n : ℂ)) := rfl
  rw [hmz] at hord
  simp only [analyticOrderNatAt] at hord
  rw [h0] at hord
  simp at hord

/-- Pole avoidance on ball(−n, 1/2) for j ≠ n−1: w + j + 1 ≠ 0. -/
lemma add_nat_add_one_ne_zero_of_mem_ball_neg {n : ℕ} (hn : 1 ≤ n) {w : ℂ}
    (hw : w ∈ Metric.ball (-(n : ℂ)) (1 / 2)) {j : ℕ} (hj : j ≠ n - 1) :
    w + (j : ℂ) + 1 ≠ 0 := by
  intro h
  have h1 : w = -((j : ℂ) + 1) := by linear_combination h
  have h2 : dist w (-(n : ℂ)) < 1 / 2 := Metric.mem_ball.mp hw
  rw [h1, Complex.dist_eq] at h2
  have h3 : -((j : ℂ) + 1) - -(n : ℂ) = ((n : ℂ) - ((j : ℂ) + 1)) := by ring
  rw [h3] at h2
  have hne : n ≠ j + 1 := by
    intro hc
    apply hj
    omega
  have h5 : (1 : ℝ) ≤ |(n : ℝ) - ((j : ℝ) + 1)| := by
    rcases lt_or_gt_of_ne hne with hlt | hgt
    · have h6 : (n : ℝ) + 1 ≤ (j : ℝ) + 1 := by
        exact_mod_cast Nat.succ_le_of_lt hlt
      rw [abs_of_neg (by linarith : (n : ℝ) - ((j : ℝ) + 1) < 0)]
      linarith
    · have h6 : (j : ℝ) + 1 + 1 ≤ (n : ℝ) := by
        exact_mod_cast Nat.succ_le_of_lt hgt
      rw [abs_of_pos (by linarith : 0 < (n : ℝ) - ((j : ℝ) + 1))]
      linarith
  have h6 : |((n : ℂ) - ((j : ℂ) + 1)).re| ≤ ‖(n : ℂ) - ((j : ℂ) + 1)‖ :=
    Complex.abs_re_le_norm _
  have hre : ((n : ℂ) - ((j : ℂ) + 1)).re = (n : ℝ) - ((j : ℝ) + 1) := by
    simp [Complex.sub_re, Complex.add_re, Complex.natCast_re, Complex.one_re]
  rw [hre] at h6
  linarith [h2, h5, h6]

/-- The digamma series with the j = n−1 term dropped; analytic on
ball(−n, 1/2). -/
def digammaSeriesPartSub (n : ℕ) (w : ℂ) : ℂ :=
  ∑' j : ℕ, (if j = n - 1 then 0 else (1 / ((j : ℂ) + 1) - 1 / (w + j + 1)))

/-- The dropped-term series is analytic on ball(−n, 1/2) (the eventually
M-test with majorant (2n+1)/(j+1)² for j ≥ 2n+1). -/
lemma digammaSeriesPartSub_analyticOn {n : ℕ} (hn : 1 ≤ n) :
    AnalyticOnNhd ℂ (digammaSeriesPartSub n) (Metric.ball (-(n : ℂ)) (1 / 2)) := by
  have hsum : Summable (fun j : ℕ => (2 * (n : ℝ) + 1) / ((j : ℝ) + 1) ^ 2) :=
    summable_div_add_one_sq _
  have hu : HasSumUniformlyOn
      (fun (j : ℕ) => fun w : ℂ =>
        (if j = n - 1 then 0 else (1 / ((j : ℂ) + 1) - 1 / (w + j + 1))))
      (fun w => ∑' j : ℕ, (if j = n - 1 then (0 : ℂ)
        else (1 / ((j : ℂ) + 1) - 1 / (w + j + 1))))
      (Metric.ball (-(n : ℂ)) (1 / 2)) := by
    apply HasSumUniformlyOn.of_norm_le_summable_eventually hsum
    rw [eventually_cofinite]
    apply (Set.finite_Iio (2 * n + 1)).subset
    intro j hj
    show j < 2 * n + 1
    by_contra hj2
    push Not at hj2
    apply hj
    intro w hw
    have hwn : ‖w‖ < (n : ℝ) + 1 / 2 := by
      have h := Metric.mem_ball.mp hw
      rw [Complex.dist_eq] at h
      have htri : ‖w‖ ≤ ‖w - -(n : ℂ)‖ + ‖-(n : ℂ)‖ := by
        calc ‖w‖ = ‖(w - -(n : ℂ)) + -(n : ℂ)‖ := by congr 1; ring
          _ ≤ _ := norm_add_le _ _
      have hnnorm : ‖(-(n : ℂ))‖ = (n : ℝ) := by
        rw [norm_neg, RCLike.norm_natCast]
      linarith
    have hjne : j ≠ n - 1 := by omega
    rw [if_neg hjne]
    have hwj : w + (j : ℂ) + 1 ≠ 0 :=
      add_nat_add_one_ne_zero_of_mem_ball_neg hn hw hjne
    have hj0 : ((j : ℂ) + 1) ≠ 0 := Nat.cast_add_one_ne_zero j
    have halg : 1 / ((j : ℂ) + 1) - 1 / (w + j + 1)
        = w / (((j : ℂ) + 1) * (w + j + 1)) := by
      field_simp
      ring
    have hnorm1 : ‖((j : ℂ) + 1)‖ = (j : ℝ) + 1 := by
      have e : ((j : ℂ) + 1) = ((j + 1 : ℕ) : ℂ) := by push_cast; ring
      rw [e, RCLike.norm_natCast, Nat.cast_add, Nat.cast_one]
    have hj1 : (0 : ℝ) < (j : ℝ) + 1 := by positivity
    -- for j ≥ 2n+1: ‖w + j + 1‖ ≥ (j+1)/2
    have hnorm2 : ((j : ℝ) + 1) / 2 ≤ ‖w + (j : ℂ) + 1‖ := by
      have h2 : (w + (j : ℂ) + 1).re ≤ ‖w + (j : ℂ) + 1‖ := Complex.re_le_norm _
      have h3 : (w + (j : ℂ) + 1).re = w.re + (j : ℝ) + 1 := by
        simp [Complex.add_re, Complex.natCast_re, Complex.one_re]
      have h4 : -‖w‖ ≤ w.re := (abs_le.mp (Complex.abs_re_le_norm w)).1
      have hj2' : 2 * ((n : ℝ) + 1) ≤ (j : ℝ) + 1 := by
        have h5 : 2 * n + 2 ≤ j + 1 := by omega
        have h6 : (2 * n + 2 : ℕ) ≤ j + 1 := h5
        have h7 : ((2 * n + 2 : ℕ) : ℝ) ≤ ((j + 1 : ℕ) : ℝ) := by exact_mod_cast h6
        push_cast at h7
        linarith
      nlinarith [hwn]
    rw [halg, norm_div, norm_mul, hnorm1]
    have hA2 : (0 : ℝ) < ((j : ℝ) + 1) ^ 2 := by positivity
    have hden0 : (0 : ℝ) < ((j : ℝ) + 1) * ‖w + (j : ℂ) + 1‖ :=
      mul_pos hj1 (by linarith [hnorm2, hj1])
    rw [div_le_div_iff₀ hden0 hA2]
    have hn0 : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg n
    have h21 : (0 : ℝ) ≤ 2 * (n : ℝ) + 1 := by linarith
    have hstep1 : ((j : ℝ) + 1) ^ 2 / 2 ≤ ((j : ℝ) + 1) * ‖w + (j : ℂ) + 1‖ := by
      have h := mul_le_mul_of_nonneg_left hnorm2 hj1.le
      nlinarith [h]
    have hstep2 : (2 * (n : ℝ) + 1) * (((j : ℝ) + 1) ^ 2 / 2)
        ≤ (2 * (n : ℝ) + 1) * (((j : ℝ) + 1) * ‖w + (j : ℂ) + 1‖) :=
      mul_le_mul_of_nonneg_left hstep1 h21
    have hstep3 : ‖w‖ * ((j : ℝ) + 1) ^ 2 ≤ ((n : ℝ) + 1 / 2) * ((j : ℝ) + 1) ^ 2 :=
      mul_le_mul_of_nonneg_right hwn.le (sq_nonneg _)
    linarith [hstep2, hstep3]
  have htend : TendstoLocallyUniformlyOn
      (fun t : Finset ℕ => fun w =>
        ∑ j ∈ t, (if j = n - 1 then 0 else (1 / ((j : ℂ) + 1) - 1 / (w + j + 1))))
      (fun w => ∑' j : ℕ, (if j = n - 1 then (0 : ℂ)
        else (1 / ((j : ℂ) + 1) - 1 / (w + j + 1))))
      atTop (Metric.ball (-(n : ℂ)) (1 / 2)) :=
    TendstoUniformlyOn.tendstoLocallyUniformlyOn
      (hasSumUniformlyOn_iff_tendstoUniformlyOn.mp hu)
  have hdiff : DifferentiableOn ℂ (fun w => ∑' j : ℕ, (if j = n - 1 then (0 : ℂ)
        else (1 / ((j : ℂ) + 1) - 1 / (w + j + 1))))
      (Metric.ball (-(n : ℂ)) (1 / 2)) := by
    apply htend.differentiableOn _ Metric.isOpen_ball
    apply Filter.Eventually.of_forall
    intro t w hw
    rw [show (fun w => ∑ j ∈ t, (if j = n - 1 then 0
          else (1 / ((j : ℂ) + 1) - 1 / (w + j + 1))))
        = ∑ j ∈ t, (fun w => if j = n - 1 then 0
          else (1 / ((j : ℂ) + 1) - 1 / (w + j + 1))) from by
      funext w; simp [Finset.sum_apply]]
    apply DifferentiableAt.differentiableWithinAt
    apply DifferentiableAt.sum
    intro j _
    by_cases hj : j = n - 1
    · show DifferentiableAt ℂ (fun w => if j = n - 1 then (0 : ℂ)
          else (1 / ((j : ℂ) + 1) - 1 / (w + j + 1))) w
      simp only [if_pos hj]
      exact differentiableAt_const 0
    · have hwj : w + (j : ℂ) + 1 ≠ 0 :=
        add_nat_add_one_ne_zero_of_mem_ball_neg hn hw hj
      show DifferentiableAt ℂ (fun w => if j = n - 1 then (0 : ℂ)
          else (1 / ((j : ℂ) + 1) - 1 / (w + j + 1))) w
      simp only [if_neg hj]
      have h2 : DifferentiableAt ℂ (fun w : ℂ => 1 / (w + (j : ℂ) + 1)) w :=
        (differentiableAt_const (1 : ℂ)).div
          ((differentiableAt_id.add (differentiableAt_const _)).add (differentiableAt_const _))
          hwj
      exact (differentiableAt_const _).sub h2
  have hdiff2 : DifferentiableOn ℂ (digammaSeriesPartSub n)
      (Metric.ball (-(n : ℂ)) (1 / 2)) := hdiff
  exact hdiff2.analyticOnNhd Metric.isOpen_ball

/-- The single-term split: for w ∈ ball(−n, 1/2), w ≠ −n,
digammaSeriesPart w = digammaSeriesPartSub n w + (1/n − 1/(w+n)). -/
lemma digammaSeriesPart_eq_sub_add_single {n : ℕ} (hn : 1 ≤ n) {w : ℂ}
    (hw : w ∈ Metric.ball (-(n : ℂ)) (1 / 2)) (hwn : w ≠ -(n : ℂ)) :
    digammaSeriesPart w
      = digammaSeriesPartSub n w + (1 / (n : ℂ) - 1 / (w + (n : ℂ))) := by
  have hZ : w ∈ Complex.integerComplement :=
    integerComplement_of_mem_ball_neg_natCast hw hwn
  have hfull : Summable (fun j : ℕ => 1 / ((j : ℂ) + 1) - 1 / (w + j + 1)) :=
    Zeta23.DigammaSeries.summable_digamma_series hZ
  have hsub : Summable (fun j : ℕ => if j = n - 1 then (0 : ℂ)
      else (1 / ((j : ℂ) + 1) - 1 / (w + j + 1))) := by
    apply Summable.of_norm_bounded hfull.norm
    intro j
    by_cases hjj : j = n - 1 <;> simp [hjj]
  have hsingle : Summable (fun j : ℕ => if j = n - 1
      then (1 / ((j : ℂ) + 1) - 1 / (w + j + 1)) else (0 : ℂ)) := by
    apply summable_of_hasFiniteSupport ((Set.finite_singleton (n - 1)).subset ?_)
    intro j hj
    rw [Function.mem_support, ne_eq] at hj
    by_contra h
    apply hj
    rw [if_neg (fun he => h (Set.mem_singleton_iff.mpr he))]
  have htsum : ∑' j, (if j = n - 1 then (1 / ((j : ℂ) + 1) - 1 / (w + j + 1)) else (0 : ℂ))
      = 1 / (n : ℂ) - 1 / (w + (n : ℂ)) := by
    rw [tsum_eq_single (n - 1) (fun j hj => if_neg hj)]
    rw [if_pos rfl]
    congr 1
    · rw [Nat.cast_sub hn, Nat.cast_one]
      ring
    · congr 1
      rw [Nat.cast_sub hn, Nat.cast_one]
      ring
  calc digammaSeriesPart w
      = ∑' (j : ℕ), (1 / ((j : ℂ) + 1) - 1 / (w + (j : ℂ) + 1)) := rfl
    _ = ∑' (j : ℕ), ((if j = n - 1 then (0 : ℂ) else (1 / ((j : ℂ) + 1) - 1 / (w + (j : ℂ) + 1)))
        + (if j = n - 1 then (1 / ((j : ℂ) + 1) - 1 / (w + (j : ℂ) + 1)) else (0 : ℂ))) := by
        apply tsum_congr
        intro j
        by_cases hjj : j = n - 1 <;> simp [hjj]
    _ = digammaSeriesPartSub n w
        + ∑' j, (if j = n - 1 then (1 / ((j : ℂ) + 1) - 1 / (w + j + 1)) else (0 : ℂ)) :=
        Summable.tsum_add hsub hsingle
    _ = digammaSeriesPartSub n w + (1 / (n : ℂ) - 1 / (w + (n : ℂ))) := by rw [htsum]

/-- H_n: digamma plus its pole term at −n, minus the pole — analytic on
ball(−n, 1/2). -/
def Hsub (n : ℕ) (w : ℂ) : ℂ :=
  -(Real.eulerMascheroniConstant : ℂ) - 1 / w + digammaSeriesPartSub n w + 1 / (n : ℂ)

/-- The punctured digamma split at −n: digamma w = −1/(w+n) + H_n w. -/
lemma digamma_eq_neg_inv_add_Hsub {n : ℕ} (hn : 1 ≤ n) {w : ℂ}
    (hw : w ∈ Metric.ball (-(n : ℂ)) (1 / 2)) (hwn : w ≠ -(n : ℂ)) :
    Complex.digamma w = -1 / (w + (n : ℂ)) + Hsub n w := by
  have hZ : w ∈ Complex.integerComplement :=
    integerComplement_of_mem_ball_neg_natCast hw hwn
  have hdig := Zeta23.DigammaSeries.digamma_series hZ
  have hsplit := digammaSeriesPart_eq_sub_add_single hn hw hwn
  rw [hdig]
  show -(Real.eulerMascheroniConstant : ℂ) - 1 / w + digammaSeriesPart w
      = -1 / (w + (n : ℂ)) + (-(Real.eulerMascheroniConstant : ℂ) - 1 / w
        + digammaSeriesPartSub n w + 1 / (n : ℂ))
  rw [hsplit]
  ring

/-- H_n is analytic at −n. -/
lemma Hsub_analyticAt {n : ℕ} (hn : 1 ≤ n) :
    AnalyticAt ℂ (Hsub n) (-(n : ℂ)) := by
  have hA : AnalyticAt ℂ (fun _ : ℂ => -(Real.eulerMascheroniConstant : ℂ)) (-(n : ℂ)) :=
    analyticAt_const
  have hB : AnalyticAt ℂ (fun w : ℂ => 1 / w) (-(n : ℂ)) := by
    apply AnalyticAt.div analyticAt_const analyticAt_id (show (-(n : ℂ)) ≠ 0 by
      simp only [ne_eq, neg_eq_zero, Nat.cast_eq_zero]
      omega)
  have hC : AnalyticAt ℂ (digammaSeriesPartSub n) (-(n : ℂ)) :=
    digammaSeriesPartSub_analyticOn hn (-(n : ℂ)) (Metric.mem_ball_self (by norm_num))
  have hD : AnalyticAt ℂ (fun _ : ℂ => 1 / (n : ℂ)) (-(n : ℂ)) := analyticAt_const
  show AnalyticAt ℂ (fun w => -(Real.eulerMascheroniConstant : ℂ) - 1 / w
      + digammaSeriesPartSub n w + 1 / (n : ℂ)) (-(n : ℂ))
  exact (((hA.sub hB).add hC).add hD)

/-- The witness at s = −2n (n ≥ 1): Fexpr agrees punctured with
Wtriv − seriesFun + 1/s + 1/(s−1) − (log π)/2 + H_n(s/2)/2. -/
lemma Fexpr_eventually_neg_two_mul {n : ℕ} (hn : 1 ≤ n) :
    ∃ W : ℂ → ℂ, AnalyticAt ℂ W (-2 * (n : ℂ)) ∧
      ∀ᶠ s in 𝓝[≠] (-2 * (n : ℂ)), Fexpr s = W s := by
  have hζ := riemannZeta_neg_two_mul hn
  have hne1 : (-2 * (n : ℂ)) ≠ 1 := by
    intro hh
    have hre := congrArg Complex.re hh
    simp at hre
    have hn1 : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
    linarith
  obtain ⟨Wtriv, hWtriv, hWtrivEq⟩ := logDeriv_zeta_sub_mult_div_eventually hζ hne1
  rw [eventually_nhdsWithin_iff, Metric.eventually_nhds_iff_ball] at hWtrivEq
  obtain ⟨ε, hε, hWtrivEq⟩ := hWtrivEq
  have hmult : zeroMult (-2 * (n : ℂ)) = 1 := zeroMult_neg_two_mul n hn
  -- the pieces
  have hB : AnalyticAt ℂ seriesFun (-2 * (n : ℂ)) := seriesFun_analyticAt (by
    intro h
    have hpos := h.2.1
    have hre : (-2 * (n : ℂ)).re = -2 * (n : ℝ) := by simp
    rw [hre] at hpos
    have hn1 : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
    linarith)
  have hC : AnalyticAt ℂ (fun s : ℂ => 1 / s) (-2 * (n : ℂ)) := by
    apply AnalyticAt.div analyticAt_const analyticAt_id (by
      have hn0 : (n : ℂ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
      exact mul_ne_zero (by norm_num) hn0)
  have hC1 : AnalyticAt ℂ (fun s : ℂ => 1 / (s - 1)) (-2 * (n : ℂ)) := by
    apply AnalyticAt.div analyticAt_const (g := fun s : ℂ => s - 1) _ (by
      have hn1 : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
      intro hh
      have hre := congrArg Complex.re hh
      simp at hre
      linarith)
    exact analyticAt_id.sub analyticAt_const
  have hD : AnalyticAt ℂ (fun _ : ℂ => (Real.log Real.pi : ℂ) / 2) (-2 * (n : ℂ)) :=
    analyticAt_const
  have hE : AnalyticAt ℂ (fun s => Hsub n (s / 2) / 2) (-2 * (n : ℂ)) := by
    apply AnalyticAt.div _ analyticAt_const (by norm_num : (2 : ℂ) ≠ 0)
    have h1 : AnalyticAt ℂ (fun s : ℂ => s / 2) (-2 * (n : ℂ)) := by
      apply AnalyticAt.div analyticAt_id analyticAt_const (by norm_num)
    have hg : AnalyticAt ℂ (Hsub n) ((-2 * (n : ℂ)) / 2) := by
      rw [show (-2 * (n : ℂ)) / 2 = -(n : ℂ) by ring]
      exact Hsub_analyticAt hn
    exact AnalyticAt.comp (f := fun s : ℂ => s / 2) hg h1
  refine ⟨fun s => Wtriv s - seriesFun s + 1 / s + 1 / (s - 1)
      - (Real.log Real.pi : ℂ) / 2 + Hsub n (s / 2) / 2, ?_, ?_⟩
  · exact ((((hWtriv.sub hB).add hC).add hC1).sub hD).add hE
  · -- punctured agreement on ball(−2n, min 1 ε) (then s/2 ∈ ball(−n, 1/2))
    rw [eventually_nhdsWithin_iff, Metric.eventually_nhds_iff_ball]
    refine ⟨min 1 ε, lt_min (by norm_num) hε, fun s hsball hsne => ?_⟩
    have hs0 : s ≠ -2 * (n : ℂ) := hsne
    have hsdist : dist s (-2 * (n : ℂ)) < 1 ∧ dist s (-2 * (n : ℂ)) < ε := by
      have h := Metric.mem_ball.mp hsball
      constructor <;> linarith [h, min_le_left 1 ε, min_le_right 1 ε]
    have hs2ball : s / 2 ∈ Metric.ball (-(n : ℂ)) (1 / 2) := by
      rw [Metric.mem_ball, Complex.dist_eq]
      have e : s / 2 - -(n : ℂ) = (s - -2 * (n : ℂ)) / 2 := by ring
      rw [e, norm_div, RCLike.norm_ofNat]
      have h := Metric.mem_ball.mp hsball
      rw [Complex.dist_eq] at h
      linarith [h, min_le_left 1 ε]
    have hs20 : s / 2 ≠ -(n : ℂ) := by
      intro h
      exact hs0 (by linear_combination 2 * h)
    have hdig := digamma_eq_neg_inv_add_Hsub hn hs2ball hs20
    -- logDeriv split: logDeriv ζ s = Wtriv s + 1/(s + 2n)
    have hlog : logDeriv riemannZeta s = Wtriv s + 1 / (s + 2 * (n : ℂ)) := by
      have h3 := hWtrivEq s (Metric.mem_ball.mpr hsdist.2) hsne
      rw [hmult, Nat.cast_one] at h3
      have e : s - -2 * (n : ℂ) = s + 2 * (n : ℂ) := by ring
      rw [e] at h3
      linear_combination h3
    show logDeriv riemannZeta s - seriesFun s + 1 / s + 1 / (s - 1)
        - (Real.log Real.pi : ℂ) / 2 + Complex.digamma (s / 2) / 2
      = Wtriv s - seriesFun s + 1 / s + 1 / (s - 1)
        - (Real.log Real.pi : ℂ) / 2 + Hsub n (s / 2) / 2
    rw [hlog, hdig]
    have h1 : -1 / (s / 2 + (n : ℂ)) / 2 = -1 / (s + 2 * (n : ℂ)) := by
      have e : s / 2 + (n : ℂ) = (s + 2 * (n : ℂ)) / 2 := by ring
      rw [e, neg_div, one_div_div]
      ring
    linear_combination h1

/-! ## 7. The witness at a nontrivial zero -/

/-- The witness at a nontrivial zero ρ₀ (mult m): Fexpr agrees punctured
with W₀ − (seriesFun − m/(s−ρ₀)) + 1/s + 1/(s−1) − (log π)/2 + ψ(s/2)/2,
analytic at ρ₀ (the NF witness + 5e-iii's polar subtraction; the
elementary terms analytic since re ρ₀ ∈ (0, 1)). -/
lemma Fexpr_eventually_nontrivial {ρ₀ : ℂ} (hρ : IsNontrivialZero ρ₀) :
    ∃ W : ℂ → ℂ, AnalyticAt ℂ W ρ₀ ∧ ∀ᶠ s in 𝓝[≠] ρ₀, Fexpr s = W s := by
  have hρ1 : ρ₀ ≠ 1 := by
    intro h
    rw [h] at hρ
    have hlt := hρ.2.2
    rw [Complex.one_re] at hlt
    exact lt_irrefl 1 hlt
  obtain ⟨W0, hW0, hW0eq⟩ := logDeriv_zeta_sub_mult_div_eventually hρ.1 hρ1
  have hS : AnalyticAt ℂ (fun s => seriesFun s - (zeroMult ρ₀ : ℂ) / (s - ρ₀)) ρ₀ :=
    seriesFun_sub_polar_analyticAt ⟨ρ₀, hρ⟩
  have hC : AnalyticAt ℂ (fun s : ℂ => 1 / s) ρ₀ := by
    apply AnalyticAt.div analyticAt_const analyticAt_id (by
      have hpos := hρ.2.1
      intro hh
      have hh' : ρ₀ = 0 := hh
      rw [hh', Complex.zero_re] at hpos
      exact lt_irrefl 0 hpos)
  have hC1 : AnalyticAt ℂ (fun s : ℂ => 1 / (s - 1)) ρ₀ := by
    apply AnalyticAt.div analyticAt_const (g := fun s : ℂ => s - 1) _ (sub_ne_zero.mpr hρ1)
    exact analyticAt_id.sub analyticAt_const
  have hD : AnalyticAt ℂ (fun _ : ℂ => (Real.log Real.pi : ℂ) / 2) ρ₀ := analyticAt_const
  have hE : AnalyticAt ℂ (fun s => Complex.digamma (s / 2) / 2) ρ₀ := by
    apply analyticAt_digamma_div_two
    intro m h
    have h2 : ρ₀ = -2 * (m : ℂ) := by linear_combination 2 * h
    have h3 : ρ₀.re = -2 * (m : ℝ) := by rw [h2]; simp
    have h4 : (0 : ℝ) ≤ (m : ℝ) := Nat.cast_nonneg m
    linarith [hρ.2.1]
  refine ⟨fun s => W0 s - (seriesFun s - (zeroMult ρ₀ : ℂ) / (s - ρ₀)) + 1 / s + 1 / (s - 1)
      - (Real.log Real.pi : ℂ) / 2 + Complex.digamma (s / 2) / 2, ?_, ?_⟩
  · exact ((((hW0.sub hS).add hC).add hC1).sub hD).add hE
  · filter_upwards [hW0eq] with s hs
    show logDeriv riemannZeta s - seriesFun s + 1 / s + 1 / (s - 1)
        - (Real.log Real.pi : ℂ) / 2 + Complex.digamma (s / 2) / 2
      = W0 s - (seriesFun s - (zeroMult ρ₀ : ℂ) / (s - ρ₀)) + 1 / s + 1 / (s - 1)
        - (Real.log Real.pi : ℂ) / 2 + Complex.digamma (s / 2) / 2
    linear_combination hs

/-! ## 8. The generic point -/

/-- Fexpr is analytic at every good point: ζ s ≠ 0 (the classification),
s ≠ 0, 1, and s/2 off the digamma poles. -/
lemma Fexpr_analyticAt_of_not_bad {s : ℂ} (hs : ¬ badPoint s) :
    AnalyticAt ℂ Fexpr s := by
  have hs0 : s ≠ 0 := fun h => hs (Or.inr (Or.inl h))
  have hs1 : s ≠ 1 := fun h => hs (Or.inr (Or.inr (Or.inl h)))
  have hζ : riemannZeta s ≠ 0 := by
    intro hz
    apply hs
    rcases zeta_zero_classification hz with h | h | ⟨n, hn, h⟩
    · exact Or.inl h
    · exact Or.inr (Or.inl h)
    · exact Or.inr (Or.inr (Or.inr ⟨n, hn, h⟩))
  have hA : AnalyticAt ℂ (logDeriv riemannZeta) s :=
    ((analyticAt_riemannZeta hs1).deriv).div (analyticAt_riemannZeta hs1) hζ
  have hB : AnalyticAt ℂ seriesFun s := seriesFun_analyticAt (fun h => hs (Or.inl h))
  have hC : AnalyticAt ℂ (fun s : ℂ => 1 / s) s := by
    apply AnalyticAt.div analyticAt_const analyticAt_id hs0
  have hC1 : AnalyticAt ℂ (fun s : ℂ => 1 / (s - 1)) s := by
    apply AnalyticAt.div analyticAt_const (g := fun s : ℂ => s - 1) _ (sub_ne_zero.mpr hs1)
    exact analyticAt_id.sub analyticAt_const
  have hD : AnalyticAt ℂ (fun _ : ℂ => (Real.log Real.pi : ℂ) / 2) s := analyticAt_const
  have hE : AnalyticAt ℂ (fun s => Complex.digamma (s / 2) / 2) s := by
    apply analyticAt_digamma_div_two
    intro m h
    apply hs
    have h2 : s = -2 * (m : ℂ) := by linear_combination 2 * h
    rcases Nat.eq_zero_or_pos m with hm0 | hm
    · subst hm0
      simp at h2
      exact Or.inr (Or.inl h2)
    · exact Or.inr (Or.inr (Or.inr ⟨m, hm, h2⟩))
  show AnalyticAt ℂ (fun s => logDeriv riemannZeta s - seriesFun s + 1 / s + 1 / (s - 1)
      - (Real.log Real.pi : ℂ) / 2 + Complex.digamma (s / 2) / 2) s
  exact ((((hA.sub hB).add hC).add hC1).sub hD).add hE

/-- Around a good point there is a ball of good points (the ζ ≠ 0
continuity ball ∩ avoidance of {0, 1}). -/
lemma exists_ball_good_of_not_bad {s : ℂ} (hs : ¬ badPoint s) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ y ∈ Metric.ball s δ, ¬ badPoint y := by
  have hs0 : s ≠ 0 := fun h => hs (Or.inr (Or.inl h))
  have hs1 : s ≠ 1 := fun h => hs (Or.inr (Or.inr (Or.inl h)))
  have hζ : riemannZeta s ≠ 0 := by
    intro hz
    apply hs
    rcases zeta_zero_classification hz with h | h | ⟨n, hn, h⟩
    · exact Or.inl h
    · exact Or.inr (Or.inl h)
    · exact Or.inr (Or.inr (Or.inr ⟨n, hn, h⟩))
  obtain ⟨ε₁, hε₁, hball₁⟩ := Metric.eventually_nhds_iff_ball.mp
    ((analyticAt_riemannZeta hs1).continuousAt.eventually_ne hζ)
  have hs0n : (0 : ℝ) < ‖s‖ := norm_pos_iff.mpr hs0
  have hs1n : (0 : ℝ) < ‖s - 1‖ := norm_pos_iff.mpr (sub_ne_zero.mpr hs1)
  refine ⟨min ε₁ (min (‖s‖ / 2) (‖s - 1‖ / 2)), lt_min hε₁ (lt_min (half_pos hs0n)
    (half_pos hs1n)), fun y hy => ?_⟩
  have hε₁y : dist y s < ε₁ := lt_of_lt_of_le (Metric.mem_ball.mp hy) (min_le_left _ _)
  have hζy : riemannZeta y ≠ 0 := hball₁ y (Metric.mem_ball.mpr hε₁y)
  have hδs : dist y s < ‖s‖ / 2 :=
    lt_of_lt_of_le (Metric.mem_ball.mp hy) ((min_le_right _ _).trans (min_le_left _ _))
  have hδ1 : dist y s < ‖s - 1‖ / 2 :=
    lt_of_lt_of_le (Metric.mem_ball.mp hy) ((min_le_right _ _).trans (min_le_right _ _))
  have hy0 : y ≠ 0 := by
    intro h
    have h0 : dist (0 : ℂ) s = ‖s‖ := by rw [Complex.dist_eq]; simp
    rw [h, h0] at hδs
    linarith
  have hy1 : y ≠ 1 := by
    intro h
    have h1 : dist (1 : ℂ) s = ‖s - 1‖ := by
      rw [Complex.dist_eq, show (1 : ℂ) - s = -(s - 1) by ring, norm_neg]
    rw [h, h1] at hδ1
    linarith
  rintro (h | h | h | ⟨n, hn, h⟩)
  · exact hζy h.1
  · exact hy0 h
  · exact hy1 h
  · rw [h] at hζy
    exact hζy (riemannZeta_neg_two_mul hn)

/-! ## 9. The entire extension -/

/-- The entire extension of Fexpr: the punctured-limit value. -/
def Gentire : ℂ → ℂ := fun s => limUnder (𝓝[≠] s) Fexpr

/-- At a good point, Gentire = Fexpr (continuity ⟹ the punctured limit
is the value). -/
lemma gentire_eq_Fexpr {s : ℂ} (hs : ¬ badPoint s) : Gentire s = Fexpr s := by
  have hlim : Tendsto Fexpr (𝓝[≠] s) (𝓝 (Fexpr s)) :=
    (Fexpr_analyticAt_of_not_bad hs).continuousAt.mono_left nhdsWithin_le_nhds
  exact tendsto_nhds_unique (tendsto_nhds_limUnder ⟨Fexpr s, hlim⟩) hlim

/-- At a bad point, Gentire agrees on a full neighborhood with the
analytic witness (punctured agreement + the value at the point by the
limUnder uniqueness). -/
lemma gentire_eventually_eq_witness {s : ℂ} (hbad : badPoint s) :
    ∃ W : ℂ → ℂ, AnalyticAt ℂ W s ∧ Gentire =ᶠ[𝓝 s] W := by
  obtain ⟨W, hW, hWeq⟩ : ∃ W, AnalyticAt ℂ W s ∧ ∀ᶠ y in 𝓝[≠] s, Fexpr y = W y := by
    rcases hbad with h | h | h | ⟨n, hn, h⟩
    · exact Fexpr_eventually_nontrivial h
    · subst h; exact Fexpr_eventually_zero
    · subst h; exact Fexpr_eventually_one
    · subst h; exact Fexpr_eventually_neg_two_mul hn
  obtain ⟨δ₂, hδ₂, hgood⟩ : ∃ δ₂ > 0, ∀ y ∈ Metric.ball s δ₂, y ≠ s → ¬ badPoint y := by
    rcases hbad with h | h | h | ⟨n, hn, h⟩
    · -- nontrivial s: isolation ∩ the re ∈ (0, 1) strip
      obtain ⟨δ, hδ, hiso⟩ := nontrivialZero_isolated ⟨s, h⟩
      have hr0 : (0 : ℝ) < s.re := h.2.1
      have hr1 : (0 : ℝ) < 1 - s.re := by linarith [h.2.2]
      refine ⟨min δ (min s.re (1 - s.re)), lt_min hδ (lt_min hr0 hr1), fun y hy hyne hby => ?_⟩
      have hrey : (0 : ℝ) < y.re ∧ y.re < 1 := by
        have hd := Metric.mem_ball.mp hy
        rw [Complex.dist_eq] at hd
        have hre_le : |y.re - s.re| ≤ ‖y - s‖ := by
          have h1 : (y - s).re = y.re - s.re := Complex.sub_re y s
          rw [← h1]
          exact Complex.abs_re_le_norm _
        have hlt : ‖y - s‖ < min s.re (1 - s.re) := lt_of_lt_of_le hd (min_le_right _ _)
        rcases abs_lt.mp (lt_of_le_of_lt hre_le hlt) with ⟨h1, h2⟩
        constructor
        · linarith [hr0, min_le_left s.re (1 - s.re)]
        · linarith [hr1, min_le_right s.re (1 - s.re)]
      rcases hby with hb | hb | hb | ⟨m, hm, hb⟩
      · have hle := hiso ⟨y, hb⟩ (fun heq => hyne (Subtype.ext_iff.mp heq))
        have hd := Metric.mem_ball.mp hy
        rw [Complex.dist_eq] at hd
        linarith [lt_of_lt_of_le hd (min_le_left _ _), hle]
      · rw [hb, Complex.zero_re] at hrey
        exact lt_irrefl 0 hrey.1
      · rw [hb, Complex.one_re] at hrey
        exact lt_irrefl 1 hrey.2
      · have hre : y.re = -2 * (m : ℝ) := by rw [hb]; simp
        have hm1 : (1 : ℝ) ≤ (m : ℝ) := by exact_mod_cast hm
        linarith [hrey.1, hre, hm1]
    · subst h
      -- s = 0: the ζ-continuity ball ∩ ball(0, 1/2)
      have hz0 : ∀ᶠ w in 𝓝 (0 : ℂ), riemannZeta w ≠ 0 :=
        (analyticAt_riemannZeta (by norm_num : (0 : ℂ) ≠ 1)).continuousAt.eventually_ne
          (by rw [riemannZeta_zero]; norm_num)
      obtain ⟨ε₁, hε₁, hball₁⟩ := Metric.eventually_nhds_iff_ball.mp hz0
      refine ⟨min ε₁ (1 / 2), lt_min hε₁ (by norm_num), fun y hy hyne hby => ?_⟩
      have hε₁y : y ∈ Metric.ball 0 ε₁ := Metric.ball_subset_ball (min_le_left _ _) hy
      have hζy : riemannZeta y ≠ 0 := hball₁ y hε₁y
      rcases hby with hb | hb | hb | ⟨m, hm, hb⟩
      · exact hζy hb.1
      · exact hyne hb
      · rw [hb] at hy
        have hd := Metric.mem_ball.mp (Metric.ball_subset_ball (min_le_right _ _) hy)
        rw [Complex.dist_eq] at hd
        norm_num at hd
      · rw [hb] at hζy
        exact hζy (riemannZeta_neg_two_mul hm)
    · subst h
      -- s = 1: the zetaA ball ∩ ball(1, 1/2)
      obtain ⟨ε₁, hε₁, hball₁⟩ := Metric.eventually_nhds_iff_ball.mp zetaA_ne_zero_near_one
      refine ⟨min ε₁ (1 / 2), lt_min hε₁ (by norm_num), fun y hy hyne hby => ?_⟩
      have hε₁y : y ∈ Metric.ball 1 ε₁ := Metric.ball_subset_ball (min_le_left _ _) hy
      have hZA : zetaA y ≠ 0 := hball₁ y hε₁y
      have hζy : riemannZeta y ≠ 0 := by
        have e := zetaA_apply hyne
        intro hz
        rw [hz, mul_zero] at e
        exact hZA e
      rcases hby with hb | hb | hb | ⟨m, hm, hb⟩
      · exact hζy hb.1
      · rw [hb] at hy
        have hd := Metric.mem_ball.mp (Metric.ball_subset_ball (min_le_right _ _) hy)
        rw [Complex.dist_eq] at hd
        norm_num at hd
      · exact hyne hb
      · rw [hb] at hζy
        exact hζy (riemannZeta_neg_two_mul hm)
    · subst h
      -- s = −2n: ball(−2n, 1/2) is bad-point-free off the center
      refine ⟨1 / 2, by norm_num, fun y hy hyne hby => ?_⟩
      rcases hby with hb | hb | hb | ⟨m, hm, hb⟩
      · have hrey : y.re < 0 := by
          have hd := Metric.mem_ball.mp hy
          rw [Complex.dist_eq] at hd
          have hre_le : |y.re - (-2 * (n : ℝ))| ≤ ‖y - -2 * (n : ℂ)‖ := by
            have h1 : (y - -2 * (n : ℂ)).re = y.re - (-2 * (n : ℝ)) := by simp
            rw [← h1]
            exact Complex.abs_re_le_norm _
          have hn1 : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
          rcases abs_lt.mp (lt_of_le_of_lt hre_le hd) with ⟨h1, h2⟩
          linarith
        have hpos := hb.2.1
        linarith
      · have hd := Metric.mem_ball.mp hy
        rw [hb, Complex.dist_eq] at hd
        have hnorm : (2 : ℝ) ≤ ‖(0 : ℂ) - -2 * (n : ℂ)‖ := by
          have h6 : |((0 : ℂ) - -2 * (n : ℂ)).re| ≤ ‖(0 : ℂ) - -2 * (n : ℂ)‖ :=
            Complex.abs_re_le_norm _
          have hre : ((0 : ℂ) - -2 * (n : ℂ)).re = 2 * (n : ℝ) := by simp
          rw [hre] at h6
          have hn1 : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
          rw [abs_of_nonneg (by linarith : (0 : ℝ) ≤ 2 * (n : ℝ))] at h6
          linarith
        linarith [hd, hnorm]
      · have hd := Metric.mem_ball.mp hy
        rw [hb, Complex.dist_eq] at hd
        have hnorm : (2 : ℝ) ≤ ‖(1 : ℂ) - -2 * (n : ℂ)‖ := by
          have h6 : |((1 : ℂ) - -2 * (n : ℂ)).re| ≤ ‖(1 : ℂ) - -2 * (n : ℂ)‖ :=
            Complex.abs_re_le_norm _
          have hre : ((1 : ℂ) - -2 * (n : ℂ)).re = 1 + 2 * (n : ℝ) := by simp
          rw [hre] at h6
          have hn1 : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
          rw [abs_of_nonneg (by linarith : (0 : ℝ) ≤ 1 + 2 * (n : ℝ))] at h6
          linarith
        linarith [hd, hnorm]
      · -- y = −2m ≠ −2n: distance 2|m − n| ≥ 2
        have hd := Metric.mem_ball.mp hy
        rw [hb, Complex.dist_eq] at hd
        have hmn : m ≠ n := by
          intro hmn
          exact hyne (by rw [hb, hmn])
        have hnorm : (2 : ℝ) ≤ ‖(-2 * (m : ℂ)) - -2 * (n : ℂ)‖ := by
          have h6 : |((-2 * (m : ℂ)) - -2 * (n : ℂ)).re| ≤
              ‖(-2 * (m : ℂ)) - -2 * (n : ℂ)‖ := Complex.abs_re_le_norm _
          have hre : ((-2 * (m : ℂ)) - -2 * (n : ℂ)).re = 2 * ((n : ℝ) - (m : ℝ)) := by
            simp
            ring
          rw [hre] at h6
          have hmn' : (1 : ℝ) ≤ |(n : ℝ) - (m : ℝ)| := by
            rcases lt_or_gt_of_ne hmn with hlt | hgt
            · have h7 : (m : ℝ) + 1 ≤ (n : ℝ) := by exact_mod_cast Nat.succ_le_of_lt hlt
              rw [abs_of_nonneg (by linarith)]
              linarith
            · have h7 : (n : ℝ) + 1 ≤ (m : ℝ) := by exact_mod_cast Nat.succ_le_of_lt hgt
              rw [abs_of_nonpos (by linarith)]
              linarith
          have h7 : |2 * ((n : ℝ) - (m : ℝ))| = 2 * |(n : ℝ) - (m : ℝ)| := by
            rw [abs_mul]
            norm_num
          rw [h7] at h6
          linarith [h6, hmn']
        linarith [hd, hnorm]
  -- assemble the full-neighborhood agreement
  have hWeqBall := hWeq
  rw [eventually_nhdsWithin_iff, Metric.eventually_nhds_iff_ball] at hWeqBall
  obtain ⟨ε₁, hε₁, hWeqBall⟩ := hWeqBall
  refine ⟨W, hW, ?_⟩
  show ∀ᶠ y in 𝓝 s, Gentire y = W y
  rw [Metric.eventually_nhds_iff_ball]
  refine ⟨min ε₁ δ₂, lt_min hε₁ hδ₂, fun y hy => ?_⟩
  have hε₁y : y ∈ Metric.ball s ε₁ := Metric.ball_subset_ball (min_le_left _ _) hy
  have hδ₂y : y ∈ Metric.ball s δ₂ := Metric.ball_subset_ball (min_le_right _ _) hy
  by_cases hye : y = s
  · have hWcont : Tendsto W (𝓝[≠] s) (𝓝 (W s)) :=
      hW.continuousAt.mono_left nhdsWithin_le_nhds
    have hWeq' : Fexpr =ᶠ[𝓝[≠] s] W := hWeq
    have hlim : Tendsto Fexpr (𝓝[≠] s) (𝓝 (W s)) := Tendsto.congr' hWeq'.symm hWcont
    have hval : limUnder (𝓝[≠] s) Fexpr = W s :=
      tendsto_nhds_unique (tendsto_nhds_limUnder ⟨W s, hlim⟩) hlim
    rw [hye]
    exact hval
  · have hygood : ¬ badPoint y := hgood y hδ₂y hye
    rw [gentire_eq_Fexpr hygood]
    exact hWeqBall y hε₁y hye

/-- The ii′-5e-iv capstone: Fexpr extends to an entire function agreeing
with it at every good point. -/
theorem gentire_analyticAt_and_eq :
    (∀ s : ℂ, AnalyticAt ℂ Gentire s) ∧ ∀ s : ℂ, ¬ badPoint s → Gentire s = Fexpr s := by
  refine ⟨fun s => ?_, fun s hs => gentire_eq_Fexpr hs⟩
  by_cases hs : badPoint s
  · obtain ⟨W, hW, hWeq⟩ := gentire_eventually_eq_witness hs
    exact hW.congr hWeq.symm
  · obtain ⟨δ, hδ, hgood⟩ := exists_ball_good_of_not_bad hs
    exact (Fexpr_analyticAt_of_not_bad hs).congr (by
      show ∀ᶠ y in 𝓝 s, Fexpr y = Gentire y
      rw [Metric.eventually_nhds_iff_ball]
      exact ⟨δ, hδ, fun y hy => (gentire_eq_Fexpr (hgood y hy)).symm⟩)

end NguyenRH1

end