7.1. The main theorem🔗

Theorem7.1.1

Statement uses 3

Statement dependency previews

Preview

Definition 4.3.2

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

used by 1✓L∃∀N

Let i \in \set{1, 2, \ldots, p-1}.

(i) If i \neq p-1, then \zpi is analytic at s=1.
(ii) The branch \zeta_{p,p-1} has a simple pole at s=1, with residue \lim_{s\to 1} (s-1)\,\zeta_{p,p-1}(s) = 1 - p^{-1}.

This rests on Definition 4.3.2, Lemma 7.2.2 and Lemma 7.3.5.

In the formalisation "analytic at s=1" is realised topologically: part (i) is ContinuousAt (zetaPBranch p hp2 i) 1 (the rigid-analytic structure is not formalised), and part (ii) is the topological limit Tendsto (fun s => (s-1)·ζ_{p,p-1}(s)) (nhdsWithin 1 {s ≠ 1}) (nhds (1-p⁻¹)).

Lean code for Theorem7.1.1●2 theorems

theoremdefined in PadicLFunctions/ResidueZeta.lean

complete

theorem PadicLFunctions.continuousAt_zetaPBranch (p : ℕ)
  [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) {i : ℕ} (hi0 : 0 < i)
  (hi : i < p - 1) :
  ContinuousAt (PadicLFunctions.zetaPBranch p hp2 i) 1

theorem PadicLFunctions.continuousAt_zetaPBranch
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (hp2 : p ≠ 2) {i : ℕ} (hi0 : 0 < i)
  (hi : i < p - 1) :
  ContinuousAt
    (PadicLFunctions.zetaPBranch p hp2 i)
    1

**RJW Theorem 7.1(i)** (TeX 2189–2190): for `0 < i < p−1` the branch
`ζ_{p,i}` is continuous ("analytic") at `s = 1` — indeed everywhere, but
we state the source's claim.

theoremdefined in PadicLFunctions/ResidueZeta.lean

complete

theorem PadicLFunctions.tendsto_sub_one_mul_zetaPBranch (p : ℕ)
  [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) :
  Filter.Tendsto
    (fun s ↦ (↑s - 1) * PadicLFunctions.zetaPBranch p hp2 (p - 1) s)
    (nhdsWithin 1 {s | s ≠ 1}) (nhds (1 - (↑p)⁻¹))

theorem PadicLFunctions.tendsto_sub_one_mul_zetaPBranch
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (hp2 : p ≠ 2) :
  Filter.Tendsto
    (fun s ↦
      (↑s - 1) *
        PadicLFunctions.zetaPBranch p hp2
          (p - 1) s)
    (nhdsWithin 1 {s | s ≠ 1})
    (nhds (1 - (↑p)⁻¹))

**RJW Theorem 7.1(ii)** (`thm:residue`, TeX 2191–2192): "The function
`ζ_{p,p−1}` has a simple pole at `s = 1` with residue `1 − p⁻¹`" — as the
topological limit `lim_{s→1, s≠1} (s−1)·ζ_{p,p−1}(s) = 1 − p⁻¹`.

Proof for Theorem 7.1.1

Proof uses 4

Proof dependency previews

Preview

Lemma 7.2.2

Loading preview

Proof dependency preview content is loaded from the Blueprint HTML cache.

Part (i) is immediate from Lemma 7.2.2(i): unwinding the definition of \zp as a pseudo-measure expresses \zpi(s) as a ratio whose denominator g_{a,i}(s) does not vanish at s=1 when i \neq p-1, so the expression is analytic there. For part (ii), the same unwinding gives, after passing to the limit using Corollary 7.2.3, \lim_{s\to 1}(s-1)\,\zeta_{p,p-1}(s) = -\frac{\int_{\Zpx} x^{-1}\cdot \mu_a}{\logp(a)}. By Lemma 7.3.4 the numerator \int_{\Zpx} x^{-1}\cdot\mu_a equals \big((1-\varphi\circ\psi)\Fat\big)(0), which by Lemma 7.3.5 is -(1-p^{-1})\logp(a); the two factors of \logp(a) then cancel to leave 1 - p^{-1}.