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

4.1. The auxiliary measure🔗

Recall the integral formula (s-1)\zeta(s) = L(f, s-1), with f(t) = t/(e^t-1), whose value at negative integers is \zeta(-k) = f^{(k)}(0) = (-1)^k B_{k+1}/(k+1). The factor s-1 smooths away the pole of \zeta at s=1. To remove this smoothing we fix an integer a coprime to p and replace f by \fa(t) = \frac{1}{e^t-1} - \frac{a}{e^{at}-1},$$ which is again \cC^\infty and rapidly decreasing, so its L-function L(\fa, s) is defined. The parameter a removes the factor s-1 at the cost of a different smoothing factor.

-- Deliberately unwired (§4 board, 2026-06-10): the Mellin/analytic-continuation half -- of this lemma is §2 material (deferred). The value formula f_a^{(k)}(0) = -- (−1)^k(1−a^{1+k})ζ(−k) — the part §4 consumes — is realised algebraically by -- PadicMeasure.muA_apply_powCM (wired at kl-mua-interpolation), with the rational -- ζ-values as zetaNeg (bridge to riemannZeta: zetaNeg_eq_riemannZeta).

Lemma4.1.1
Statement uses 2
Statement dependency previews
Preview
Definition 2.1.1
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 1XL∃∀N

With \fa as above, L(\fa, s) = (1 - a^{1-s})\,\zeta(s),$$ which extends analytically to all of \C, and the derivatives at 0 satisfy \fa^{(k)}(0) = (-1)^k\,(1 - a^{1+k})\,\zeta(-k).$$ This depends on the analytic theory of Definition 2.1.1 and on the special values Corollary 2.3.4.

Proof for Lemma 4.1.1
uses 1

Use the Mellin presentation L(\fa,s) = \frac{1}{\Gamma(s)}\int_0^\infty \fa(t)\,t^{s-1}\,dt, valid for \Re(s) large because \fa is \cC^\infty and rapidly decreasing. Split \fa(t) = \frac{1}{e^t-1} - \frac{a}{e^{at}-1} into its two terms. The first gives the classical integral \frac{1}{\Gamma(s)}\int_0^\infty \frac{t^{s-1}}{e^t-1}\,dt = \zeta(s). In the second, substitute u = at: then a\,t^{s-1}\,dt = a^{1-s}u^{s-1}\,du and e^{at}-1 = e^u-1, so the term becomes a^{1-s}\cdot\frac{1}{\Gamma(s)}\int_0^\infty \frac{u^{s-1}}{e^u-1}\,du = a^{1-s}\zeta(s). Subtracting, L(\fa,s) = (1-a^{1-s})\zeta(s), which inherits the analytic continuation of \zeta to \C (the factor 1-a^{1-s} is entire). For the derivatives, expand the generating series \frac{t}{e^t-1} = \sum_{n\ge0} B_n\frac{t^n}{n!}, so that \frac{1}{e^t-1} = \sum_{n\ge0} B_n\frac{t^{n-1}}{n!} and \fa(t) = \sum_{n\ge0} B_n(1-a^n)\frac{t^{n-1}}{n!}. The coefficient of t^k is \frac{B_{k+1}(1-a^{k+1})}{(k+1)!}, whence \fa^{(k)}(0) = \frac{B_{k+1}(1-a^{k+1})}{k+1}. Substituting the special value \zeta(-k) = (-1)^k B_{k+1}/(k+1) from Corollary 2.3.4 turns the Bernoulli factor into (-1)^k\zeta(-k), giving \fa^{(k)}(0) = (-1)^k(1-a^{1+k})\zeta(-k).

The next observation turns the analytic object \fa into a p-adic power series. Under e^t = T+1 the operator d/dt becomes \pa = (1+T)\frac{d}{dT}.

Lemma4.1.2
uses 0used by 1✓L∃∀N

Under the substitution e^t = T+1, the derivative d/dt corresponds to the operator \pa = (1+T)\frac{d}{dT}. Setting \Fa(T) := \frac{1}{T} - \frac{a}{(1+T)^a - 1},$$ one has \fa^{(k)}(0) = (\pa^k \Fa)(0) for all k \ge 0.

Lean code for Lemma4.1.2●1 theorem
  • theoremdefined in PadicLFunctions/KubotaLeopoldt/MuA.lean
    complete
    theorem PadicMeasure.constantCoeff_iterate_delQ (p : ℕ)
  [hp : Fact (Nat.Prime p)] (k : ℕ) (F : PowerSeries ℚ_[p]) :
  PowerSeries.constantCoeff ((PadicMeasure.delQ p)^[k] F) =
    ↑k.factorial *
      (PowerSeries.coeff k)
        (PowerSeries.subst (PowerSeries.exp ℚ_[p] - 1) F)
    theorem PadicMeasure.constantCoeff_iterate_delQ
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (k : ℕ) (F : PowerSeries ℚ_[p]) :
  PowerSeries.constantCoeff
      ((PadicMeasure.delQ p)^[k] F) =
    ↑k.factorial *
      (PowerSeries.coeff k)
        (PowerSeries.subst
          (PowerSeries.exp ℚ_[p] - 1) F)
    `(∂^k F)(0) = k! · [t^k](F(e^t−1))`: evaluating iterated `∂` at `0` extracts
Taylor coefficients after the exponential substitution (RJW eq. between Lem. 4.3
and Prop. 4.6).
Proof for Lemma 4.1.2
uses 0

Since e^t = 1+T, we have \frac{dT}{dt} = e^t = 1+T, so the chain rule turns \frac{d}{dt} into the operator \frac{dT}{dt}\frac{d}{dT} = (1+T)\frac{d}{dT} = \pa acting on functions of T. Substituting e^t = 1+T and e^{at} = (1+T)^a into \fa(t) = \frac{1}{e^t-1} - \frac{a}{e^{at}-1} expresses it as the rational function \Fa(T) = \frac1T - \frac{a}{(1+T)^a-1}. As \frac{d}{dt} and \pa agree as operators under the substitution, their k-fold iterates \frac{d^k}{dt^k} and \pa^k also agree; the substitution sends t=0 to T=0, so evaluating both at the origin gives \fa^{(k)}(0) = (\pa^k \Fa)(0).

The left-hand side \fa^{(k)}(0) computes the zeta value \zeta(-k) by Lemma 4.1.1, while the right-hand side (\pa^k\Fa)(0) is exactly the shape of the formula \int_{\Zp} x^k\cdot\mu = (\pa^k \Am_\mu)(0) expressing integrals of monomials in terms of the Mahler transform \Am_\mu. This motivates seeking a measure \mua with \Am_{\mua} = \Fa; for that we first check \Fa is a bounded power series.

Proposition4.1.3
uses 0used by 1✓L∃∀N

The function \Fa(T) lies in \Zp[[T]].

Lean code for Proposition4.1.3●1 theorem
  • theoremdefined in PadicLFunctions/KubotaLeopoldt/MuA.lean
    complete
    theorem PadicMeasure.one_add_X_pow_sub_one_mul_Fa (p : ℕ)
  [hp : Fact (Nat.Prime p)] {a : ℕ} (hpa : ¬p ∣ a) :
  ((1 + PowerSeries.X) ^ a - 1) * PadicMeasure.Fa p a =
    PadicMeasure.geomSum p a - ↑a
    theorem PadicMeasure.one_add_X_pow_sub_one_mul_Fa
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  {a : ℕ} (hpa : ¬p ∣ a) :
  ((1 + PowerSeries.X) ^ a - 1) *
      PadicMeasure.Fa p a =
    PadicMeasure.geomSum p a - ↑a
    The characterising identity `((1+T)^a − 1)·F_a = geomSum a − a`, the formal
content of `F_a = 1/T − a/((1+T)^a−1)`. Source: RJW Lem. 4.3 (TeX line 1475).
Proof for Proposition 4.1.3
uses 0

Expand the denominator using the binomial series: (1+T)^a - 1 = \sum_{n\ge 1}\binom{a}{n}T^n = aT\bigl[\,1 + T g(T)\,\bigr],$$ where g(T) = \sum_{n\ge 2}\tfrac{1}{a}\binom{a}{n}T^{n-2}. Each coefficient \tfrac1a\binom{a}{n} is a p-adic integer: the binomial coefficients \binom{a}{n} lie in \Z, and dividing by a does not leave \Zp precisely because a is a unit in \Zp (here we use that a is coprime to p). Thus g(T)\in\Zp[[T]]. Substituting and cancelling the factor a, \frac{1}{T} - \frac{a}{(1+T)^a-1} = \frac{1}{T} - \frac{1}{T\bigl(1 + Tg(T)\bigr)} = \frac{1}{T}\Bigl(1 - \frac{1}{1+Tg(T)}\Bigr) = \frac{1}{T}\cdot\frac{Tg(T)}{1+Tg(T)}.$$ Since Tg(T) has zero constant term, 1+Tg(T) is a unit in \Zp[[T]] and the geometric series gives \frac{Tg(T)}{1+Tg(T)} = \sum_{n\ge 1}(-1)^{n-1}\bigl(Tg(T)\bigr)^n, each term of which is divisible by T. Dividing by T therefore cancels the pole and leaves a power series with \Zp-coefficients, so \Fa(T)\in\Zp[[T]].

Definition4.1.4
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 7
Reverse dependency previews
Preview
Proposition 4.1.5
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N

Fix an integer a coprime to p. Let \mua be the (unique) p-adic measure on \Zp whose Mahler transform is \Am_{\mua} = \Fa(T); this exists by Proposition 4.1.3 together with the Definition 3.4.3 identification of measures with \Zp[[T]].

Lean code for Definition4.1.4●1 definition
  • defdefined in PadicLFunctions/KubotaLeopoldt/MuA.lean
    complete
    def PadicMeasure.muA (p : ℕ) [hp : Fact (Nat.Prime p)] (a : ℕ) :
  PadicMeasure p ℤ_[p]
    def PadicMeasure.muA (p : ℕ)
  [hp : Fact (Nat.Prime p)] (a : ℕ) :
  PadicMeasure p ℤ_[p]
    **RJW Def. 4.5 (`DefinitionMeasuremua`)**: the measure `μ_a` on `ℤ_p` whose Mahler
transform is `F_a`.
Proposition4.1.5
uses 0used by 1✓L∃∀N

For all k \ge 0, \int_{\Zp} x^k \cdot \mua = (-1)^k\,(1 - a^{k+1})\,\zeta(-k).$$

Lean code for Proposition4.1.5●1 theorem
  • theoremdefined in PadicLFunctions/KubotaLeopoldt/MuA.lean
    complete
    theorem PadicMeasure.muA_apply_powCM (p : ℕ) [hp : Fact (Nat.Prime p)] {a : ℕ}
  (hpa : ¬p ∣ a) (k : ℕ) :
  ↑((PadicMeasure.muA p a) (PadicMeasure.powCM p k)) =
    (-1) ^ k * (1 - ↑a ^ (k + 1)) * ↑(zetaNeg k)
    theorem PadicMeasure.muA_apply_powCM (p : ℕ)
  [hp : Fact (Nat.Prime p)] {a : ℕ}
  (hpa : ¬p ∣ a) (k : ℕ) :
  ↑((PadicMeasure.muA p a)
        (PadicMeasure.powCM p k)) =
    (-1) ^ k * (1 - ↑a ^ (k + 1)) *
      ↑(zetaNeg k)
    **RJW Prop. 4.6**: `∫_{ℤ_p} x^k dμ_a = (−1)^k (1 − a^{k+1}) ζ(−k)` in `ℚ_p`.
Proof for Proposition 4.1.5
Proof uses 4
Proof dependency previews
Preview
Definition 3.4.3
Loading preview
Proof dependency preview content is loaded from the Blueprint HTML cache.

The Definition 3.4.3 satisfies \int_{\Zp} x^k\cdot\mu = (\pa^k \Am_{\mu})(0), expressing the k-th monomial integral as the k-fold \pa-derivative of the Mahler transform at the origin. Apply this to \mu = \mua. By the definition Definition 4.1.4 of \mua we have \Am_{\mua} = \Fa, so the integral equals (\pa^k \Fa)(0), which is \fa^{(k)}(0) by Lemma 4.1.2. Finally \fa^{(k)}(0) = (-1)^k(1-a^{k+1})\zeta(-k) by Lemma 4.1.1.