LiZetaCoeff.lean

Declarations

Source

/-
NguyenRH1/LiZetaCoeff.lean — tier ii′ sub-stage ii′-3a, piece (B)
(D-066 §2): the ζ-piece of the (4.10) coefficient split.

The meromorphic function 1/s + ζ′/ζ(1+s) is analytic at s = 0 (the pole
cancels: −ζ′/ζ(1+s) = 1/s + Σ_j c_j s^j), and its j-th Taylor coefficient
at 0 is −c_j = −lcoeff j. We package this as the analytic function

  hLiExt s := (1 − hLi (1+s)) / s   [extended by −deriv hLi 1 at 0]

(since hLi(1+s) = s·(−ζ′/ζ(1+s)) punctured near 0 by `hLi_eq_near_one`,
hLiExt = 1/s + ζ′/ζ(1+s) on a punctured neighbourhood —
`hLiExt_eq_near_zero`) and prove

  **iteratedDeriv j hLiExt 0 = −(j!)·lcoeff j**

— by the exact function identity s·hLiExt s = 1 − hLi(1+s)
(`hLiExt_mul_id`), the Leibniz collapse (iteratedDeriv_mul with the
identity factor killing all but the i = 1 term), and the comp bridge
iteratedDeriv (j+1) (hLi(1+·)) 0 = iteratedDeriv (j+1) hLi 1.

Archive references: D-066 (route β4, piece B), D-064, journal-019.
-/
import Mathlib
import NguyenRH1.LiResidue

open Zeta23 Complex Filter Topology
open scoped Nat

noncomputable section

namespace NguyenRH1

/-! ## 1. The limit value at 0 -/

/-- The slope limit: (1 − hLi(1+s))/s → −deriv hLi 1 as s → 0, s ≠ 0. -/
lemma hLiExt_tendsto :
    Tendsto (fun s : ℂ => (1 - hLi (1 + s)) / s) (𝓝[≠] 0) (𝓝 (-deriv hLi 1)) := by
  have hd : HasDerivAt (fun s : ℂ => hLi (1 + s)) (deriv hLi 1) 0 := by
    have h1 : HasDerivAt hLi (deriv hLi 1) (1 + (0 : ℂ)) := by
      simpa using hLi_analyticAt_one.differentiableAt.hasDerivAt
    have h2 : HasDerivAt (fun s : ℂ => 1 + s) 1 0 := by
      simpa using (hasDerivAt_id (0 : ℂ)).const_add 1
    have h3 := h1.comp 0 h2
    rw [mul_one] at h3
    have h4 : (hLi ∘ fun s : ℂ => 1 + s) = fun s : ℂ => hLi (1 + s) := rfl
    rw [h4] at h3
    exact h3
  have hslope : Tendsto (fun s : ℂ => (hLi (1 + s) - hLi 1) / s) (𝓝[≠] 0)
      (𝓝 (deriv hLi 1)) := by
    have h := hasDerivAt_iff_tendsto_slope.mp hd
    simpa [slope_fun_def_field] using h
  have hev : (fun s : ℂ => -((hLi (1 + s) - hLi 1) / s)) =ᶠ[𝓝[≠] 0]
      (fun s => (1 - hLi (1 + s)) / s) := by
    filter_upwards [self_mem_nhdsWithin] with s hs
    rw [hLi_one]
    ring
  exact hslope.neg.congr' hev

/-! ## 2. hLiExt: the analytic extension -/

/-- hLiExt s := (1 − hLi(1+s))/s, extended by −deriv hLi 1 at 0 — the
analytic-at-0 form of 1/s + ζ′/ζ(1+s) (`hLiExt_eq_near_zero`). -/
def hLiExt : ℂ → ℂ := Function.update (fun s => (1 - hLi (1 + s)) / s) 0 (-deriv hLi 1)

lemma hLiExt_zero : hLiExt 0 = -deriv hLi 1 := Function.update_self _ _ _

lemma hLiExt_of_ne {s : ℂ} (hs : s ≠ 0) : hLiExt s = (1 - hLi (1 + s)) / s :=
  Function.update_of_ne hs _ _

/-- hLiExt is analytic at 0 (removable singularity; the limit exists by
`hLiExt_tendsto`). Mirrors `zetaA_analyticAt_one`. -/
lemma hLiExt_analyticAt_zero : AnalyticAt ℂ hLiExt 0 := by
  have hT := hLiExt_tendsto
  rw [Metric.tendsto_nhdsWithin_nhds] at hT
  obtain ⟨δ, hδ0, hδ⟩ := hT 1 one_pos
  -- hLi is analytic on a ball around 1
  have hball : ∀ᶠ w in 𝓝 (1 : ℂ), AnalyticAt ℂ hLi w :=
    hLi_analyticAt_one.eventually_analyticAt
  rw [Metric.eventually_nhds_iff_ball] at hball
  obtain ⟨ε, hε0, hε⟩ := hball
  -- differentiability on a punctured ball around 0
  have hdiff : DifferentiableOn ℂ (fun s => (1 - hLi (1 + s)) / s)
      (Metric.ball 0 (min (δ / 2) ε) \ {0}) := by
    intro s hs
    have hs0 : s ≠ 0 := hs.2
    have hs1 : (1 + s) ∈ Metric.ball 1 ε := by
      have hds : dist s 0 < ε := lt_of_lt_of_le hs.1 (min_le_right _ _)
      rw [Metric.mem_ball, dist_eq_norm]
      have e : (1 + s) - 1 = s := by ring
      rw [e, ← dist_zero_right]
      exact hds
    have ha : AnalyticAt ℂ hLi (1 + s) := hε (1 + s) hs1
    have hnum : DifferentiableAt ℂ (fun s : ℂ => 1 - hLi (1 + s)) s := by
      have hcomp : AnalyticAt ℂ hLi (1 + s) := ha
      have hpath : AnalyticAt ℂ (fun s : ℂ => 1 + s) s :=
        analyticAt_const.add analyticAt_id
      have h := hcomp.comp hpath
      have heq : (hLi ∘ fun s : ℂ => 1 + s) = fun s : ℂ => hLi (1 + s) := rfl
      rw [heq] at h
      exact analyticAt_const.sub h |>.differentiableAt
    exact hnum.div (differentiableAt_id) hs0 |>.differentiableWithinAt
  -- boundedness on the punctured ball
  have hbd : BddAbove ((fun s => ‖(1 - hLi (1 + s)) / s‖) ''
      (Metric.ball 0 (min (δ / 2) ε) \ {0})) := by
    refine ⟨‖deriv hLi 1‖ + 1, ?_⟩
    rintro _ ⟨s, hs, rfl⟩
    have hs0 : s ≠ 0 := hs.2
    have hds : dist s 0 < δ := by
      have := hs.1
      rw [Metric.mem_ball] at this
      have h2 : dist s 0 < min (δ / 2) ε := this
      have h3 : min (δ / 2) ε ≤ δ / 2 := min_le_left _ _
      linarith [h2, h3, hδ0]
    have h1 := hδ (Set.mem_compl_singleton_iff.mpr hs0) hds
    rw [dist_eq_norm] at h1
    have h2 : ‖(1 - hLi (1 + s)) / s‖ ≤ ‖(1 - hLi (1 + s)) / s - (-deriv hLi 1)‖ +
        ‖(-deriv hLi 1 : ℂ)‖ := by
      nth_rewrite 1 [show (1 - hLi (1 + s)) / s =
        ((1 - hLi (1 + s)) / s - (-deriv hLi 1)) + (-deriv hLi 1) from by ring]
      exact norm_add_le _ _
    rw [norm_neg] at h2
    linarith [h1, h2]
  have h := differentiableOn_update_limUnder_of_bddAbove
    (Metric.ball_mem_nhds 0 (by positivity : (0 : ℝ) < min (δ / 2) ε)) hdiff hbd
  have hlim : limUnder (𝓝[≠] (0 : ℂ)) (fun s => (1 - hLi (1 + s)) / s) = -deriv hLi 1 :=
    hLiExt_tendsto.limUnder_eq
  rw [hlim] at h
  have han := h.analyticOnNhd Metric.isOpen_ball
  exact han 0 (Metric.mem_ball_self (by positivity : (0 : ℝ) < min (δ / 2) ε))

/-! ## 3. The function identity and the coefficient reading -/

/-- The exact global identity s·hLiExt s = 1 − hLi(1+s). -/
lemma hLiExt_mul_id : (fun s : ℂ => s) * hLiExt = fun s => 1 - hLi (1 + s) := by
  funext s
  by_cases hs : s = 0
  · subst hs
    show (0 : ℂ) * hLiExt 0 = 1 - hLi (1 + 0)
    simp only [add_zero]
    rw [hLiExt_zero, hLi_one]
    simp
  · show s * hLiExt s = 1 - hLi (1 + s)
    rw [hLiExt_of_ne hs, mul_div_assoc', mul_div_cancel_left₀ _ hs]

/-- The comp bridge: iterated derivatives of hLi(1+·) at 0 = those of hLi at 1. -/
lemma iteratedDeriv_hLi_one_add (m : ℕ) :
    iteratedDeriv m (fun s : ℂ => hLi (1 + s)) 0 = iteratedDeriv m hLi 1 := by
  have e := congr_fun (iteratedDeriv_comp_sub_const m hLi (-1 : ℂ)) 0
  have e2 : (fun z : ℂ => hLi (z - -1)) = fun s : ℂ => hLi (1 + s) := by
    funext z
    congr 1
    ring
  rw [e2] at e
  simpa using e

/-- **Piece (B)** (D-066 §2): the Taylor coefficients of hLiExt at 0 are
−j!·lcoeff j — i.e. 1/s + ζ′/ζ(1+s) has j-th coefficient −c_j. -/
theorem iteratedDeriv_hLiExt (j : ℕ) :
    iteratedDeriv j hLiExt 0 = -(Nat.factorial j : ℂ) * lcoeff j := by
  have hcid : ContDiffAt ℂ (j + 1) (fun s : ℂ => s) 0 := contDiff_id.contDiffAt
  have hcE : ContDiffAt ℂ (j + 1) hLiExt 0 := hLiExt_analyticAt_zero.contDiffAt
  have h1 : iteratedDeriv (j + 1) ((fun s : ℂ => s) * hLiExt) 0 =
      ∑ i ∈ Finset.range (j + 2), ((j + 1).choose i : ℂ) * iteratedDeriv i (fun s : ℂ => s) 0 *
        iteratedDeriv (j + 1 - i) hLiExt 0 := iteratedDeriv_mul hcid hcE
  -- LHS via the function identity
  have hLHS : iteratedDeriv (j + 1) ((fun s : ℂ => s) * hLiExt) 0 =
      -iteratedDeriv (j + 1) hLi 1 := by
    rw [hLiExt_mul_id]
    have hconst : ContDiffAt ℂ (j + 1) (fun s : ℂ => (1 : ℂ)) 0 := contDiff_const.contDiffAt
    have hcompC : ContDiffAt ℂ (j + 1) (fun s : ℂ => hLi (1 + s)) 0 := by
      have h1a : AnalyticAt ℂ hLi (1 + (0 : ℂ)) := by simpa using hLi_analyticAt_one
      have h2a : AnalyticAt ℂ (fun s : ℂ => 1 + s) 0 := analyticAt_const.add analyticAt_id
      have h3 := h1a.comp h2a
      have heq : (hLi ∘ fun s : ℂ => 1 + s) = fun s : ℂ => hLi (1 + s) := rfl
      rw [heq] at h3
      exact h3.contDiffAt
    rw [show (fun s : ℂ => 1 - hLi (1 + s)) = (fun s => (1 : ℂ)) - (fun s => hLi (1 + s))
      from by funext s; simp [Pi.sub_apply]]
    rw [iteratedDeriv_sub hconst hcompC]
    have hconst' : iteratedDeriv (j + 1) (fun s : ℂ => (1 : ℂ)) 0 = 0 := by
      rw [iteratedDeriv_const, if_neg (by omega)]
    rw [hconst', zero_sub, iteratedDeriv_hLi_one_add]
  -- RHS: the Leibniz sum collapses to the i = 1 term
  have hid : ∀ i : ℕ, iteratedDeriv i (fun s : ℂ => s) 0 = if i = 1 then 1 else 0 := by
    intro i
    rcases i with _ | _ | i
    · simp [iteratedDeriv_zero]
    · simp [iteratedDeriv_one, deriv_id'']
    · have hd : deriv (fun s : ℂ => s) = fun _ => (1 : ℂ) := deriv_id''
      have hne1 : ¬(i + 1 = 0) := Nat.succ_ne_zero i
      have hne2 : ¬(i + 2 = 1) := by omega
      have h2 : iteratedDeriv (i + 2) (fun s : ℂ => s) 0 = 0 := by
        rw [iteratedDeriv_succ', hd, iteratedDeriv_const, if_neg hne1]
      rw [h2, if_neg hne2]
  have hsum : iteratedDeriv (j + 1) ((fun s : ℂ => s) * hLiExt) 0 =
      (j + 1 : ℂ) * iteratedDeriv j hLiExt 0 := by
    rw [h1]
    rw [Finset.sum_eq_single 1]
    · rw [hid 1, if_pos rfl]
      simp [Nat.choose_one_right]
    · intro i hi hi1
      rw [Finset.mem_range] at hi
      rw [hid i, if_neg hi1]
      simp
    · intro h1'
      rw [Finset.mem_range] at h1'
      exact (h1' (by omega)).elim
  -- combine
  rw [hsum] at hLHS
  -- (j+1)·iteratedDeriv j hLiExt 0 = −iteratedDeriv (j+1) hLi 1
  have hlc : iteratedDeriv (j + 1) hLi 1 = ((j + 1)! : ℂ) * lcoeff j := by
    rw [lcoeff]
    have hf : ((j + 1)! : ℂ) ≠ 0 := by simp [Nat.factorial_ne_zero]
    rw [show ((j + 1) ! : ℂ) = (Nat.factorial (j + 1) : ℂ) from rfl]
    field_simp [hf]
  rw [hlc] at hLHS
  have hj1 : (j : ℂ) + 1 ≠ 0 := by
    have h : ((j + 1 : ℕ) : ℂ) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.succ_ne_zero j)
    rwa [Nat.cast_add_one] at h
  have hjs : ((j + 1)! : ℂ) = (j + 1) * (j ! : ℂ) := by
    rw [Nat.factorial_succ]
    simp [Nat.cast_mul]
  rw [hjs] at hLHS
  -- (j+1)·X = −(j+1)·j!·lcoeff j ⟹ X = −j!·lcoeff j
  have hcancel : (j + 1 : ℂ) * iteratedDeriv j hLiExt 0 =
      (j + 1 : ℂ) * (-(Nat.factorial j : ℂ) * lcoeff j) := by
    rw [hLHS]
    ring
  exact mul_left_cancel₀ hj1 hcancel

/-! ## 4. The reading as 1/s + ζ′/ζ(1+s) -/

/-- On a punctured neighbourhood of 0, hLiExt s = 1/s + ζ′/ζ(1+s). -/
lemma hLiExt_eq_near_zero :
    ∀ᶠ s in 𝓝[≠] (0 : ℂ),
      hLiExt s = 1 / s + deriv riemannZeta (1 + s) / riemannZeta (1 + s) := by
  -- ζ(1+s) ≠ 0 on a punctured nhd of 0 (transport of residue_one.eventually_ne)
  have hne1 : ∀ᶠ w in 𝓝[≠] (1 : ℂ), riemannZeta w ≠ 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
  have hmap : Tendsto (fun s : ℂ => 1 + s) (𝓝[≠] (0 : ℂ)) (𝓝[≠] (1 : ℂ)) := by
    apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
    · have hc : ContinuousAt (fun s : ℂ => 1 + s) 0 :=
        continuousAt_const.add continuousAt_id
      have h1 : Tendsto (fun s : ℂ => 1 + s) (𝓝 0) (𝓝 (1 : ℂ)) := by
        simpa using hc.tendsto
      exact h1.mono_left nhdsWithin_le_nhds
    · filter_upwards [self_mem_nhdsWithin] with s hs
      intro hcontra
      exact hs (add_eq_left.mp hcontra)
  have hne : ∀ᶠ s in 𝓝[≠] (0 : ℂ), riemannZeta (1 + s) ≠ 0 := hmap.eventually hne1
  filter_upwards [hne, self_mem_nhdsWithin] with s hs0 hs
  have hs1 : (1 : ℂ) + s ≠ 1 := by
    intro h
    exact hs (add_eq_left.mp h)
  rw [hLiExt_of_ne hs, hLi_eq_of_ne hs1 hs0]
  have e : ((1 : ℂ) + s) - 1 = s := by ring
  rw [e]
  rw [show (1 : ℂ) - s * (-deriv riemannZeta (1 + s) / riemannZeta (1 + s)) =
    1 + s * (deriv riemannZeta (1 + s) / riemannZeta (1 + s)) from by ring]
  rw [add_div, mul_div_cancel_left₀ _ hs]