LiSides.lean

Declarations

Source

/-
NguyenRH1/LiSides.lean — tier ii′ sub-stage ii′-1b(iii) (D-064 §4 R1):
the rectangle residue theorem for the Lagarias-kernel integrand

  J(w) = kFun n w · (−ζ′/ζ(w)),   kFun n w = (w/(w−1))ⁿ − 1   (= k_n(w−1)).

J is meromorphic on ℂ with: a pole of order n+1 at w = 1 (residue `ResW1 n`,
session 016), simple poles at every zero ρ of ζ with residue
mult(ρ)·(1 − (ρ/(ρ−1))ⁿ) (logDeriv poles are simple; multiple zeros OK).

Method (D-064 §4 R1): subtract the explicit principal part `ppart n` at 1
(session 016). The remainder R = J − P is:
* holomorphic off {1} ∪ {zeros of ζ} (product/quotient rule),
* BOUNDED near 1 (`Rfun_bounded_near_one`): on a punctured neighbourhood,
  (w−1)^{n+1}·R = F − TaylₙF where F(w) = (wⁿ−(w−1)ⁿ)·hLi(w) is analytic
  at 1 (`hLi_analyticAt_one`), and F − TaylₙF vanishes to order ≥ n+1
  (`Ffun_sub_TaylP_order`, via `natCast_le_analyticOrderAt_iff_
  iteratedDeriv_eq_zero`), so R extends continuously across 1;
* simple-poled at each zero ρ with the residue above (`Rfun_residue_at`,
  via the analytic-order normal form ζ = (w−ρ)^m·h, h(ρ) ≠ 0).

Then the vendored `residueTheorem_finset` (Zeta23.Analytic.RectangleLogDeriv)
plus session 016's `rectInt'_ppart` give `rectInt'_Jlag`:
for any rectangle with 1 interior and no zeros of ζ on the border,

  RectangleIntegral' (Jlag n) z w
    = ResW1 n + Σ_{ρ ∈ Sz} (zeroMult ρ)·(1 − (ρ/(ρ−1))ⁿ),

where Sz is any finset exactly capturing the zeros of zetaA (equivalently,
off 1, of ζ) inside the rectangle — produced downstream by the vendored
`finite_zeros_rectangle` (zetaA is entire, `zetaA_analyticAt_one`).

NOTE (deferred): the value mult(−2) = 1 (simplicity of the trivial zeros)
is NOT proved here; the sum keeps `zeroMult ρ` symbolic at trivial zeros.
The split Sz = {nontrivial zeros} ∪ {−2} on the D-064 rectangle
(σ ∈ [−5/2, 2√n]) is ii′-4 territory.

Archive references: D-036, D-037, D-064 (R1), journal-015/016.
-/
import Mathlib
import Zeta23.Analytic.RectangleLogDeriv
import NguyenRH1.LiPrincipal

open Zeta23 Complex Filter Topology
open scoped Nat

noncomputable section

namespace NguyenRH1

/-! ## 1. The integrand: kFun, Jlag, Rfun -/

/-- The kernel factor kFun n w = (w/(w−1))ⁿ − 1 (= k_n(w−1) with
k_n(x) = (1+1/x)ⁿ − 1). Pole of order n at w = 1, analytic elsewhere. -/
def kFun (n : ℕ) (s : ℂ) : ℂ := (s / (s - 1)) ^ n - 1

/-- The Lagarias-kernel integrand J(w) = kFun n w · (−ζ′/ζ(w)) (D-064 §2). -/
def Jlag (n : ℕ) (s : ℂ) : ℂ := kFun n s * (-(deriv riemannZeta s / riemannZeta s))

/-- The remainder R = J − P with P the principal part at 1 (LiPrincipal). -/
def Rfun (n : ℕ) : ℂ → ℂ := Jlag n - ppart n

lemma kFun_differentiableAt {n : ℕ} {s : ℂ} (hs : s ≠ 1) :
    DifferentiableAt ℂ (kFun n) s := by
  have h1d : DifferentiableAt ℂ (fun w : ℂ => w - 1) s :=
    differentiableAt_id.sub (differentiableAt_const 1)
  have h2d : DifferentiableAt ℂ (fun w : ℂ => w / (w - 1)) s :=
    differentiableAt_id.div h1d (sub_ne_zero.mpr hs)
  exact (h2d.pow n).sub (differentiableAt_const 1)

lemma ppart_differentiableAt {n : ℕ} {s : ℂ} (hs : s ≠ 1) :
    DifferentiableAt ℂ (ppart n) s := by
  rw [show (ppart n) = ∑ i ∈ Finset.Icc 1 (n + 1),
      (fun w : ℂ => Acoeff n i / (w - 1) ^ i) from by
    funext w; simp [ppart, Finset.sum_apply]]
  apply DifferentiableAt.sum
  intro i hi
  exact (differentiableAt_const _).div
    ((differentiableAt_id.sub (differentiableAt_const 1)).pow i)
    (pow_ne_zero _ (sub_ne_zero.mpr hs))

lemma Jlag_differentiableAt {n : ℕ} {s : ℂ} (hs1 : s ≠ 1) (hs0 : riemannZeta s ≠ 0) :
    DifferentiableAt ℂ (Jlag n) s := by
  have hζ : AnalyticAt ℂ riemannZeta s := analyticAt_riemannZeta hs1
  have hd : DifferentiableAt ℂ (fun w : ℂ => -(deriv riemannZeta w / riemannZeta w)) s :=
    (hζ.deriv.differentiableAt.div hζ.differentiableAt hs0).neg
  exact (kFun_differentiableAt hs1).mul hd

lemma Rfun_differentiableAt {n : ℕ} {s : ℂ} (hs1 : s ≠ 1) (hs0 : riemannZeta s ≠ 0) :
    DifferentiableAt ℂ (Rfun n) s :=
  (Jlag_differentiableAt hs1 hs0).sub (ppart_differentiableAt hs1)

lemma ppart_continuousAt {n : ℕ} {s : ℂ} (hs : s ≠ 1) :
    ContinuousAt (ppart n) s := by
  have hterm : ∀ i : ℕ, ContinuousAt (fun w => Acoeff n i / (w - 1) ^ i) s := by
    intro i
    have hw1 : s - 1 ≠ 0 := sub_ne_zero.mpr hs
    exact continuousAt_const.div ((continuousAt_id.sub continuousAt_const).pow _)
      (pow_ne_zero _ hw1)
  have : ∀ t : Finset ℕ, ContinuousAt (fun w => ∑ i ∈ t, Acoeff n i / (w - 1) ^ i) s := by
    intro t
    induction t using Finset.induction with
    | empty =>
      simp only [Finset.sum_empty]
      exact continuousAt_const
    | insert a t hat ht =>
      simp_rw [Finset.sum_insert hat]
      exact ContinuousAt.add (hterm a) ht
  exact this _

/-! ## 2. Finite order of ζ at every point ≠ 1 (via the entire zetaA) -/

lemma zetaA_analyticOnNhd_univ : AnalyticOnNhd ℂ zetaA Set.univ := by
  intro s _
  by_cases hs : s = 1
  · subst hs; exact zetaA_analyticAt_one
  · exact zetaA_analyticAt_of_ne hs

/-- ζ has finite analytic order at every ρ ≠ 1 (identity principle through
the entire function zetaA = (w−1)ζ, which is nonzero at 1). -/
lemma zeta_order_ne_top_of_ne {ρ : ℂ} (hρ : ρ ≠ 1) :
    analyticOrderAt riemannZeta ρ ≠ ⊤ := by
  have h0 : analyticOrderAt zetaA 1 = 0 :=
    (zetaA_analyticAt_one.analyticOrderAt_eq_zero).mpr (by rw [zetaA_one]; norm_num)
  have hA : analyticOrderAt zetaA ρ ≠ ⊤ :=
    AnalyticOnNhd.analyticOrderAt_ne_top_of_isPreconnected zetaA_analyticOnNhd_univ
      isPreconnected_univ (Set.mem_univ 1) (Set.mem_univ ρ) (by rw [h0]; simp)
  have hcong : zetaA =ᶠ[𝓝 ρ] (fun w : ℂ => w - 1) * riemannZeta := by
    filter_upwards [eventually_ne_nhds hρ] with w hw using zetaA_apply hw
  rw [analyticOrderAt_congr hcong,
    analyticOrderAt_mul (f := fun w : ℂ => w - 1) (g := riemannZeta)
      (analyticAt_id.sub analyticAt_const) (analyticAt_riemannZeta hρ)] at hA
  have h0' : analyticOrderAt (fun w : ℂ => w - 1) ρ = 0 :=
    ((show AnalyticAt ℂ (fun w : ℂ => w - 1) ρ from
      analyticAt_id.sub analyticAt_const).analyticOrderAt_eq_zero).mpr (sub_ne_zero.mpr hρ)
  rw [h0', zero_add] at hA
  exact hA

/-! ## 3. Interior points from border avoidance -/

/-- A point of the rectangle not on its border is interior (the rectangle is
a neighbourhood of it). Extracted from the vendored hZint argument. -/
lemma rectangle_mem_nhds_of_mem_not_border {z w p : ℂ} (hre : z.re ≤ w.re) (him : z.im ≤ w.im)
    (hmem : p ∈ Rectangle z w) (hb : p ∉ RectangleBorder z w) :
    Rectangle z w ∈ 𝓝 p := by
  obtain ⟨h1, h2⟩ := hmem
  have h1' : z.re ≤ p.re ∧ p.re ≤ w.re := by simpa [Set.uIcc_of_le hre] using h1
  have h2' : z.im ≤ p.im ∧ p.im ≤ w.im := by simpa [Set.uIcc_of_le him] using h2
  simp only [RectangleBorder, Set.mem_union, Complex.mem_reProdIm, Set.mem_singleton_iff,
    not_or] at hb
  obtain ⟨⟨⟨hb1, hb2⟩, hb3⟩, hb4⟩ := hb
  rw [rectangle_mem_nhds_iff, Complex.mem_reProdIm, Set.uIoo_of_le hre, Set.uIoo_of_le him]
  refine ⟨⟨lt_of_le_of_ne h1'.1 (fun h => hb2 ⟨h.symm, h2⟩),
    lt_of_le_of_ne h1'.2 (fun h => hb4 ⟨h, h2⟩)⟩,
    ⟨lt_of_le_of_ne h2'.1 (fun h => hb1 ⟨h1, h.symm⟩),
    lt_of_le_of_ne h2'.2 (fun h => hb3 ⟨h1, h⟩)⟩⟩

/-! ## 4. The removable singularity of R at w = 1 -/

/-- F(w) = (wⁿ−(w−1)ⁿ)·hLi(w) — the analytic-at-1 numerator (w−1)^{n+1}·J
(punctured). Same function as in `ResW1`/`Acoeff` (defeq). -/
def Ffun (n : ℕ) (w : ℂ) : ℂ := (w ^ n - (w - 1) ^ n) * hLi w

/-- The order-n Taylor polynomial of Ffun n at 1. -/
def TaylP (n : ℕ) (w : ℂ) : ℂ :=
  ∑ j ∈ Finset.range (n + 1), (iteratedDeriv j (Ffun n) 1 / j !) * (w - 1) ^ j

lemma Ffun_analyticAt_one (n : ℕ) : AnalyticAt ℂ (Ffun n) 1 :=
  ((analyticAt_id.pow n).sub ((analyticAt_id.sub analyticAt_const).pow n)).mul
    hLi_analyticAt_one

lemma TaylP_analyticAt (n : ℕ) (w : ℂ) : AnalyticAt ℂ (TaylP n) w := by
  have hterm : ∀ j : ℕ, AnalyticAt ℂ
      (fun w : ℂ => (iteratedDeriv j (Ffun n) 1 / j !) * (w - 1) ^ j) w :=
    fun j => analyticAt_const.mul ((analyticAt_id.sub analyticAt_const).pow j)
  have : ∀ t : Finset ℕ, AnalyticAt ℂ
      (fun w : ℂ => ∑ j ∈ t, (iteratedDeriv j (Ffun n) 1 / j !) * (w - 1) ^ j) w := by
    intro t
    induction t using Finset.induction with
    | empty =>
      simp only [Finset.sum_empty]
      exact analyticAt_const
    | insert a t hat ht =>
      simp_rw [Finset.sum_insert hat]
      exact (hterm a).add ht
  exact this _

/-- (w−1)^{n+1}·ppart n w is the Taylor polynomial of Ffun n at 1 (w ≠ 1). -/
lemma ppart_mul_pow (n : ℕ) {s : ℂ} (hs : s ≠ 1) :
    (s - 1) ^ (n + 1) * ppart n s = TaylP n s := by
  have hs1 : s - 1 ≠ 0 := sub_ne_zero.mpr hs
  show (s - 1) ^ (n + 1) * (∑ i ∈ Finset.Icc 1 (n + 1), Acoeff n i / (s - 1) ^ i) =
    ∑ j ∈ Finset.range (n + 1), (iteratedDeriv j (Ffun n) 1 / j !) * (s - 1) ^ j
  rw [Finset.mul_sum]
  apply Finset.sum_bij (fun i _ => n + 1 - i)
  · intro i hi
    rw [Finset.mem_Icc] at hi
    rw [Finset.mem_range]
    omega
  · intro a₁ ha₁ a₂ ha₂ h
    rw [Finset.mem_Icc] at ha₁ ha₂
    omega
  · intro j hj
    rw [Finset.mem_range] at hj
    exact ⟨n + 1 - j, by rw [Finset.mem_Icc]; omega, by omega⟩
  · intro i hi
    rw [Finset.mem_Icc] at hi
    have hA : Acoeff n i = iteratedDeriv (n + 1 - i) (Ffun n) 1 / (n + 1 - i) ! := rfl
    rw [hA]
    have e : (s - 1) ^ (n + 1) = (s - 1) ^ i * (s - 1) ^ (n + 1 - i) := by
      rw [← pow_add]; congr 1; omega
    have key : ∀ C : ℂ, (s - 1) ^ (n + 1) * (C / (s - 1) ^ i) = C * (s - 1) ^ (n + 1 - i) := by
      intro C
      have hi' : (s - 1) ^ i ≠ 0 := pow_ne_zero i hs1
      rw [e]
      field_simp [hi']
    exact key _

/-- (w−1)^{n+1}·Jlag n w = Ffun n w off 1 and off the zeros of ζ. -/
lemma Jlag_mul_pow (n : ℕ) {s : ℂ} (hs1 : s ≠ 1) (hs0 : riemannZeta s ≠ 0) :
    (s - 1) ^ (n + 1) * Jlag n s = Ffun n s := by
  have h1 : s - 1 ≠ 0 := sub_ne_zero.mpr hs1
  have h2 : (s - 1) ^ n ≠ 0 := pow_ne_zero n h1
  have hk : kFun n s = (s ^ n - (s - 1) ^ n) / (s - 1) ^ n := by
    show (s / (s - 1)) ^ n - 1 = (s ^ n - (s - 1) ^ n) / (s - 1) ^ n
    rw [div_pow]
    field_simp [h2]
  show (s - 1) ^ (n + 1) * (kFun n s * (-(deriv riemannZeta s / riemannZeta s))) =
    (s ^ n - (s - 1) ^ n) * hLi s
  rw [hk, hLi_eq_of_ne hs1 hs0, pow_succ]
  field_simp [h2, hs0]

/-- On a punctured neighbourhood of 1, R n = (Ffun n − TaylP n)/(w−1)^{n+1}. -/
lemma Rfun_eq_sub_div_near_one (n : ℕ) :
    ∀ᶠ s in 𝓝[≠] (1 : ℂ), Rfun n s = (Ffun n s - TaylP n s) / (s - 1) ^ (n + 1) := by
  have hne : ∀ᶠ s in 𝓝[≠] (1 : ℂ), riemannZeta s ≠ 0 := by
    have h := riemannZeta_residue_one.eventually_ne (show (1 : ℂ) ≠ 0 by norm_num)
    filter_upwards [h] with w hw
    have h2 := hw
    simp only [ne_eq, mul_eq_zero] at h2
    push Not at h2
    exact h2.2
  filter_upwards [hne, self_mem_nhdsWithin] with s hs0 hs1
  have hs1' : s ≠ 1 := hs1
  have h1 : (s - 1) ^ (n + 1) ≠ 0 := pow_ne_zero _ (sub_ne_zero.mpr hs1')
  have e : (s - 1) ^ (n + 1) * Rfun n s = Ffun n s - TaylP n s := by
    have e1 := Jlag_mul_pow n hs1' hs0
    have e2 := ppart_mul_pow n hs1'
    show (s - 1) ^ (n + 1) * (Jlag n s - ppart n s) = Ffun n s - TaylP n s
    rw [mul_sub, e1, e2]
  exact eq_div_of_mul_eq h1 (by rw [mul_comm]; exact e)

/-- The i-th iterated derivative of the Taylor polynomial at 1 matches
Ffun's (i ≤ n): the j ≠ i summands vanish by the descFactorial/0^k split. -/
lemma iteratedDeriv_TaylP {n i : ℕ} (hi : i ≤ n) :
    iteratedDeriv i (TaylP n) 1 = iteratedDeriv i (Ffun n) 1 := by
  have hterm : ∀ j ∈ Finset.range (n + 1),
      ContDiffAt ℂ i (fun w : ℂ => (iteratedDeriv j (Ffun n) 1 / j !) * (w - 1) ^ j) 1 :=
    fun j _ => contDiffAt_const.mul (((contDiff_id.sub contDiff_const).pow j).contDiffAt)
  have hdp : ∀ j : ℕ, iteratedDeriv i (fun w : ℂ => (w - 1) ^ j) (1 : ℂ) =
      (j.descFactorial i : ℂ) * (0 : ℂ) ^ (j - i) := by
    intro j
    have e := congr_fun (iteratedDeriv_comp_sub_const i (fun w : ℂ => w ^ j) (1 : ℂ)) 1
    rw [iteratedDeriv_pow] at e
    simpa using e
  rw [show (TaylP n) = ∑ j ∈ Finset.range (n + 1),
      (fun w : ℂ => (iteratedDeriv j (Ffun n) 1 / j !) * (w - 1) ^ j) from by
    funext w; simp [TaylP, Finset.sum_apply]]
  rw [iteratedDeriv_sum hterm]
  have hpoint : ∀ j ∈ Finset.range (n + 1),
      iteratedDeriv i (fun w : ℂ => (iteratedDeriv j (Ffun n) 1 / j !) * (w - 1) ^ j) 1 =
        (iteratedDeriv j (Ffun n) 1 / j !) * ((j.descFactorial i : ℂ) * (0 : ℂ) ^ (j - i)) := by
    intro j hj
    rw [iteratedDeriv_const_mul_field, hdp j]
  rw [Finset.sum_congr rfl hpoint]
  rw [Finset.sum_eq_single i]
  · have hfi : ((i ! : ℕ) : ℂ) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero i)
    rw [Nat.descFactorial_self]
    simp only [Nat.sub_self, pow_zero, mul_one]
    exact div_mul_cancel₀ _ hfi
  · intro j hj hji
    rw [Finset.mem_range] at hj
    by_cases hlt : j < i
    · have h0 : (j.descFactorial i : ℂ) = 0 := by
        have h := Nat.descFactorial_eq_zero_iff_lt.mpr hlt
        exact_mod_cast h
      simp [h0]
    · have h0 : (0 : ℂ) ^ (j - i) = 0 := zero_pow (by omega)
      simp [h0]
  · intro hi'
    rw [Finset.mem_range] at hi'
    omega

/-- Ffun n − TaylP n vanishes to order ≥ n+1 at 1. -/
lemma Ffun_sub_TaylP_iteratedDeriv (n i : ℕ) (hi : i ≤ n) :
    iteratedDeriv i (Ffun n - TaylP n) 1 = 0 := by
  have hF : ContDiffAt ℂ i (Ffun n) 1 := (Ffun_analyticAt_one n).contDiffAt
  have hT : ContDiffAt ℂ i (TaylP n) 1 := (TaylP_analyticAt n 1).contDiffAt
  rw [iteratedDeriv_sub hF hT, iteratedDeriv_TaylP hi, sub_self]

lemma Ffun_sub_TaylP_order (n : ℕ) :
    ((n + 1 : ℕ) : ℕ∞) ≤ analyticOrderAt (Ffun n - TaylP n) 1 := by
  rw [natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero
    ((Ffun_analyticAt_one n).sub (TaylP_analyticAt n 1))]
  intro i hi
  exact Ffun_sub_TaylP_iteratedDeriv n i (Nat.lt_succ_iff.mp hi)

/-- R converges at 1 along the punctured filter (the would-be residue value). -/
lemma Rfun_tendsto_one (n : ℕ) :
    ∃ L : ℂ, Tendsto (Rfun n) (𝓝[≠] (1 : ℂ)) (𝓝 L) := by
  have hgan : AnalyticAt ℂ (Ffun n - TaylP n) 1 :=
    (Ffun_analyticAt_one n).sub (TaylP_analyticAt n 1)
  have hord : ((n + 1 : ℕ) : ℕ∞) ≤ analyticOrderAt (Ffun n - TaylP n) 1 :=
    Ffun_sub_TaylP_order n
  by_cases htop : analyticOrderAt (Ffun n - TaylP n) 1 = ⊤
  · refine ⟨0, ?_⟩
    have h0 : ∀ᶠ s in 𝓝 (1 : ℂ), (Ffun n - TaylP n) s = 0 := analyticOrderAt_eq_top.mp htop
    have hev : (Rfun n) =ᶠ[𝓝[≠] (1 : ℂ)] (fun _ => (0 : ℂ)) := by
      filter_upwards [Rfun_eq_sub_div_near_one n, mem_nhdsWithin_of_mem_nhds h0] with s hs hg0
      have hg0' : Ffun n s - TaylP n s = 0 := hg0
      rw [hs, hg0']
      exact zero_div _
    exact tendsto_const_nhds.congr' hev.symm
  · obtain ⟨h, hh, hh0, hfh⟩ := hgan.analyticOrderAt_ne_top.mp htop
    have hnm : n + 1 ≤ analyticOrderNatAt (Ffun n - TaylP n) 1 := by
      rw [← Nat.cast_analyticOrderNatAt htop] at hord
      exact ENat.natCast_le_natCast.mp hord
    have hev : (Rfun n) =ᶠ[𝓝[≠] (1 : ℂ)]
        (fun s => (s - 1) ^ (analyticOrderNatAt (Ffun n - TaylP n) 1 - (n + 1)) * h s) := by
      filter_upwards [Rfun_eq_sub_div_near_one n,
        mem_nhdsWithin_of_mem_nhds hfh.eventually_nhds, self_mem_nhdsWithin] with s hs hgf hs1
      have hs1' : s ≠ 1 := hs1
      have hs1n : s - 1 ≠ 0 := sub_ne_zero.mpr hs1'
      rw [hs]
      have hgs : (Ffun n - TaylP n) s =
          (s - 1) ^ analyticOrderNatAt (Ffun n - TaylP n) 1 * h s := by
        have h2 := hgf.self_of_nhds
        rwa [smul_eq_mul] at h2
      have hgs' : Ffun n s - TaylP n s =
          (s - 1) ^ analyticOrderNatAt (Ffun n - TaylP n) 1 * h s := hgs
      rw [hgs']
      have e : (s - 1) ^ analyticOrderNatAt (Ffun n - TaylP n) 1 =
          (s - 1) ^ (n + 1) *
            (s - 1) ^ (analyticOrderNatAt (Ffun n - TaylP n) 1 - (n + 1)) := by
        rw [← pow_add]
        congr 1
        omega
      rw [e, mul_assoc, mul_div_cancel_left₀ _ (pow_ne_zero (n + 1) hs1n)]
    refine ⟨(1 - 1 : ℂ) ^ (analyticOrderNatAt (Ffun n - TaylP n) 1 - (n + 1)) * h 1, ?_⟩
    have hcont : ContinuousAt
        (fun s : ℂ => (s - 1) ^ (analyticOrderNatAt (Ffun n - TaylP n) 1 - (n + 1)) * h s) 1 :=
      ((continuousAt_id.sub continuousAt_const).pow _).mul hh.continuousAt
    exact (hcont.tendsto.mono_left nhdsWithin_le_nhds).congr' hev.symm

/-- The near-condition at 1 with residue 0: R is bounded on the punctured
neighbourhood (the singularity is removable). -/
lemma Rfun_bounded_near_one (n : ℕ) : (Rfun n) =O[𝓝[≠] (1 : ℂ)] (1 : ℂ → ℂ) := by
  obtain ⟨L, hL⟩ := Rfun_tendsto_one n
  exact hL.isBigO_one ℂ

/-! ## 5. The residue at a zero of ζ -/

/-- At any ρ ≠ 1, R has at worst a simple pole with residue
zeroMult(ρ)·(1 − (ρ/(ρ−1))ⁿ) (zero if ζ(ρ) ≠ 0). Via the order normal form
ζ = (w−ρ)^m·h near ρ: −ζ′/ζ = −m/(w−ρ) − h′/h, and the kFun slope and the
principal part are continuous at ρ. -/
lemma Rfun_residue_at (n : ℕ) {ρ : ℂ} (hρ : ρ ≠ 1) :
    ((Rfun n) - fun s => ((zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)) / (s - ρ))
      =O[𝓝[≠] ρ] (1 : ℂ → ℂ) := by
  have hρα : AnalyticAt ℂ riemannZeta ρ := analyticAt_riemannZeta hρ
  obtain ⟨h, hh, hh0, hfh⟩ := hρα.analyticOrderAt_ne_top.mp (zeta_order_ne_top_of_ne hρ)
  have hkd : DifferentiableAt ℂ (kFun n) ρ := kFun_differentiableAt hρ
  have hexp : ∀ᶠ s in 𝓝[≠] ρ,
      (-(analyticOrderNatAt riemannZeta ρ : ℂ) * ((kFun n s - kFun n ρ) / (s - ρ))
          - kFun n s * logDeriv h s - ppart n s)
        = ((Rfun n) - fun s => ((zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)) / (s - ρ)) s := by
    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 hA : (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n) =
        -(analyticOrderNatAt riemannZeta ρ : ℂ) * kFun n ρ := by
      have hmz : (zeroMult ρ : ℂ) = (analyticOrderNatAt riemannZeta ρ : ℂ) := rfl
      rw [hmz]
      show (analyticOrderNatAt riemannZeta ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n) =
        -(analyticOrderNatAt riemannZeta ρ : ℂ) * ((ρ / (ρ - 1)) ^ n - 1)
      ring
    simp only [Pi.sub_apply, Rfun, Jlag, hA]
    rw [← logDeriv_apply, hld]
    field_simp [hsρ']
    ring
  have hslope : Tendsto (fun s => (kFun n s - kFun n ρ) / (s - ρ)) (𝓝[≠] ρ)
      (𝓝 (deriv (kFun n) ρ)) := by
    have h2 := hasDerivAt_iff_tendsto_slope.mp hkd.hasDerivAt
    simpa only [slope_fun_def_field] using h2
  have hcont1 : Tendsto (fun s => kFun n s * logDeriv h s) (𝓝[≠] ρ)
      (𝓝 (kFun n ρ * logDeriv h ρ)) := by
    have hc : ContinuousAt (fun s => kFun n s * (deriv h s / h s)) ρ :=
      hkd.continuousAt.mul (hh.deriv.continuousAt.div hh.continuousAt hh0)
    simpa only [logDeriv_apply] using hc.tendsto.mono_left nhdsWithin_le_nhds
  have hcont2 : Tendsto (ppart n) (𝓝[≠] ρ) (𝓝 (ppart n ρ)) :=
    (ppart_continuousAt hρ).tendsto.mono_left nhdsWithin_le_nhds
  have hT : Tendsto
      (fun s => -(analyticOrderNatAt riemannZeta ρ : ℂ) * ((kFun n s - kFun n ρ) / (s - ρ))
        - kFun n s * logDeriv h s - ppart n s)
      (𝓝[≠] ρ)
      (𝓝 (-(analyticOrderNatAt riemannZeta ρ : ℂ) * deriv (kFun n) ρ
        - kFun n ρ * logDeriv h ρ - ppart n ρ)) :=
    ((hslope.const_mul _).sub hcont1).sub hcont2
  exact (hT.isBigO_one ℂ).congr' hexp EventuallyEq.rfl

/-! ## 6. The rectangle residue theorem for J -/

/-- **Rectangle residue theorem for the Lagarias-kernel integrand** (D-064 §2):
on any rectangle with 1 interior and no zeros of ζ on the border,
  RectangleIntegral' (Jlag n) z w
    = ResW1 n + Σ_{ρ ∈ Sz} (zeroMult ρ)·(1 − (ρ/(ρ−1))ⁿ),
where Sz captures exactly the zeros of zetaA (⟺ zeros of ζ off 1) inside. -/
theorem rectInt'_Jlag (n : ℕ) {z w : ℂ} (hre : z.re ≤ w.re) (him : z.im ≤ w.im)
    (h1 : Rectangle z w ∈ 𝓝 (1 : ℂ))
    (hborder : ∀ s ∈ RectangleBorder z w, riemannZeta s ≠ 0)
    (Sz : Finset ℂ) (hSz : ∀ s : ℂ, s ∈ Sz ↔ s ∈ Rectangle z w ∧ zetaA s = 0) :
    RectangleIntegral' (Jlag n) z w =
      ResW1 n + ∑ ρ ∈ Sz, (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n) := by
  classical
  have hzA1 : zetaA 1 ≠ 0 := by rw [zetaA_one]; norm_num
  have h1notSz : (1 : ℂ) ∉ Sz := fun h => hzA1 ((hSz 1).mp h).2
  have hSz_ne_one : ∀ ρ ∈ Sz, ρ ≠ 1 := fun ρ hρ h => h1notSz (h ▸ hρ)
  have hSz_zeta : ∀ ρ ∈ Sz, riemannZeta ρ = 0 := by
    intro ρ hρ
    have hρ1 := hSz_ne_one ρ hρ
    have h2 := ((hSz ρ).mp hρ).2
    rw [zetaA_apply hρ1, mul_eq_zero] at h2
    rcases h2 with h | h
    · exact absurd (sub_eq_zero.mp h) hρ1
    · exact h
  have hSzint : ∀ ρ ∈ Sz, Rectangle z w ∈ 𝓝 ρ := by
    intro ρ hρ
    exact rectangle_mem_nhds_of_mem_not_border hre him ((hSz ρ).mp hρ).1
      (fun hb => hborder ρ hb (hSz_zeta ρ hρ))
  set A : ℂ → ℂ := fun p => if p = 1 then 0 else (zeroMult p : ℂ) * (1 - (p / (p - 1)) ^ n)
    with hAdef
  have fHolo : HolomorphicOn (Rfun n) (Rectangle z w \ ↑(insert (1 : ℂ) Sz)) := by
    intro s hs
    have hsc : s ∉ (↑(insert (1 : ℂ) Sz) : Set ℂ) := hs.2
    have hs1 : s ≠ 1 := fun h =>
      hsc (Finset.mem_coe.mpr (h.symm ▸ Finset.mem_insert_self 1 Sz))
    have hsSz : s ∉ Sz := fun h => hsc (Finset.mem_coe.mpr (Finset.mem_insert_of_mem h))
    have hs0 : riemannZeta s ≠ 0 := by
      intro h0
      exact hsSz ((hSz s).mpr ⟨hs.1, by rw [zetaA_apply hs1, h0, mul_zero]⟩)
    exact (Rfun_differentiableAt hs1 hs0).differentiableWithinAt
  have key := Analytic.residueTheorem_finset (f := Rfun n) hre him (insert 1 Sz) A
    (by
      intro p hp
      rw [Finset.mem_insert] at hp
      rcases hp with rfl | hp
      · exact h1
      · exact hSzint p hp)
    fHolo
    (by
      intro p hp
      rw [Finset.mem_insert] at hp
      rcases hp with rfl | hp
      · have hA1 : A 1 = 0 := by simp [hAdef]
        have h2 : ((Rfun n) - fun s => A 1 / (s - 1)) = Rfun n := by
          funext s
          simp [hA1]
        rw [h2]
        exact Rfun_bounded_near_one n
      · have hp1 : p ≠ 1 := hSz_ne_one p hp
        have hAp : A p = (zeroMult p : ℂ) * (1 - (p / (p - 1)) ^ n) := by simp [hAdef, hp1]
        rw [hAp]
        exact Rfun_residue_at n hp1)
  have hsum : ∑ p ∈ insert 1 Sz, A p =
      ∑ ρ ∈ Sz, (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n) := by
    rw [Finset.sum_insert h1notSz]
    have hA1 : A 1 = 0 := by simp [hAdef]
    rw [hA1, zero_add]
    apply Finset.sum_congr rfl
    intro ρ hρ
    have hρ1 := hSz_ne_one ρ hρ
    simp [hAdef, hρ1]
  rw [hsum] at key
  have hRint : RectangleBorderIntegrable (Rfun n) z w := by
    apply ContinuousOn.rectangleBorder_integrable
    apply fHolo.continuousOn.mono
    intro s hs
    have hsR : s ∈ Rectangle z w := rectangleBorder_subset_rectangle z w hs
    refine ⟨hsR, fun hsc => ?_⟩
    rw [Finset.mem_coe, Finset.mem_insert] at hsc
    rcases hsc with h | h
    · exact not_mem_rectangleBorder_of_rectangle_mem_nhds h1 (h ▸ hs)
    · exact hborder s hs (hSz_zeta s h)
  have hPint : RectangleBorderIntegrable (ppart n) z w := by
    apply HolomorphicOn.rectangleBorderIntegrable' _ h1
    intro s hs
    exact (ppart_differentiableAt hs.2).differentiableWithinAt
  have heq : Jlag n = Rfun n + ppart n := (sub_add_cancel _ _).symm
  rw [heq, RectangleIntegral'_add _ _ _ _ hRint hPint, key, rectInt'_ppart hre him h1]
  ring

end NguyenRH1