LiSeries.lean

Declarations

Source

/-
NguyenRH1/LiSeries.lean — tier ii′ sub-stage ii′-5e-iii (D-068 §3):
the zero-side partial-fraction series

  seriesFun s := ∑' ρ : {ρ // IsNontrivialZero ρ}, (zeroMult ρ : ℂ)·(1/(s−ρ) + 1/ρ)

and its three structural properties:

(§1–2) ABSOLUTE SUMMABILITY at every s (`seriesSummable`): the tail bound
  ‖1/(s−ρ) + 1/ρ‖ = ‖s‖/(‖ρ‖·‖s−ρ‖) ≤ 2‖s‖/‖ρ‖² (for 2 ≤ ‖ρ‖, 2‖s‖ ≤ ‖ρ‖)
  feeds the ii′-1a dominator chain (the comparison
  1 + ‖γ_ρ‖² ≤ (17/12)·‖ρ‖² on the tail, then Zeta23
  `WeilEF.zero_sum_inv_sq`); the head is a finite subtype sum
  (`finite_subtype_norm_lt`, the ii′-1a compact-finiteness pattern).

(§3–4) ANALYTICITY off the zeros (`seriesFun_analyticOnNhd`): around any
  s₀ that is not a nontrivial zero there is a ball avoiding the
  nontrivial zeros (`exists_ball_avoid_nontrivialZeros`: continuity of ζ
  where ζ s₀ ≠ 0; the order normal form where ζ s₀ = 0, s₀ ≠ 1; the
  zetaA factorization at s₀ = 1), and on that ball the series converges
  UNIFORMLY (Weierstrass M-test,
  `HasSumUniformlyOn.of_norm_le_summable_eventually`) with analytic
  partial sums — the journal-020/021-banked locally-uniform ⟹ analytic
  pattern.

(§5) ISOLATION (`nontrivialZero_isolated`: minimum-distance over the
  finite ball) and the reduced series `seriesFunSub ρ₀` (the ρ₀-term
  zeroed out): analytic AT ρ₀ (`seriesFunSub_analyticAt`), so both the
  term subtraction s ↦ seriesFun s − seriesTerm s ρ₀ and the polar
  subtraction s ↦ seriesFun s − mult(ρ₀)/(s−ρ₀) are analytic at ρ₀
  (`seriesFun_sub_self_term_analyticAt`,
  `seriesFun_sub_polar_analyticAt`) — the inputs 5e-iv needs for the
  residue cancellation at the nontrivial zeros.

Archive references: D-068 §3, journal-015 (ii′-1a dominator chain),
journal-020/021 (Weierstrass-convergence pattern), journal-024 (the
compact-finiteness ball pattern).
-/
import Mathlib
import Zeta23.Statement
import Zeta23.WeilEF.ZeroSummability
import Zeta23.Statement.SeamClosed
import NguyenRH1.LiSides

open Zeta23 Complex Filter Topology

noncomputable section

namespace NguyenRH1

/-! ## 0. The series -/

/-- The zero-series summand: mult(ρ)·(1/(s−ρ) + 1/ρ) over the nontrivial
zero subtype (the ii′-1a encoding; D-068 §3). -/
def seriesTerm (s : ℂ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ :=
  (zeroMult ρ : ℂ) * (1 / (s - (ρ : ℂ)) + 1 / (ρ : ℂ))

/-- The zero-side partial-fraction series. Summable at every s
(`seriesSummable`), analytic off the nontrivial zeros
(`seriesFun_analyticOnNhd`). -/
def seriesFun (s : ℂ) : ℂ := ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, seriesTerm s ρ

/-! ## 1. The norm comparison and the tail bound -/

/-- For a nontrivial zero with 2 ≤ ‖ρ‖: 1 + ‖γ_ρ‖² ≤ (17/12)·‖ρ‖².
On re ρ ∈ (0, 1): ‖γ‖² = im² + (1/2−re)² ≤ im² + 1/4, and
im² = ‖ρ‖² − re² ≥ 4 − 1 = 3 gives 5/4 ≤ (5/12)·im². -/
lemma one_add_normSq_gammaOf_le (ρ : {ρ : ℂ // IsNontrivialZero ρ})
    (hρ : (2 : ℝ) ≤ ‖(ρ : ℂ)‖) :
    1 + Complex.normSq (gammaOf (ρ : ℂ)) ≤ 17 / 12 * ‖(ρ : ℂ)‖ ^ 2 := by
  have hz := ρ.2
  have hre0 : 0 < (ρ : ℂ).re := hz.2.1
  have hre1 : (ρ : ℂ).re < 1 := hz.2.2
  have hnorm : ‖(ρ : ℂ)‖ ^ 2 = (ρ : ℂ).re ^ 2 + (ρ : ℂ).im ^ 2 := by
    rw [← Complex.normSq_eq_norm_sq, Complex.normSq_apply]
    ring
  have hgam : Complex.normSq (gammaOf (ρ : ℂ))
      = (ρ : ℂ).im ^ 2 + (1 / 2 - (ρ : ℂ).re) ^ 2 := by
    rw [Complex.normSq_apply, WeilEF.gammaOf_re, WeilEF.gammaOf_im]
    ring
  have hρsq : 4 ≤ ‖(ρ : ℂ)‖ ^ 2 := by nlinarith [hρ, norm_nonneg (ρ : ℂ)]
  have hre2 : (ρ : ℂ).re ^ 2 ≤ 1 := by nlinarith [hre0, hre1]
  have him2 : 3 ≤ (ρ : ℂ).im ^ 2 := by nlinarith [hρsq, hre2]
  have hquarter : (1 / 2 - (ρ : ℂ).re) ^ 2 ≤ 1 / 4 := by nlinarith [hre0, hre1]
  rw [hgam, hnorm]
  nlinarith [him2, hquarter, sq_nonneg (ρ : ℂ).re]

/-- The key algebra: 1/(s−ρ) + 1/ρ = s/(ρ·(s−ρ)). -/
lemma one_div_sub_add_one_div {s ρ : ℂ} (h0 : ρ ≠ 0) (h1 : s - ρ ≠ 0) :
    1 / (s - ρ) + 1 / ρ = s / (ρ * (s - ρ)) := by
  have h2 : ρ * (s - ρ) ≠ 0 := mul_ne_zero h0 h1
  field_simp
  ring

/-- Tail bound: for 2 ≤ ‖ρ‖ and 2‖s‖ ≤ ‖ρ‖,
‖seriesTerm s ρ‖ ≤ (17/6)·‖s‖·mult/(1+‖γ_ρ‖²). -/
lemma seriesTerm_norm_le {s : ℂ} (ρ : {ρ : ℂ // IsNontrivialZero ρ})
    (hρ2 : (2 : ℝ) ≤ ‖(ρ : ℂ)‖) (hsρ : 2 * ‖s‖ ≤ ‖(ρ : ℂ)‖) :
    ‖seriesTerm s ρ‖ ≤
      17 / 6 * ‖s‖ * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ)))) := by
  have h0 : (ρ : ℂ) ≠ 0 := by
    intro h; rw [h, norm_zero] at hρ2; norm_num at hρ2
  have hρpos : (0 : ℝ) < ‖(ρ : ℂ)‖ := norm_pos_iff.mpr h0
  have hsr : ‖(ρ : ℂ)‖ / 2 ≤ ‖s - (ρ : ℂ)‖ := by
    have h := abs_norm_sub_norm_le s (ρ : ℂ)
    rw [abs_le] at h
    linarith [h.1]
  have h1 : s - (ρ : ℂ) ≠ 0 := by
    intro h; rw [h, norm_zero] at hsr; linarith
  have hcomp := one_add_normSq_gammaOf_le ρ hρ2
  have hg0 : (0 : ℝ) < 1 + Complex.normSq (gammaOf (ρ : ℂ)) := by
    have h := Complex.normSq_nonneg (gammaOf (ρ : ℂ)); linarith
  have halg := one_div_sub_add_one_div h0 h1
  have hden : ‖(ρ : ℂ)‖ ^ 2 / 2 ≤ ‖(ρ : ℂ)‖ * ‖s - (ρ : ℂ)‖ := by
    nlinarith [mul_le_mul_of_nonneg_left hsr hρpos.le]
  have hden0 : (0 : ℝ) < ‖(ρ : ℂ)‖ * ‖s - (ρ : ℂ)‖ :=
    mul_pos hρpos (by linarith [hsr, hρpos])
  have hρsq0 : (0 : ℝ) < ‖(ρ : ℂ)‖ ^ 2 := pow_pos hρpos 2
  have hfrac : ‖s‖ / (‖(ρ : ℂ)‖ * ‖s - (ρ : ℂ)‖) ≤ 2 * ‖s‖ / ‖(ρ : ℂ)‖ ^ 2 := by
    rw [div_le_div_iff₀ hden0 hρsq0]
    nlinarith [hden, norm_nonneg s, hρpos]
  have hmul0 : (0 : ℝ) ≤ (zeroMult ρ : ℝ) := Nat.cast_nonneg _
  simp only [seriesTerm]
  rw [halg, norm_mul, RCLike.norm_natCast, norm_div, norm_mul]
  calc (zeroMult ρ : ℝ) * (‖s‖ / (‖(ρ : ℂ)‖ * ‖s - (ρ : ℂ)‖))
      ≤ (zeroMult ρ : ℝ) * (2 * ‖s‖ / ‖(ρ : ℂ)‖ ^ 2) :=
        mul_le_mul_of_nonneg_left hfrac hmul0
    _ = 2 * ‖s‖ * (zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ 2 := by ring
    _ ≤ 17 / 6 * ‖s‖ * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ)))) := by
        have hR : 17 / 6 * ‖s‖ * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ))))
            = (17 / 6 * ‖s‖ * (zeroMult ρ : ℝ)) / (1 + Complex.normSq (gammaOf (ρ : ℂ))) := by
          ring
        rw [hR, div_le_div_iff₀ hρsq0 hg0]
        have hkey : 2 * (1 + Complex.normSq (gammaOf (ρ : ℂ)))
            ≤ 17 / 6 * ‖(ρ : ℂ)‖ ^ 2 := by linarith [hcomp]
        calc 2 * ‖s‖ * (zeroMult ρ : ℝ) * (1 + Complex.normSq (gammaOf (ρ : ℂ)))
            = (‖s‖ * (zeroMult ρ : ℝ)) * (2 * (1 + Complex.normSq (gammaOf (ρ : ℂ)))) := by
              ring
          _ ≤ (‖s‖ * (zeroMult ρ : ℝ)) * (17 / 6 * ‖(ρ : ℂ)‖ ^ 2) :=
              mul_le_mul_of_nonneg_left hkey (by positivity)
          _ = 17 / 6 * ‖s‖ * (zeroMult ρ : ℝ) * ‖(ρ : ℂ)‖ ^ 2 := by ring

/-! ## 2. Summability -/

/-- The subtype elements in a closed ball form a finite set (the ii′-1a
compact-finiteness pattern: nontrivial zeros ⊆ `riemannZetaZeros`,
finite in compacts by Mathlib's discreteness of the zero set). -/
lemma finite_subtype_norm_lt (R : ℝ) :
    {ρ : {ρ : ℂ // IsNontrivialZero ρ} | ‖(ρ : ℂ)‖ < R}.Finite := by
  have hcomp : IsCompact (Metric.closedBall (0 : ℂ) R) := isCompact_closedBall _ _
  have hzeros : (Metric.closedBall (0 : ℂ) R) ∩ {ρ : ℂ | IsNontrivialZero ρ}
      ⊆ (Metric.closedBall (0 : ℂ) R) ∩ riemannZetaZeros := by
    intro z hz
    exact ⟨hz.1, hz.2.1⟩
  have hfin2 := (hcomp.inter_riemannZetaZeros_finite).subset hzeros
  have himg : (Subtype.val '' {ρ : {ρ // IsNontrivialZero ρ} | ‖(ρ : ℂ)‖ < R}).Finite := by
    apply hfin2.subset
    rintro z ⟨ρ, hρ, rfl⟩
    refine ⟨?_, ρ.2⟩
    simp only [Metric.mem_closedBall, dist_zero_right]
    exact le_of_lt hρ
  exact Set.Finite.of_finite_image himg (Subtype.val_injective.injOn)

/-- The M-test majorant family, summable by Zeta23's `zero_sum_inv_sq`. -/
lemma seriesTerm_summable_majorant (M : ℝ) :
    Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>
      17 / 6 * M * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ))))) :=
  (WeilEF.zero_sum_inv_sq zetaSeam).mul_left _

/-- The series is absolutely summable at every s (the ii′-1a D-trick:
dominator (17/6)(‖s‖+1)·mult/(1+‖γ‖²) on the tail ‖ρ‖ ≥ max 2 (2‖s‖),
finite head by `finite_subtype_norm_lt`). -/
theorem seriesSummable (s : ℂ) :
    Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => seriesTerm s ρ) := by
  set R₀ : ℝ := max 2 (2 * ‖s‖) with hR₀
  have hR₀2 : (2 : ℝ) ≤ R₀ := le_max_left _ _
  have hR₀s : 2 * ‖s‖ ≤ R₀ := le_max_right _ _
  set C : ℝ := 17 / 6 * (‖s‖ + 1) with hC
  have hbase : Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>
      C * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ))))) :=
    (WeilEF.zero_sum_inv_sq zetaSeam).mul_left C
  set D : {ρ : ℂ // IsNontrivialZero ρ} → ℝ := fun ρ =>
    if R₀ ≤ ‖(ρ : ℂ)‖ then
      C * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ))))
    else ‖seriesTerm s ρ‖ with hDdef
  have hfin : {ρ : {ρ // IsNontrivialZero ρ} | ¬ (R₀ ≤ ‖(ρ : ℂ)‖)}.Finite := by
    apply (finite_subtype_norm_lt R₀).subset
    intro ρ hρ
    exact not_le.mp hρ
  have hE : Summable (fun ρ : {ρ // IsNontrivialZero ρ} =>
      D ρ - C * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ))))) := by
    apply summable_of_hasFiniteSupport
    apply hfin.subset
    intro ρ hρ
    simp only [Function.mem_support, ne_eq] at hρ
    by_contra hball
    apply hρ
    have hball' : R₀ ≤ ‖(ρ : ℂ)‖ := not_not.mp hball
    simp only [D, if_pos hball']
    ring
  have hD : Summable D := by
    have hsum := hbase.add hE
    have heq : (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>
        C * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ)))) +
          (D ρ - C * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ)))))) = D := by
      funext ρ
      ring
    rw [heq] at hsum
    exact hsum
  refine Summable.of_norm_bounded hD (fun ρ => ?_)
  by_cases hρ : R₀ ≤ ‖(ρ : ℂ)‖
  · simp only [D, if_pos hρ]
    have h2 : (2 : ℝ) ≤ ‖(ρ : ℂ)‖ := hR₀2.trans hρ
    have hs2 : 2 * ‖s‖ ≤ ‖(ρ : ℂ)‖ := hR₀s.trans hρ
    have h := seriesTerm_norm_le ρ h2 hs2
    apply h.trans
    have hg0 : (0 : ℝ) ≤ (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ))) := by
      have hnn := Complex.normSq_nonneg (gammaOf (ρ : ℂ))
      positivity
    have hC' : 17 / 6 * ‖s‖ ≤ C := by
      rw [hC]
      nlinarith [norm_nonneg s]
    exact mul_le_mul_of_nonneg_right hC' hg0
  · simp only [D, if_neg hρ, le_refl]

/-! ## 3. Balls avoiding the nontrivial zeros -/

/-- Around any point that is not a nontrivial zero there is a ball
containing no nontrivial zero: continuity of ζ where ζ s₀ ≠ 0; the order
normal form (zeros isolated among ζ-zeros) where ζ s₀ = 0, s₀ ≠ 1; the
zetaA factorization (pole neighbourhood) at s₀ = 1. -/
lemma exists_ball_avoid_nontrivialZeros (s₀ : ℂ) (hs₀ : ¬ IsNontrivialZero s₀) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ ρ : {ρ : ℂ // IsNontrivialZero ρ}, (ρ : ℂ) ∉ Metric.ball s₀ δ := by
  by_cases h1 : s₀ = 1
  · subst h1
    obtain ⟨ε, hε, hball⟩ := Metric.eventually_nhds_iff_ball.mp zetaA_ne_zero_near_one
    refine ⟨ε, hε, fun ρ hρ => ?_⟩
    have hρ1 : (ρ : ℂ) ≠ 1 := by
      intro h
      have hlt : (ρ : ℂ).re < 1 := ρ.2.2.2
      rw [h, Complex.one_re] at hlt
      exact lt_irrefl 1 hlt
    have hz := hball (ρ : ℂ) hρ
    rw [zetaA_apply hρ1, ρ.2.1, mul_zero] at hz
    exact hz rfl
  · by_cases h0 : riemannZeta s₀ = 0
    · obtain ⟨h, hh, hh0, hfh⟩ :=
        (analyticAt_riemannZeta h1).analyticOrderAt_ne_top.mp (zeta_order_ne_top_of_ne h1)
      obtain ⟨ε₁, hε₁, hball₁⟩ := Metric.eventually_nhds_iff_ball.mp
        (hh.continuousAt.eventually_ne hh0)
      obtain ⟨ε₂, hε₂, hball₂⟩ := Metric.eventually_nhds_iff_ball.mp hfh
      refine ⟨min ε₁ ε₂, lt_min hε₁ hε₂, fun ρ hρ => ?_⟩
      have hmem1 : (ρ : ℂ) ∈ Metric.ball s₀ ε₁ := Metric.ball_subset_ball (min_le_left _ _) hρ
      have hmem2 : (ρ : ℂ) ∈ Metric.ball s₀ ε₂ := Metric.ball_subset_ball (min_le_right _ _) hρ
      have heq := hball₂ (ρ : ℂ) hmem2
      have hne : h (ρ : ℂ) ≠ 0 := hball₁ (ρ : ℂ) hmem1
      by_cases hρs : (ρ : ℂ) = s₀
      · exact hs₀ (hρs ▸ ρ.2)
      · have hpow : ((ρ : ℂ) - s₀) ^ analyticOrderNatAt riemannZeta s₀ ≠ 0 :=
          pow_ne_zero _ (sub_ne_zero.mpr hρs)
        have hz : riemannZeta (ρ : ℂ) ≠ 0 := by
          rw [heq]
          show (↑ρ - s₀) ^ analyticOrderNatAt riemannZeta s₀ * h (ρ : ℂ) ≠ 0
          exact mul_ne_zero hpow hne
        exact hz ρ.2.1
    · obtain ⟨ε, hε, hball⟩ := Metric.eventually_nhds_iff_ball.mp
        ((analyticAt_riemannZeta h1).continuousAt.eventually_ne h0)
      refine ⟨ε, hε, fun ρ hρ => ?_⟩
      exact hball (ρ : ℂ) hρ ρ.2.1

/-! ## 4. Analyticity off the zeros -/

/-- The series is analytic at every point that is not a nontrivial zero
(Weierstrass M-test on an avoiding ball; the journal-020/021 pattern). -/
theorem seriesFun_analyticAt {s₀ : ℂ} (hs₀ : ¬ IsNontrivialZero s₀) :
    AnalyticAt ℂ seriesFun s₀ := by
  obtain ⟨δ, hδ, hball⟩ := exists_ball_avoid_nontrivialZeros s₀ hs₀
  set M : ℝ := ‖s₀‖ + δ with hM
  have hM0 : (0 : ℝ) ≤ M := by rw [hM]; linarith [norm_nonneg s₀, hδ.le]
  set R₀ : ℝ := max 2 (2 * M) with hR₀
  set u : {ρ : ℂ // IsNontrivialZero ρ} → ℝ := fun ρ =>
    17 / 6 * M * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ)))) with hu
  have hsum_u : Summable u := seriesTerm_summable_majorant M
  have hfu : ∀ᶠ ρ in cofinite, ∀ s ∈ Metric.ball s₀ δ, ‖seriesTerm s ρ‖ ≤ u ρ := by
    rw [eventually_cofinite]
    apply (finite_subtype_norm_lt R₀).subset
    intro ρ hρ
    show ‖(ρ : ℂ)‖ < R₀
    by_contra hlt
    rw [not_lt] at hlt
    apply hρ
    intro s hs
    have hsM : ‖s‖ ≤ M := by
      have hlt2 : ‖s‖ < M := by
        calc ‖s‖ ≤ ‖s - s₀‖ + ‖s₀‖ := by
                nth_rewrite 1 [show s = (s - s₀) + s₀ from by ring]
                exact norm_add_le _ _
          _ < δ + ‖s₀‖ := by
                have hmem := Metric.mem_ball.mp hs
                rw [dist_eq_norm] at hmem
                linarith
          _ = M := by rw [hM]; ring
      exact le_of_lt hlt2
    have h2 : (2 : ℝ) ≤ ‖(ρ : ℂ)‖ := (le_max_left _ _).trans hlt
    have hs2 : 2 * ‖s‖ ≤ ‖(ρ : ℂ)‖ := by
      have h2M : 2 * ‖s‖ ≤ 2 * M := by linarith
      exact (h2M.trans (le_max_right _ _)).trans hlt
    have h := seriesTerm_norm_le ρ h2 hs2
    apply h.trans
    have hg0 : (0 : ℝ) ≤ (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ))) := by
      have hnn := Complex.normSq_nonneg (gammaOf (ρ : ℂ))
      positivity
    have hle : 17 / 6 * ‖s‖ ≤ 17 / 6 * M := by nlinarith [hsM, hM0, norm_nonneg s]
    exact mul_le_mul_of_nonneg_right hle hg0
  have hu' : HasSumUniformlyOn (fun ρ => fun s : ℂ => seriesTerm s ρ)
      (fun s => ∑' ρ, seriesTerm s ρ) (Metric.ball s₀ δ) :=
    HasSumUniformlyOn.of_norm_le_summable_eventually hsum_u hfu
  have htend : TendstoLocallyUniformlyOn
      (fun t : Finset {ρ : ℂ // IsNontrivialZero ρ} => fun s => ∑ ρ ∈ t, seriesTerm s ρ)
      (fun s => ∑' ρ, seriesTerm s ρ) atTop (Metric.ball s₀ δ) :=
    TendstoUniformlyOn.tendstoLocallyUniformlyOn
      (hasSumUniformlyOn_iff_tendstoUniformlyOn.mp hu')
  have hdiff : DifferentiableOn ℂ (fun s => ∑' ρ, seriesTerm s ρ)
      (Metric.ball s₀ δ) := by
    apply htend.differentiableOn _ Metric.isOpen_ball
    apply Filter.Eventually.of_forall
    intro t s hs
    rw [show (fun s => ∑ ρ ∈ t, seriesTerm s ρ) = ∑ ρ ∈ t, (fun s => seriesTerm s ρ) from by
      funext s; simp [Finset.sum_apply]]
    apply DifferentiableAt.differentiableWithinAt
    apply DifferentiableAt.sum
    intro ρ hρt
    have hsρ : s - (ρ : ℂ) ≠ 0 := by
      have hρout : (ρ : ℂ) ∉ Metric.ball s₀ δ := hball ρ
      intro h
      apply hρout
      have heq : (ρ : ℂ) = s := (sub_eq_zero.mp h).symm
      rw [heq]
      exact hs
    have hρ0 : (ρ : ℂ) ≠ 0 := by
      intro h
      have hlt := ρ.2.2.1
      rw [h] at hlt
      simp at hlt
    have h1 : DifferentiableAt ℂ (fun s : ℂ => 1 / (s - (ρ : ℂ))) s :=
      (differentiableAt_const (1 : ℂ)).div
        (differentiableAt_id.sub (differentiableAt_const _)) hsρ
    have h2 : DifferentiableAt ℂ (fun s : ℂ => 1 / (ρ : ℂ)) s := differentiableAt_const _
    show DifferentiableAt ℂ (fun s => (zeroMult ρ : ℂ) * (1 / (s - (ρ : ℂ)) + 1 / (ρ : ℂ))) s
    exact (h1.add h2).const_mul _
  have han : AnalyticOnNhd ℂ (fun s => ∑' ρ, seriesTerm s ρ) (Metric.ball s₀ δ) :=
    hdiff.analyticOnNhd Metric.isOpen_ball
  exact han s₀ (Metric.mem_ball_self hδ)

/-- The series is analytic on the complement of the nontrivial zeros. -/
theorem seriesFun_analyticOnNhd :
    AnalyticOnNhd ℂ seriesFun {s : ℂ | ¬ IsNontrivialZero s} :=
  fun _s₀ hs₀ => seriesFun_analyticAt hs₀

/-! ## 5. Isolation and the reduced series -/

/-- Each nontrivial zero is isolated from the others (finiteness of the
zero set in the unit ball + minimum distance). -/
theorem nontrivialZero_isolated (ρ₀ : {ρ : ℂ // IsNontrivialZero ρ}) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ ρ₁ : {ρ : ℂ // IsNontrivialZero ρ}, ρ₁ ≠ ρ₀ →
      δ ≤ ‖(ρ₁ : ℂ) - (ρ₀ : ℂ)‖ := by
  have hcomp : IsCompact (Metric.closedBall (ρ₀ : ℂ) 1) := isCompact_closedBall _ _
  have hzeros : (Metric.closedBall (ρ₀ : ℂ) 1) ∩ {ρ : ℂ | IsNontrivialZero ρ}
      ⊆ (Metric.closedBall (ρ₀ : ℂ) 1) ∩ riemannZetaZeros := by
    intro z hz
    exact ⟨hz.1, hz.2.1⟩
  have hfin : ((Metric.closedBall (ρ₀ : ℂ) 1) ∩ {ρ : ℂ | IsNontrivialZero ρ}).Finite :=
    (hcomp.inter_riemannZetaZeros_finite).subset hzeros
  set S : Set {ρ : ℂ // IsNontrivialZero ρ} :=
    {ρ | (ρ : ℂ) ∈ Metric.closedBall (ρ₀ : ℂ) 1 ∧ ρ ≠ ρ₀} with hS
  have hSfin : S.Finite := by
    have himg : (Subtype.val '' S).Finite := by
      apply hfin.subset
      rintro z ⟨ρ, ⟨hρ, -⟩, rfl⟩
      exact ⟨hρ, ρ.2⟩
    exact Set.Finite.of_finite_image himg (Subtype.val_injective.injOn)
  by_cases hne : S.Nonempty
  · set d : Finset ℝ := hSfin.toFinset.image
        (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => ‖(ρ : ℂ) - (ρ₀ : ℂ)‖) with hd
    have hdm : ∀ x : ℝ, x ∈ d ↔
        ∃ ρ : {ρ : ℂ // IsNontrivialZero ρ}, ρ ∈ S ∧ ‖(ρ : ℂ) - (ρ₀ : ℂ)‖ = x := by
      intro x
      rw [hd]
      simp only [Finset.mem_image, Set.Finite.mem_toFinset]
    have hdne : d.Nonempty := by
      obtain ⟨ρ, hρ⟩ := hne
      exact ⟨‖(ρ : ℂ) - (ρ₀ : ℂ)‖, (hdm _).mpr ⟨ρ, hρ, rfl⟩⟩
    have hdpos : ∀ x ∈ d, 0 < x := by
      intro x hx
      obtain ⟨ρ, hρ, rfl⟩ := (hdm x).mp hx
      have h1 : (ρ : ℂ) ≠ (ρ₀ : ℂ) := fun h => hρ.2 (Subtype.ext h)
      exact norm_pos_iff.mpr (sub_ne_zero.mpr h1)
    have hmin0 : 0 < d.min' hdne := hdpos _ (Finset.min'_mem _ _)
    have hmin1 : d.min' hdne ≤ 1 := by
      obtain ⟨ρ, hρ, heq⟩ := (hdm _).mp (Finset.min'_mem d hdne)
      rw [← heq]
      have hρ1 := hρ.1
      rw [Metric.mem_closedBall, dist_eq_norm] at hρ1
      exact hρ1
    refine ⟨d.min' hdne / 2, half_pos hmin0, fun ρ₁ hρ₁ => ?_⟩
    by_cases hmem : (ρ₁ : ℂ) ∈ Metric.closedBall (ρ₀ : ℂ) 1
    · have h1 : ρ₁ ∈ S := ⟨hmem, hρ₁⟩
      have h2 : ‖(ρ₁ : ℂ) - (ρ₀ : ℂ)‖ ∈ d := (hdm _).mpr ⟨ρ₁, h1, rfl⟩
      have h3 : d.min' hdne ≤ ‖(ρ₁ : ℂ) - (ρ₀ : ℂ)‖ := Finset.min'_le _ _ h2
      linarith
    · have h4 : 1 ≤ ‖(ρ₁ : ℂ) - (ρ₀ : ℂ)‖ := by
        by_contra h
        apply hmem
        rw [Metric.mem_closedBall, dist_eq_norm]
        exact le_of_lt (not_le.mp h)
      linarith
  · refine ⟨1 / 2, by norm_num, fun ρ₁ hρ₁ => ?_⟩
    by_contra h
    rw [not_le] at h
    apply hne
    exact ⟨ρ₁, ⟨by
      rw [Metric.mem_closedBall, dist_eq_norm]
      linarith, hρ₁⟩⟩

/-- The reduced summand: the ρ₀-term zeroed out. -/
def seriesTermSub (ρ₀ : {ρ : ℂ // IsNontrivialZero ρ}) (s : ℂ)
    (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ :=
  if ρ = ρ₀ then 0 else seriesTerm s ρ

/-- The reduced series (the ρ₀ polar term removed): analytic AT ρ₀
(`seriesFunSub_analyticAt`). -/
def seriesFunSub (ρ₀ : {ρ : ℂ // IsNontrivialZero ρ}) (s : ℂ) : ℂ :=
  ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, seriesTermSub ρ₀ s ρ

lemma seriesTermSub_norm_le (ρ₀ : {ρ : ℂ // IsNontrivialZero ρ}) (s : ℂ)
    (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ‖seriesTermSub ρ₀ s ρ‖ ≤ ‖seriesTerm s ρ‖ := by
  by_cases h : ρ = ρ₀ <;> simp [seriesTermSub, h]

theorem seriesTermSub_summable (ρ₀ : {ρ : ℂ // IsNontrivialZero ρ}) (s : ℂ) :
    Summable (seriesTermSub ρ₀ s) :=
  Summable.of_norm_bounded (seriesSummable s).norm (fun ρ => seriesTermSub_norm_le ρ₀ s ρ)

lemma single_summable (ρ₀ : {ρ : ℂ // IsNontrivialZero ρ}) (s : ℂ) :
    Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>
      if ρ = ρ₀ then seriesTerm s ρ else (0 : ℂ)) := by
  apply summable_of_hasFiniteSupport ((Set.finite_singleton ρ₀).subset ?_)
  intro ρ hρ
  rw [Function.mem_support, ne_eq] at hρ
  by_contra h
  apply hρ
  rw [if_neg (fun he => h (Set.mem_singleton_iff.mpr he))]

/-- Pointwise split: seriesFun = seriesFunSub + the ρ₀-term (everywhere). -/
lemma seriesFun_eq_sub_add (ρ₀ : {ρ : ℂ // IsNontrivialZero ρ}) (s : ℂ) :
    seriesFun s = seriesFunSub ρ₀ s + seriesTerm s ρ₀ := by
  have hsingle : ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},
      (if ρ = ρ₀ then seriesTerm s ρ else (0 : ℂ)) = seriesTerm s ρ₀ := by
    rw [tsum_eq_single ρ₀ (fun ρ hρ => if_neg hρ)]
    exact if_pos rfl
  calc seriesFun s = ∑' ρ, seriesTerm s ρ := rfl
    _ = ∑' ρ, (seriesTermSub ρ₀ s ρ + (if ρ = ρ₀ then seriesTerm s ρ else (0 : ℂ))) := by
        apply tsum_congr
        intro ρ
        by_cases h : ρ = ρ₀ <;> simp [seriesTermSub, h]
    _ = ∑' ρ, seriesTermSub ρ₀ s ρ + ∑' ρ, (if ρ = ρ₀ then seriesTerm s ρ else (0 : ℂ)) :=
        Summable.tsum_add (seriesTermSub_summable ρ₀ s) (single_summable ρ₀ s)
    _ = seriesFunSub ρ₀ s + seriesTerm s ρ₀ := by rw [hsingle]; rfl

/-- The series minus its ρ₀-term equals the reduced series (everywhere). -/
theorem seriesFun_sub_term (ρ₀ : {ρ : ℂ // IsNontrivialZero ρ}) (s : ℂ) :
    seriesFun s - seriesTerm s ρ₀ = seriesFunSub ρ₀ s := by
  have h := seriesFun_eq_sub_add ρ₀ s
  rw [h]
  ring

/-- The reduced series is analytic at ρ₀ (the other terms have no pole
in the isolation ball; Weierstrass M-test as in §4). -/
theorem seriesFunSub_analyticAt (ρ₀ : {ρ : ℂ // IsNontrivialZero ρ}) :
    AnalyticAt ℂ (seriesFunSub ρ₀) (ρ₀ : ℂ) := by
  obtain ⟨δ, hδ, hiso⟩ := nontrivialZero_isolated ρ₀
  set δ' : ℝ := δ / 2 with hδ'
  have hδ'0 : 0 < δ' := half_pos hδ
  set M : ℝ := ‖(ρ₀ : ℂ)‖ + δ' with hM
  have hM0 : (0 : ℝ) ≤ M := by rw [hM]; linarith [norm_nonneg (ρ₀ : ℂ), hδ'0.le]
  set R₀ : ℝ := max 2 (2 * M) with hR₀
  set u : {ρ : ℂ // IsNontrivialZero ρ} → ℝ := fun ρ =>
    17 / 6 * M * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ)))) with hu
  have hsum_u : Summable u := seriesTerm_summable_majorant M
  have hfu : ∀ᶠ ρ in cofinite, ∀ s ∈ Metric.ball (ρ₀ : ℂ) δ',
      ‖seriesTermSub ρ₀ s ρ‖ ≤ u ρ := by
    rw [eventually_cofinite]
    apply (finite_subtype_norm_lt R₀).subset
    intro ρ hρ
    show ‖(ρ : ℂ)‖ < R₀
    by_contra hlt
    rw [not_lt] at hlt
    apply hρ
    intro s hs
    have hsM : ‖s‖ ≤ M := by
      have hlt2 : ‖s‖ < M := by
        calc ‖s‖ ≤ ‖s - (ρ₀ : ℂ)‖ + ‖(ρ₀ : ℂ)‖ := by
                nth_rewrite 1 [show s = (s - (ρ₀ : ℂ)) + (ρ₀ : ℂ) from by ring]
                exact norm_add_le _ _
          _ < δ' + ‖(ρ₀ : ℂ)‖ := by
                have hmem := Metric.mem_ball.mp hs
                rw [dist_eq_norm] at hmem
                linarith
          _ = M := by rw [hM]; ring
      exact le_of_lt hlt2
    by_cases h0 : ρ = ρ₀
    · rw [seriesTermSub, if_pos h0, norm_zero]
      have hg0 : (0 : ℝ) ≤ (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ))) := by
        have hnn := Complex.normSq_nonneg (gammaOf (ρ : ℂ))
        positivity
      exact mul_nonneg (mul_nonneg (by norm_num) hM0) hg0
    · have h2 : (2 : ℝ) ≤ ‖(ρ : ℂ)‖ := (le_max_left _ _).trans hlt
      have hs2 : 2 * ‖s‖ ≤ ‖(ρ : ℂ)‖ := by
        have h2M : 2 * ‖s‖ ≤ 2 * M := by linarith
        exact (h2M.trans (le_max_right _ _)).trans hlt
      rw [seriesTermSub, if_neg h0]
      have h := seriesTerm_norm_le ρ h2 hs2
      apply h.trans
      have hg0 : (0 : ℝ) ≤ (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ))) := by
        have hnn := Complex.normSq_nonneg (gammaOf (ρ : ℂ))
        positivity
      have hle : 17 / 6 * ‖s‖ ≤ 17 / 6 * M := by nlinarith [hsM, hM0, norm_nonneg s]
      exact mul_le_mul_of_nonneg_right hle hg0
  have hu' : HasSumUniformlyOn (fun ρ => fun s : ℂ => seriesTermSub ρ₀ s ρ)
      (fun s => ∑' ρ, seriesTermSub ρ₀ s ρ) (Metric.ball (ρ₀ : ℂ) δ') :=
    HasSumUniformlyOn.of_norm_le_summable_eventually hsum_u hfu
  have htend : TendstoLocallyUniformlyOn
      (fun t : Finset {ρ : ℂ // IsNontrivialZero ρ} => fun s => ∑ ρ ∈ t, seriesTermSub ρ₀ s ρ)
      (fun s => ∑' ρ, seriesTermSub ρ₀ s ρ) atTop (Metric.ball (ρ₀ : ℂ) δ') :=
    TendstoUniformlyOn.tendstoLocallyUniformlyOn
      (hasSumUniformlyOn_iff_tendstoUniformlyOn.mp hu')
  have hdiff : DifferentiableOn ℂ (fun s => ∑' ρ, seriesTermSub ρ₀ s ρ)
      (Metric.ball (ρ₀ : ℂ) δ') := by
    apply htend.differentiableOn _ Metric.isOpen_ball
    apply Filter.Eventually.of_forall
    intro t s hs
    rw [show (fun s => ∑ ρ ∈ t, seriesTermSub ρ₀ s ρ)
        = ∑ ρ ∈ t, (fun s => seriesTermSub ρ₀ s ρ) from by
      funext s; simp [Finset.sum_apply]]
    apply DifferentiableAt.differentiableWithinAt
    apply DifferentiableAt.sum
    intro ρ hρt
    by_cases h0 : ρ = ρ₀
    · show DifferentiableAt ℂ (fun s => if ρ = ρ₀ then (0 : ℂ) else seriesTerm s ρ) s
      simp only [if_pos h0]
      exact differentiableAt_const 0
    · have hsρ : s - (ρ : ℂ) ≠ 0 := by
        have hle : δ ≤ ‖(ρ : ℂ) - (ρ₀ : ℂ)‖ := hiso ρ h0
        have hlt : ‖s - (ρ₀ : ℂ)‖ < δ' := by
          have hmem := Metric.mem_ball.mp hs
          rwa [dist_eq_norm] at hmem
        intro hzero
        have h1 : ‖(ρ : ℂ) - (ρ₀ : ℂ)‖ ≤ ‖(ρ : ℂ) - s‖ + ‖s - (ρ₀ : ℂ)‖ := by
          nth_rewrite 1 [show (ρ : ℂ) - (ρ₀ : ℂ) = ((ρ : ℂ) - s) + (s - (ρ₀ : ℂ)) from by ring]
          exact norm_add_le _ _
        have h2 : ‖(ρ : ℂ) - s‖ = 0 := by
          have heq : s = (ρ : ℂ) := sub_eq_zero.mp hzero
          rw [← heq, sub_self, norm_zero]
        rw [h2] at h1
        linarith [hle, hlt, hδ, hδ']
      have hρ0 : (ρ : ℂ) ≠ 0 := by
        intro h
        have hlt := ρ.2.2.1
        rw [h] at hlt
        simp at hlt
      show DifferentiableAt ℂ (fun s => if ρ = ρ₀ then (0 : ℂ) else seriesTerm s ρ) s
      simp only [if_neg h0]
      show DifferentiableAt ℂ
          (fun s => (zeroMult ρ : ℂ) * (1 / (s - (ρ : ℂ)) + 1 / (ρ : ℂ))) s
      exact (((differentiableAt_const (1 : ℂ)).div
        (differentiableAt_id.sub (differentiableAt_const _)) hsρ).add
          (differentiableAt_const _)).const_mul _
  have han : AnalyticOnNhd ℂ (fun s => ∑' ρ, seriesTermSub ρ₀ s ρ) (Metric.ball (ρ₀ : ℂ) δ') :=
    hdiff.analyticOnNhd Metric.isOpen_ball
  exact han (ρ₀ : ℂ) (Metric.mem_ball_self hδ'0)

/-- The series with its ρ₀-term subtracted is analytic at ρ₀. -/
theorem seriesFun_sub_self_term_analyticAt (ρ₀ : {ρ : ℂ // IsNontrivialZero ρ}) :
    AnalyticAt ℂ (fun s => seriesFun s - seriesTerm s ρ₀) (ρ₀ : ℂ) := by
  apply AnalyticAt.congr (seriesFunSub_analyticAt ρ₀)
  exact Filter.Eventually.of_forall (fun s => (seriesFun_sub_term ρ₀ s).symm)

/-- The polar subtraction form consumed by 5e-iv: the series minus
mult(ρ₀)/(s−ρ₀) is analytic at ρ₀ (the +mult/ρ₀ part is a constant). -/
theorem seriesFun_sub_polar_analyticAt (ρ₀ : {ρ : ℂ // IsNontrivialZero ρ}) :
    AnalyticAt ℂ (fun s => seriesFun s - (zeroMult (ρ₀ : ℂ) : ℂ) / (s - (ρ₀ : ℂ)))
      (ρ₀ : ℂ) := by
  have h := seriesFun_sub_self_term_analyticAt ρ₀
  have heq : (fun s => seriesFun s - (zeroMult (ρ₀ : ℂ) : ℂ) / (s - (ρ₀ : ℂ)))
      = (fun s => (seriesFun s - seriesTerm s ρ₀) + (zeroMult (ρ₀ : ℂ) : ℂ) / (ρ₀ : ℂ)) := by
    funext s
    simp only [seriesTerm]
    ring
  rw [heq]
  exact h.add analyticAt_const

end NguyenRH1

end