LiResidue.lean

Declarations

Source

/-
NguyenRH1/LiResidue.lean — tier ii′ sub-stage ii′-1b (D-064 §4 R1):
the w = 1 residue of the Lagarias-kernel integrand, computed exactly.

Contents (Part 1):
* `zetaA w = (w−1)·ζ(w)` extended by 1 at w = 1 — analytic at 1 with
  value 1 (removable singularity; Mathlib `riemannZeta_residue_one` +
  `differentiableOn_update_limUnder_of_bddAbove`).
* `hLi w = 1 − (w−1)·(zetaA′/zetaA)(w)` — analytic at 1, hLi 1 = 1;
  agrees with (w−1)·(−ζ′/ζ)(w) on a punctured neighborhood of 1
  (`hLi_eq_near_one`).
* `lcoeff k` — the Laurent coefficients of −ζ′/ζ at 1, DEFINED as
  iteratedDeriv (k+1) hLi 1 / (k+1)!.
* `ResW1 n` — the residue at w = 1 of J(w) = k_n(w−1)·(−ζ′/ζ(w)),
  packaged as (1/n!)·(d/dw)ⁿ[(wⁿ−(w−1)ⁿ)·hLi] at w = 1 (D-064 §4 R1:
  (w−1)^{n+1}J = [wⁿ−(w−1)ⁿ]·hLi on a punctured neighborhood, by
  `hLi_eq_near_one`). Value: `ResW1_eq_sum`.

Archive references: D-036, D-037, D-064 (R1), journal-014/015.
-/
import Mathlib
import Zeta23.Statement
import Zeta23.FromPNTPlus.ZetaBounds

open Zeta23 Complex Filter Topology
open scoped Nat

noncomputable section

namespace NguyenRH1

/-! ## 1. The regularized factor zetaA = (w−1)ζ(w) at w = 1 -/

/-- `zetaA w = (w−1)·ζ(w)` with the removable singularity at w = 1 filled
by the residue value 1. Analytic at 1 (`zetaA_analyticAt_one`), value
`zetaA 1 = 1`. -/
def zetaA : ℂ → ℂ := Function.update (fun w => (w - 1) * riemannZeta w) 1 1

lemma zetaA_apply {w : ℂ} (hw : w ≠ 1) : zetaA w = (w - 1) * riemannZeta w :=
  Function.update_of_ne hw _ _

lemma zetaA_one : zetaA 1 = 1 := Function.update_self _ _ _

/-- The regularized factor is analytic at w = 1 (removable singularity). -/
lemma zetaA_analyticAt_one : AnalyticAt ℂ zetaA 1 := by
  have hT := riemannZeta_residue_one
  rw [Metric.tendsto_nhdsWithin_nhds] at hT
  obtain ⟨δ, hδ0, hδ⟩ := hT 1 one_pos
  have hdiff : DifferentiableOn ℂ (fun w => (w - 1) * riemannZeta w)
      (Metric.ball 1 (δ / 2) \ {1}) := by
    intro w hw
    have hw1 : w ≠ 1 := hw.2
    exact ((differentiableAt_id.sub (differentiableAt_const 1)).mul
      (differentiableAt_riemannZeta hw1)).differentiableWithinAt
  have hbd : BddAbove ((fun z => ‖(z - 1) * riemannZeta z‖) ''
      (Metric.ball 1 (δ / 2) \ {1})) := by
    refine ⟨2, ?_⟩
    rintro _ ⟨z, hz, rfl⟩
    have hz1 : z ≠ 1 := hz.2
    have hdist : dist z 1 < δ := by
      have := hz.1
      rw [Metric.mem_ball] at this
      linarith [this, hδ0]
    have h1 := hδ (Set.mem_compl_singleton_iff.mpr hz1) hdist
    rw [dist_eq_norm] at h1
    have h2 : ‖(z - 1) * riemannZeta z‖ ≤ ‖(z - 1) * riemannZeta z - 1‖ + ‖(1 : ℂ)‖ := by
      nth_rewrite 1 [show (z - 1) * riemannZeta z =
        ((z - 1) * riemannZeta z - 1) + 1 from by ring]
      exact norm_add_le _ _
    rw [norm_one] at h2
    linarith [h1, h2]
  have h := differentiableOn_update_limUnder_of_bddAbove
    (Metric.ball_mem_nhds 1 (by positivity : (0 : ℝ) < δ / 2)) hdiff hbd
  have hlim : limUnder (𝓝[≠] (1 : ℂ)) (fun w => (w - 1) * riemannZeta w) = 1 :=
    riemannZeta_residue_one.limUnder_eq
  rw [hlim] at h
  have han := h.analyticOnNhd Metric.isOpen_ball
  exact han 1 (Metric.mem_ball_self (by positivity : (0 : ℝ) < δ / 2))

/-- zetaA is nonzero on a neighborhood of 1 (value 1 there). -/
lemma zetaA_ne_zero_near_one : ∀ᶠ w in 𝓝 (1 : ℂ), zetaA w ≠ 0 :=
  (zetaA_analyticAt_one.continuousAt).eventually_ne (by rw [zetaA_one]; norm_num)

/-- zetaA is analytic at any w ≠ 1 (agrees with (w−1)ζ there). -/
lemma zetaA_analyticAt_of_ne {w : ℂ} (hw : w ≠ 1) : AnalyticAt ℂ zetaA w := by
  have h : (fun w => (w - 1) * riemannZeta w) =ᶠ[𝓝 w] zetaA := by
    filter_upwards [eventually_ne_nhds hw] with z hz using (zetaA_apply hz).symm
  have ha : AnalyticAt ℂ (fun w => (w - 1) * riemannZeta w) w :=
    (analyticAt_id.sub analyticAt_const).mul (analyticAt_riemannZeta hw)
  exact ha.congr h

/-! ## 2. hLi w = 1 − (w−1)·(zetaA′/zetaA)(w): analytic at 1, value 1 -/

/-- hLi(w) = 1 − (w−1)·(zetaA′/zetaA)(w) — the analytic-at-1 form of
(w−1)(−ζ′/ζ)(w) (`hLi_eq_near_one`). hLi 1 = 1. -/
def hLi (w : ℂ) : ℂ := 1 - (w - 1) * (deriv zetaA w / zetaA w)

lemma hLi_one : hLi 1 = 1 := by simp [hLi]

lemma hLi_analyticAt_one : AnalyticAt ℂ hLi 1 := by
  have ha := zetaA_analyticAt_one
  have hda : AnalyticAt ℂ (deriv zetaA) 1 := ha.deriv
  have hne : zetaA 1 ≠ 0 := by rw [zetaA_one]; norm_num
  have hprod : AnalyticAt ℂ (fun w => (w - 1) * (deriv zetaA w / zetaA w)) 1 :=
    (analyticAt_id.sub analyticAt_const).mul (hda.div ha hne)
  exact analyticAt_const.sub hprod

/-- On the punctured plane minus zeros of ζ, hLi = (w−1)·(−ζ′/ζ). -/
lemma hLi_eq_of_ne {w : ℂ} (hw1 : w ≠ 1) (hw0 : riemannZeta w ≠ 0) :
    hLi w = (w - 1) * (-(deriv riemannZeta w) / riemannZeta w) := by
  have hA : zetaA w = (w - 1) * riemannZeta w := zetaA_apply hw1
  have hdA : deriv zetaA w = riemannZeta w + (w - 1) * deriv riemannZeta w := by
    have h1 : deriv (fun z => (z - 1) * riemannZeta z) w =
        deriv (fun z => z - 1) w * riemannZeta w +
          (w - 1) * deriv riemannZeta w :=
      deriv_mul ((differentiableAt_id.sub (differentiableAt_const 1)))
        (differentiableAt_riemannZeta hw1)
    have h2 : deriv (fun z => z - 1) w = 1 := by
      simp [deriv_id'']
    have h3 : (fun z => (z - 1) * riemannZeta z) =ᶠ[𝓝 w] zetaA := by
      filter_upwards [eventually_ne_nhds hw1] with z hz using (zetaA_apply hz).symm
    rw [← h3.deriv_eq, h1, h2, one_mul]
  rw [hLi, hdA, hA]
  have hw1' : w - 1 ≠ 0 := sub_ne_zero.mpr hw1
  field_simp [hw0, hw1']
  ring

/-- On a punctured neighborhood of 1, hLi = (w−1)·(−ζ′/ζ). -/
lemma hLi_eq_near_one :
    ∀ᶠ w in 𝓝[≠] (1 : ℂ), hLi w = (w - 1) * (-(deriv riemannZeta w) / riemannZeta w) := by
  have hne : ∀ᶠ w in 𝓝[≠] (1 : ℂ), (w - 1) * riemannZeta w ≠ 0 :=
    riemannZeta_residue_one.eventually_ne (show (1 : ℂ) ≠ 0 by norm_num)
  filter_upwards [hne, eventually_mem_nhdsWithin] with w hw hw1
  have hz : riemannZeta w ≠ 0 := by
    have h2 := hw
    simp only [ne_eq, mul_eq_zero] at h2
    push Not at h2
    exact h2.2
  exact hLi_eq_of_ne hw1 hz

/-! ## 3. The Laurent coefficients of −ζ′/ζ at 1 (operational definition) -/

/-- The k-th Laurent coefficient of −ζ′/ζ at s = 1, DEFINED as
iteratedDeriv (k+1) hLi 1 / (k+1)! (the power-series coefficient of the
analytic hLi; the identification with −ζ′/ζ's Laurent expansion is
`hLi_eq_near_one`). -/
def lcoeff (k : ℕ) : ℂ := iteratedDeriv (k + 1) hLi 1 / (k + 1)!

/-- hLi's Taylor coefficients: iteratedDeriv j hLi 1 / j ! = lcoeff (j−1). -/
lemma hLi_iteratedDeriv_div_factorial {j : ℕ} (hj : 1 ≤ j) :
    iteratedDeriv j hLi 1 / j ! = lcoeff (j - 1) := by
  rw [lcoeff, show j - 1 + 1 = j from by omega]

/-! ## 4. The A-polynomial derivative: A(w) = wⁿ − (w−1)ⁿ -/

/-- Iterated derivatives of A(w) = wⁿ − (w−1)ⁿ at 1:
A^{(i)}(1) = n.descFactorial i for i < n, and A^{(n)}(1) = 0. -/
lemma A_iter (n i : ℕ) (hi : i ≤ n) :
    iteratedDeriv i (fun w : ℂ => w ^ n - (w - 1) ^ n) (1 : ℂ) =
      if i < n then n.descFactorial i else 0 := by
  have hf : ContDiffAt ℂ i (fun w : ℂ => w ^ n) 1 :=
    (contDiff_id.pow n).contDiffAt
  have hg : ContDiffAt ℂ i (fun w : ℂ => (w - 1) ^ n) 1 :=
    ((contDiff_id.sub contDiff_const).pow n).contDiffAt
  rw [show (fun w : ℂ => w ^ n - (w - 1) ^ n) =
    (fun w : ℂ => w ^ n) - (fun w : ℂ => (w - 1) ^ n) from by
    funext w; simp [Pi.sub_apply], iteratedDeriv_sub hf hg]
  have h1 : iteratedDeriv i (fun w : ℂ => w ^ n) 1 = n.descFactorial i := by
    rw [iteratedDeriv_pow]
    simp
  have h2 : iteratedDeriv i (fun w : ℂ => (w - 1) ^ n) 1 =
      n.descFactorial i * (0 : ℂ) ^ (n - i) := by
    have e := congr_fun (iteratedDeriv_comp_sub_const i (fun w : ℂ => w ^ n) (1 : ℂ)) 1
    rw [iteratedDeriv_pow] at e
    simpa using e
  rw [h1, h2]
  by_cases hin : i < n
  · rw [if_pos hin]
    have hz : (0 : ℂ) ^ (n - i) = 0 := zero_pow (by omega)
    rw [hz, mul_zero, sub_zero]
  · rw [if_neg hin]
    have hin' : i = n := le_antisymm hi (by omega)
    subst hin'
    simp [Nat.descFactorial_self]

/-! ## 5. The residue at w = 1: ResW1 n = Σ_{j=1}^n C(n,j)·lcoeff (j−1) -/

/-- The residue at w = 1 of the Lagarias-kernel integrand
J(w) = k_n(w−1)·(−ζ′/ζ(w)), packaged as (1/n!)·(d/dw)ⁿ[(wⁿ−(w−1)ⁿ)hLi]
at w = 1 (D-064 §4 R1: (w−1)^{n+1}J = [wⁿ−(w−1)ⁿ]·hLi punctured near 1,
by `hLi_eq_near_one`). -/
def ResW1 (n : ℕ) : ℂ :=
  iteratedDeriv n (fun w : ℂ => (w ^ n - (w - 1) ^ n) * hLi w) (1 : ℂ) / n !

/-- The w = 1 residue value: ResW1 n = Σ_{j=1}^n C(n,j)·lcoeff (j−1). -/
theorem ResW1_eq_sum (n : ℕ) :
    ResW1 n = ∑ j ∈ Finset.Icc 1 n, (n.choose j : ℂ) * lcoeff (j - 1) := by
  have hA : ContDiffAt ℂ n (fun w : ℂ => w ^ n - (w - 1) ^ n) 1 :=
    ((contDiff_id.pow n).sub ((contDiff_id.sub contDiff_const).pow n)).contDiffAt
  have hh : ContDiffAt ℂ n hLi 1 := hLi_analyticAt_one.contDiffAt
  have hmul : iteratedDeriv n (fun w => (w ^ n - (w - 1) ^ n) * hLi w) 1 =
      ∑ i ∈ Finset.range (n + 1),
        n.choose i * iteratedDeriv i (fun w : ℂ => w ^ n - (w - 1) ^ n) 1 *
          iteratedDeriv (n - i) hLi 1 := by
    have h := iteratedDeriv_mul hA hh
    rw [show (fun w => (w ^ n - (w - 1) ^ n) * hLi w) =
      (fun w : ℂ => w ^ n - (w - 1) ^ n) * hLi from by
      funext w; simp [Pi.mul_apply]]
    exact h
  rw [ResW1, hmul]
  have hsum : (∑ i ∈ Finset.range (n + 1),
        n.choose i * iteratedDeriv i (fun w : ℂ => w ^ n - (w - 1) ^ n) 1 *
          iteratedDeriv (n - i) hLi 1) =
      ∑ i ∈ Finset.range n,
        n.choose i * (n.descFactorial i : ℂ) * iteratedDeriv (n - i) hLi 1 := by
    rw [Finset.sum_range_succ]
    simp [A_iter n n le_rfl]
    apply Finset.sum_congr rfl
    intro i hi
    rw [Finset.mem_range] at hi
    rw [A_iter n i (by omega), if_pos hi]
  rw [hsum]
  have hterm : ∀ i ∈ Finset.range n,
      n.choose i * (n.descFactorial i : ℂ) * iteratedDeriv (n - i) hLi 1 / n ! =
        (n.choose i : ℂ) * lcoeff (n - i - 1) := by
    intro i hi
    rw [Finset.mem_range] at hi
    have hdesc : (n.descFactorial i : ℂ) = (n ! : ℂ) / ((n - i) ! : ℂ) := by
      have h2 := Nat.factorial_mul_descFactorial (show i ≤ n by omega)
      have hcast : ((n - i) ! : ℂ) * (n.descFactorial i : ℂ) = (n ! : ℂ) := by
        exact_mod_cast h2
      rw [eq_div_iff_mul_eq (by simp [Nat.factorial_ne_zero])]
      rw [mul_comm]
      exact hcast
    rw [hdesc]
    have hlc : lcoeff (n - i - 1) = iteratedDeriv (n - i) hLi 1 / ((n - i) ! : ℂ) := by
      rw [hLi_iteratedDeriv_div_factorial (j := n - i) (by omega)]
    rw [hlc]
    have hf1 : (n ! : ℂ) ≠ 0 := by simp [Nat.factorial_ne_zero]
    have hf2 : ((n - i) ! : ℂ) ≠ 0 := by simp [Nat.factorial_ne_zero]
    field_simp [hf1, hf2]
  rw [Finset.sum_div]
  rw [Finset.sum_congr rfl hterm]
  have hre : (∑ i ∈ Finset.range n, (n.choose i : ℂ) * lcoeff (n - i - 1)) =
      ∑ j ∈ Finset.Icc 1 n, (n.choose j : ℂ) * lcoeff (j - 1) := by
    apply Finset.sum_bij (fun i _ => n - i)
    · intro i hi
      rw [Finset.mem_range] at hi
      rw [Finset.mem_Icc]
      omega
    · intro a₁ ha₁ a₂ ha₂ h
      rw [Finset.mem_range] at ha₁ ha₂
      omega
    · intro j hj
      rw [Finset.mem_Icc] at hj
      exact ⟨n - j, by rw [Finset.mem_range]; omega, by omega⟩
    · intro i hi
      rw [Finset.mem_range] at hi
      have e2 : n.choose (n - i) = n.choose i := Nat.choose_symm (by omega)
      rw [e2]
  exact hre

end NguyenRH1