An introduction to p-adic L-functions — Lean blueprint

7.3. Computing the numerator🔗

It remains to evaluate \int_{\Zpx} x^{-1}\cdot\mu_a. As in the chapter on the value at s=1, the difficulty is that multiplication by x^{-1} is not defined on measures on \Zp; on Mahler transforms this is the indeterminacy in inverting the operator \dpartial = (1+T)\tfrac{d}{dT}. Recall that the Mahler transform of \mu_a is F_a(T) = \tfrac{1}{T} - \tfrac{a}{(1+T)^a-1}. We seek a primitive \Fat with \dpartial\Fat = F_a, lying in the ring \Rp of power series \sum a_n T^n with \abs{a_n}r^n \to 0 for every 0\le r<1.

Definition7.3.1
uses 0
Used by 3
Reverse dependency previews
Preview
Lemma 7.3.2
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N

Define the primitive of F_a by \Fat(T) := \log\!\left(\frac{T}{1+T}\cdot\frac{(1+T)^a}{(1+T)^a-1}\right) = \log\!\left(\frac{T}{(1+T)^a-1}\cdot (1+T)^{a-1}\right).

The Lean definition realises the second expression through the unit factorisation (1+T)^a-1 = aT\,u_a(T) (with u_a of constant term 1): \Fat = -\logp(a) - \log u_a + (a-1)\log(1+T), each summand a legal formal composition over a complete normed \Qp-field K.

Lean code for Definition7.3.1●2 definitions
  • defdefined in PadicLFunctions/ResidueZeta.lean
    complete
    def PadicLFunctions.FtildeA.{u_1} (p : ℕ) [hp : Fact (Nat.Prime p)]
  (K : Type u_1) [NormedField K] [NormedAlgebra ℚ_[p] K] (a : ℕ) :
  PowerSeries K
    def PadicLFunctions.FtildeA.{u_1} (p : ℕ)
  [hp : Fact (Nat.Prime p)] (K : Type u_1)
  [NormedField K] [NormedAlgebra ℚ_[p] K]
  (a : ℕ) : PowerSeries K
    R7.4b: RJW's antiderivative `F̃_a = log(T/(1+T) · (1+T)^a/((1+T)^a−1))`
(TeX 2268), realised through the factorisation
`F̃_a = −log_p(a) − log(u_a) + (a−1)·log(1+T)` (TeX eq:tilde F_a 2 +
eq:F_a tilde): the formal compositions are legal (`u_a − 1` has constant
term `0`).
  • defdefined in PadicLFunctions/ResidueZeta.lean
    complete
    def PadicLFunctions.uA.{u_1} (K : Type u_1) [NormedField K] (a : ℕ) :
  PowerSeries K
    def PadicLFunctions.uA.{u_1} (K : Type u_1)
  [NormedField K] (a : ℕ) : PowerSeries K
    R7.4a: the unit factor `u_a` of `(1+T)^a − 1 = a·T·u_a`
(`u_a = Σ_n a⁻¹·C(a, n+1)·Tⁿ`, constant term `1`; TeX 2296–2300).
Lemma7.3.2
Statement uses 2
Statement dependency previews
Preview
Definition 3.4.3
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 1✓L∃∀N

Formally, \dpartial \Fat(T) = F_a(T). This depends on Definition 7.3.1 and Definition 3.4.3.

The Lean statement carries the (implicit in the notes' §4 setting) hypothesis p\nmid a: the project's F_a is the junk value 0 when p \mid a (its denominator-inverse degenerates), while \dpartial\Fat is never zero.

Lean code for Lemma7.3.2●1 theorem
  • theoremdefined in PadicLFunctions/ResidueZeta.lean
    complete
    theorem PadicLFunctions.one_add_mul_derivative_FtildeA.{u_1} (p : ℕ)
  [hp : Fact (Nat.Prime p)] (K : Type u_1) [NormedField K]
  [NormedAlgebra ℚ_[p] K] [CharZero K] {a : ℕ} (ha : ¬p ∣ a)
  (ha0 : a ≠ 0) :
  (1 + PowerSeries.X) * (PadicLFunctions.FtildeA p K a).derivativeFun =
    (PowerSeries.map ((algebraMap ℚ_[p] K).comp PadicInt.Coe.ringHom))
      (PadicMeasure.Fa p a)
    theorem PadicLFunctions.one_add_mul_derivative_FtildeA.{u_1}
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (K : Type u_1) [NormedField K]
  [NormedAlgebra ℚ_[p] K] [CharZero K]
  {a : ℕ} (ha : ¬p ∣ a) (ha0 : a ≠ 0) :
  (1 + PowerSeries.X) *
      (PadicLFunctions.FtildeA p K
          a).derivativeFun =
    (PowerSeries.map
        ((algebraMap ℚ_[p] K).comp
          PadicInt.Coe.ringHom))
      (PadicMeasure.Fa p a)
    R7.4d (RJW Lemma 7.3, TeX 2271–2279): `∂F̃_a = F_a` formally.

Statement note (T704): hypothesis `¬p∣a` added — `Fa p a` is the junk value `0`
when `p ∣ a` (`Ring.inverse` of a non-unit) while `∂F̃_a ≠ 0`; RJW carries
`p ∤ a` from §4.1 throughout.
Proof for Lemma 7.3.2
uses 0

The operator \dpartial = (1+T)\tfrac{d}{dT} satisfies the chain rule, so for any unit power series u one has \dpartial\log u = (1+T)u'/u. Applied to u = \tfrac{(1+T)^a-1}{(1+T)^a}, whose logarithmic derivative computes to (1+T)\big[\tfrac{a(1+T)^{a-1}}{(1+T)^a-1} - \tfrac{a(1+T)^{a-1}}{(1+T)^a}\big], this collapses (after clearing (1+T)^a) to \dpartial\log\big(\tfrac{(1+T)^a-1}{(1+T)^a}\big) = \tfrac{a}{(1+T)^a-1}. Specialising to a=1 gives \dpartial\log\big(\tfrac{T}{1+T}\big) = \tfrac1T. Since \Fat = \log\big(\tfrac{T}{1+T}\big) - \log\big(\tfrac{(1+T)^a-1}{(1+T)^a}\big), linearity of \dpartial yields \dpartial\Fat = \tfrac1T - \tfrac{a}{(1+T)^a-1} = F_a(T), the Mahler transform of \mu_a.

Lemma7.3.3
Statement uses 2
Statement dependency previews
Preview
Definition 3.4.3
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
Used by 2
Reverse dependency previews
Preview
Lemma 7.3.4
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
XL∃∀N

We have \Fat(T) \in \Rp, so that \Fat corresponds under the Mahler correspondence to a locally analytic distribution. This depends on Definition 7.3.1 and Definition 3.4.3.

Not formalised as stated (RJW Lemma 7.4): the formalisation follows a distribution-free route (decomposition R7, replan 1) that never constructs \Rp or the locally analytic distribution \widetilde\mu_a. The analytic content actually used — the coefficients of \Fat grow at most linearly, so its evaluation series converges on the open unit disc — is proved directly (the norm_coeff_FtildeA_le/summable_seriesEval_FtildeA layer in ResidueZeta.lean), and the constant-of-integration argument runs in \ker\psi exactly as in the value-at-s=1 chapter.

Proof for Lemma 7.3.3
uses 0

Write (1+T)^a-1 = aT\,(1+Tg(T)) with g(T) = \sum_{n\ge 2} a^{-1}\binom{a}{n}T^{n-2}, so that, as in the construction of \mu_a, \tfrac{1}{(1+T)^a-1} = \tfrac{1}{aT}(1+Th(T)) with h(T)\in\Zp[[T]]. Hence \tfrac{T}{(1+T)^a-1} = a^{-1}(1+Th(T)), and \log\!\left(\frac{T}{(1+T)^a-1}\right) = -\logp(a) + \sum_{n\ge 1}\frac{(-1)^{n+1}}{n}T^n h(T)^n. The coefficients here grow only logarithmically in n (the 1/n is offset by \val(n)), so this series lies in \Rp. Likewise (1+T)^{a-1} = 1 + T\sum_{n\ge1}\binom{a-1}{n}T^{n-1} has a well-defined logarithm in \Rp. Adding the two elements of \Rp yields \Fat \in \Rp.

With \Fat \in \Rp in hand we may attach to it a locally analytic distribution \widetilde\mu_a (the one whose Mahler transform is \Fat), and the relation \dpartial\Fat = F_a says precisely that x\,\widetilde\mu_a = \mu_a. This is the device that makes sense of the otherwise ill-defined product x^{-1}\mu_a.

Lemma7.3.4
Statement uses 4
Statement dependency previews
Preview
Definition 3.7.3
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
Used by 2
Reverse dependency previews
Preview
Theorem 7.1.1
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N

The numerator of the residue formula is the value at 0 of the restriction of \Fat to \Zpx: \int_{\Zpx} x^{-1}\cdot\mu_a = \big((1-\varphi\circ\psi)\Fat\big)(0), where \varphi\circ\psi acts on power series by \varphi\circ\psi(F)(T) = \tfrac1p\sum_{\xi\in\mu_p} F((1+T)\xi - 1). This depends on Lemma 7.3.2, Lemma 7.3.3, Definition 3.7.3 and Theorem 6.1.1.

Distribution-free realisation: instead of \widetilde\mu_a, the formalisation works with the genuine measure \rho_a = x^{-1}\Res_{\Zpx}(\mu_a) (the canonical numerator of \zp), shows \psi(\rho_a)=0 and \dpartial\sA_{\rho_a} = \sA_{\Res_{\Zpx}\mu_a}, and pins the constant of integration by evaluating at the p-th roots of unity: the displayed identity appears p-scaled as p\,\sA_{\rho_a}(0) = p\,\Fat(0) - \sum_{\xi\in\mu_p}\Fat(\xi-1), with the left side equal to p\int_{\Zpx}x^{-1}\mu_a.

Lean code for Lemma7.3.4●3 theorems
  • theoremdefined in PadicLFunctions/ResidueZeta.lean
    complete
    theorem PadicLFunctions.psi_rhoA.{u_1} (p : ℕ) [hp : Fact (Nat.Prime p)]
  (K : Type u_1) [NormedField K] [NormedAlgebra ℚ_[p] K]
  [IsUltrametricDist K] [CompleteSpace K] (a : ℕ) :
  PadicLFunctions.MeasureR.psi p K (PadicLFunctions.rhoA p K a) = 0
    theorem PadicLFunctions.psi_rhoA.{u_1} (p : ℕ)
  [hp : Fact (Nat.Prime p)] (K : Type u_1)
  [NormedField K] [NormedAlgebra ℚ_[p] K]
  [IsUltrametricDist K] [CompleteSpace K]
  (a : ℕ) :
  PadicLFunctions.MeasureR.psi p K
      (PadicLFunctions.rhoA p K a) =
    0
    R7.5b: `ρ_a` is supported on the units.
  • theoremdefined in PadicLFunctions/ResidueZeta.lean
    complete
    theorem PadicLFunctions.one_add_mul_derivative_mahlerK_rhoA.{u_1} (p : ℕ)
  [hp : Fact (Nat.Prime p)] (K : Type u_1) [NormedField K]
  [NormedAlgebra ℚ_[p] K] [IsUltrametricDist K] [CompleteSpace K]
  (a : ℕ) :
  (1 + PowerSeries.X) *
      (PadicLFunctions.mahlerK p K
          (PadicLFunctions.rhoA p K a)).derivativeFun =
    PadicLFunctions.mahlerK p K
      (PadicLFunctions.MeasureR.res p K ⋯
        ((PadicLFunctions.MeasureR.baseChange p K)
          (PadicMeasure.muA p a)))
    theorem PadicLFunctions.one_add_mul_derivative_mahlerK_rhoA.{u_1}
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (K : Type u_1) [NormedField K]
  [NormedAlgebra ℚ_[p] K]
  [IsUltrametricDist K] [CompleteSpace K]
  (a : ℕ) :
  (1 + PowerSeries.X) *
      (PadicLFunctions.mahlerK p K
          (PadicLFunctions.rhoA p K
            a)).derivativeFun =
    PadicLFunctions.mahlerK p K
      (PadicLFunctions.MeasureR.res p K ⋯
        ((PadicLFunctions.MeasureR.baseChange
            p K)
          (PadicMeasure.muA p a)))
    R7.5c: multiplication by `x` recovers `Res_{ℤ_p^×}(μ_a)` —
`∂𝓐(ρ_a) = 𝓐(Res_{units}(μ_a))` over `K` (Lemma 6.3's pattern, T614).
  • theoremdefined in PadicLFunctions/ResidueZeta.lean
    complete
    theorem PadicLFunctions.p_mul_constantCoeff_mahlerK_rhoA.{u_1} (p : ℕ)
  [hp : Fact (Nat.Prime p)] (K : Type u_1) [NormedField K]
  [NormedAlgebra ℚ_[p] K] [IsUltrametricDist K] [CompleteSpace K]
  [CharZero K] {a : ℕ} (ha : ¬p ∣ a) (ha0 : a ≠ 0) {ξ : K}
  (hξ : IsPrimitiveRoot ξ p) :
  ↑p *
      PowerSeries.constantCoeff
        (PadicLFunctions.mahlerK p K (PadicLFunctions.rhoA p K a)) =
    ↑p * PowerSeries.constantCoeff (PadicLFunctions.FtildeA p K a) -
      ∑ i,
        PadicLFunctions.seriesEval (PadicLFunctions.FtildeA p K a)
          (ξ ^ ↑i - 1)
    theorem PadicLFunctions.p_mul_constantCoeff_mahlerK_rhoA.{u_1}
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (K : Type u_1) [NormedField K]
  [NormedAlgebra ℚ_[p] K]
  [IsUltrametricDist K] [CompleteSpace K]
  [CharZero K] {a : ℕ} (ha : ¬p ∣ a)
  (ha0 : a ≠ 0) {ξ : K}
  (hξ : IsPrimitiveRoot ξ p) :
  ↑p *
      PowerSeries.constantCoeff
        (PadicLFunctions.mahlerK p K
          (PadicLFunctions.rhoA p K a)) =
    ↑p *
        PowerSeries.constantCoeff
          (PadicLFunctions.FtildeA p K
            a) -
      ∑ i,
        PadicLFunctions.seriesEval
          (PadicLFunctions.FtildeA p K a)
          (ξ ^ ↑i - 1)
    R7.6a (the c₀-pin, T615-pattern — no Gauss clearing this time):
`p·𝓐(ρ_a)(0) = p·F̃_a(0) − Σ_{i<p} F̃_a(ξ^i − 1)`.
Proof for Lemma 7.3.4
uses 0

On \Zpx the function x is invertible, so x\,\widetilde\mu_a = \mu_a gives \Res_{\Zpx}(\widetilde\mu_a) = x^{-1}\Res_{\Zpx}(\mu_a) and hence \int_{\Zpx} x^{-1}\cdot\mu_a = \int_{\Zpx}\widetilde\mu_a. The right-hand side is the value at the trivial character of the restricted distribution, which on Mahler transforms is read off as the constant term: writing \Res_{\Zpx} = 1-\varphi\circ\psi (the complement of restriction to p\Zp, whose Mahler transform is \varphi\circ\psi\Fat), one gets \int_{\Zpx}\widetilde\mu_a = \big((1-\varphi\circ\psi)\Fat\big)(0). This is the exact analogue, with \Fat in place of \widetilde F_\theta, of the computation that produced the value at s=1. This reduces the residue computation to a single evaluation.

Lemma7.3.5
Statement uses 3
Statement dependency previews
Preview
Definition 7.3.1
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 1✓L∃∀N

We have \big((1-\varphi\circ\psi)\Fat\big)(0) = -(1-p^{-1})\,\logp(a). This depends on Definition 7.3.1 and Lemma 7.3.3.

Formalised as constantCoeff_mahlerK_rhoA (with the left side realised as \sA_{\rho_a}(0), see Lemma 7.3.4) from the two evaluations constantCoeff_FtildeA (\Fat(0) = -\logp a) and sum_seriesEval_FtildeA (\sum_{\xi\in\mu_p}\Fat(\xi-1) = -\logp a); the \mu_p-collapse is run by a product identity (the multiset \set{\xi^a} equals \mu_p, so \prod_{\xi\neq 1} u_a(\xi-1) = a^{-(p-1)}) together with Fermat's a^{p-1}\equiv 1 \bmod p, in a complete algebraically closed field K=\CC_p containing \mu_p; zetaNum_one is the descent of the resulting mass to \Qp along the injective structure map.

Lean code for Lemma7.3.5●4 theorems
  • theoremdefined in PadicLFunctions/ResidueZeta.lean
    complete
    theorem PadicLFunctions.constantCoeff_FtildeA.{u_1} (p : ℕ)
  [hp : Fact (Nat.Prime p)] (K : Type u_1) [NormedField K]
  [NormedAlgebra ℚ_[p] K] [CharZero K] {a : ℕ} (ha0 : a ≠ 0) :
  PowerSeries.constantCoeff (PadicLFunctions.FtildeA p K a) =
    -PadicLFunctions.extLog p ↑a
    theorem PadicLFunctions.constantCoeff_FtildeA.{u_1}
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (K : Type u_1) [NormedField K]
  [NormedAlgebra ℚ_[p] K] [CharZero K]
  {a : ℕ} (ha0 : a ≠ 0) :
  PowerSeries.constantCoeff
      (PadicLFunctions.FtildeA p K a) =
    -PadicLFunctions.extLog p ↑a
    R7.4c: the constant coefficient is `−log_p(a)` (TeX eq:F_a(0)).

Statement note (T704): `a ≠ 0` added — `uA 0 = 0` makes the formal composition
junk (`HasSubst` fails at constant coefficient `−1`).
  • theoremdefined in PadicLFunctions/ResidueZeta.lean
    complete
    theorem PadicLFunctions.sum_seriesEval_FtildeA.{u_1} (p : ℕ)
  [hp : Fact (Nat.Prime p)] (K : Type u_1) [NormedField K]
  [NormedAlgebra ℚ_[p] K] [IsUltrametricDist K] [CompleteSpace K]
  [CharZero K] (hp2 : p ≠ 2) {a : ℕ} (ha : ¬p ∣ a) (ha0 : a ≠ 0) {ξ : K}
  (hξ : IsPrimitiveRoot ξ p) :
  ∑ i,
      PadicLFunctions.seriesEval (PadicLFunctions.FtildeA p K a)
        (ξ ^ ↑i - 1) =
    -PadicLFunctions.extLog p ↑a
    theorem PadicLFunctions.sum_seriesEval_FtildeA.{u_1}
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (K : Type u_1) [NormedField K]
  [NormedAlgebra ℚ_[p] K]
  [IsUltrametricDist K] [CompleteSpace K]
  [CharZero K] (hp2 : p ≠ 2) {a : ℕ}
  (ha : ¬p ∣ a) (ha0 : a ≠ 0) {ξ : K}
  (hξ : IsPrimitiveRoot ξ p) :
  ∑ i,
      PadicLFunctions.seriesEval
        (PadicLFunctions.FtildeA p K a)
        (ξ ^ ↑i - 1) =
    -PadicLFunctions.extLog p ↑a
    R7.6b (RJW Lemma 7.5's trace, TeX 2330–2349): the evaluated `μ_p`-sum
collapses — `Σ_{i<p} F̃_a(ξ^i − 1) = −log_p(a)` (the `{ξ^a} = μ_p`
reindex for `p ∤ a` and `Π_ξ(Xξ−1) = X^p−1`).
  • theoremdefined in PadicLFunctions/ResidueZeta.lean
    complete
    theorem PadicLFunctions.constantCoeff_mahlerK_rhoA.{u_1} (p : ℕ)
  [hp : Fact (Nat.Prime p)] (K : Type u_1) [NormedField K]
  [NormedAlgebra ℚ_[p] K] [IsUltrametricDist K] [CompleteSpace K]
  [CharZero K] (hp2 : p ≠ 2) {a : ℕ} (ha : ¬p ∣ a) (ha0 : a ≠ 0) {ξ : K}
  (hξ : IsPrimitiveRoot ξ p) :
  PowerSeries.constantCoeff
      (PadicLFunctions.mahlerK p K (PadicLFunctions.rhoA p K a)) =
    -(1 - (↑p)⁻¹) * PadicLFunctions.extLog p ↑a
    theorem PadicLFunctions.constantCoeff_mahlerK_rhoA.{u_1}
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (K : Type u_1) [NormedField K]
  [NormedAlgebra ℚ_[p] K]
  [IsUltrametricDist K] [CompleteSpace K]
  [CharZero K] (hp2 : p ≠ 2) {a : ℕ}
  (ha : ¬p ∣ a) (ha0 : a ≠ 0) {ξ : K}
  (hξ : IsPrimitiveRoot ξ p) :
  PowerSeries.constantCoeff
      (PadicLFunctions.mahlerK p K
        (PadicLFunctions.rhoA p K a)) =
    -(1 - (↑p)⁻¹) *
      PadicLFunctions.extLog p ↑a
    R7.6c (RJW Lemma 7.5, TeX 2320): the mass of `x⁻¹·Res(μ_a)` —
`((1−φψ)F̃_a)(0) = −(1−p⁻¹)·log_p(a)`, in the c₀-design form.
  • theoremdefined in PadicLFunctions/ResidueZeta.lean
    complete
    theorem PadicLFunctions.zetaNum_one (p : ℕ) [hp : Fact (Nat.Prime p)]
  (hp2 : p ≠ 2) {a : ℕ} (ha : ¬p ∣ a) (ha0 : a ≠ 0) :
  ↑((PadicMeasure.zetaNum p a) 1) =
    -(1 - (↑p)⁻¹) * PadicLFunctions.extLog p ↑a
    theorem PadicLFunctions.zetaNum_one (p : ℕ)
  [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2)
  {a : ℕ} (ha : ¬p ∣ a) (ha0 : a ≠ 0) :
  ↑((PadicMeasure.zetaNum p a) 1) =
    -(1 - (↑p)⁻¹) *
      PadicLFunctions.extLog p ↑a
    R7.7 (eq:zeta p residue 2 + Lemma 7.5, descended to `ℚ_p`): the total
mass of the §4 numerator measure —
`∫_{ℤ_p^×} x⁻¹·μ_a = −(1−p⁻¹)·log_p(a)` (computed in `ℂ_p` and pulled
back along the injective structure map).
Proof for Lemma 7.3.5
Proof uses 2
Proof dependency previews
Preview
Definition 7.3.1
Loading preview
Proof dependency preview content is loaded from the Blueprint HTML cache.

Value of \Fat(0). From the second expression in Definition 7.3.1, \Fat(0) = \log\big(\tfrac{T}{(1+T)^a-1}\big)\big|_{T=0} + \log((1+T)^{a-1})\big|_{T=0}; the first summand equals -\logp(a) by the expansion in Lemma 7.3.3 and the second is 0, so \Fat(0) = -\logp(a).

Value of (\varphi\circ\psi)\Fat(0). Summing the logarithm over \xi\in\mu_p turns the sum into the logarithm of a product, and \prod_{\xi\in\mu_p}(X\xi-1) = X^p-1 collapses each factor. Using that a is a topological generator (so \set{\xi^a:\xi\in\mu_p}=\mu_p) and \prod_{\xi\in\mu_p}\xi^{a-1}=1, (\varphi\circ\psi)\Fat(T) = \frac1p\log\!\left(\frac{(1+T)^p-1}{(1+T)^{ap}-1}\cdot (1+T)^{(a-1)p}\right). Writing (1+T)^p-1 = pT(1+Tj(T)) and \tfrac{1}{(1+T)^{ap}-1} = \tfrac{1}{apT}(1+Tk(T)) as before, the factors of pT cancel and the right-hand side at T=0 collapses to -p^{-1}\logp(a).

Conclusion. Subtracting the two evaluations, \big((1-\varphi\circ\psi)\Fat\big)(0) = \Fat(0) - (\varphi\circ\psi)\Fat(0) = -\logp(a) + p^{-1}\logp(a) = -(1-p^{-1})\,\logp(a), as claimed.

Combining the limit formula with the value of the numerator, the two occurrences of \logp(a) cancel and we obtain \lim_{s\to 1}(s-1)\,\zeta_{p,p-1}(s) = -\frac{-(1-p^{-1})\logp(a)}{\logp(a)} = 1 - p^{-1}, completing the proof of the residue theorem. The residue 1-p^{-1} is the precise p-adic shadow of the residue 1 of the complex \zeta at s=1: it is \zeta(s) with its Euler factor at p removed, evaluated at the pole.