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

5.1. Characters of p-power conductor🔗

The headline result twists \zetap by a Dirichlet character of p-power conductor. Its proof runs the construction of \zetap in reverse: a twisted measure is built, its Mahler transform is computed, the corresponding function of t is identified with a complex L-function via the Mellin transform, and the special-value formula is read off.

Theorem5.1.1
Statement uses 4
Statement dependency previews
Preview
Definition 2.1.3
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
Used by 7
Reverse dependency previews
Preview
Theorem 2.5.1
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N

Let \chi be a primitive Dirichlet character of conductor p^n, n \geq 1, viewed as a locally constant character of \Zpx. Then for every integer k > 0, \int_{\Zpx}\chi(x)\,x^k \cdot \zetap = L(\chi, 1-k). This depends on Definition 4.3.2, Definition 5.1.2, Lemma 5.1.6 and Definition 2.1.3.

In the formalisation the pairing with \zetap follows the witness encoding of PadicMeasure.kubotaLeopoldt: tame_conductor states that every measure-witness ν of ([b]-[1])\zetap has χ-twisted moments (\chi(b)b^k - 1)\,L(\chi,1-k); the engine is the θ-form tame_conductor_theta (\int \chi(x)x^k\,\theta_a = -(1-\chi(a)a^k)L(\chi,1-k), the source's own display) and the moment formula twist_muA_moments. The value L(\chi,1-k) is the generalised Bernoulli expression LvalNeg (complex comparison: LFunction_neg_nat), and a primitive p^n-th root of unity in the coefficient field is assumed, mirroring the source's ambient \eps_{p^n}.

Lean code for Theorem5.1.1●3 theorems
  • theoremdefined in PadicLFunctions/Interpolation/TameConductor.lean
    complete
    theorem PadicLFunctions.MeasureR.tame_conductor.{u_1} {p : ℕ}
  [hp : Fact (Nat.Prime p)] {K : Type u_1} [NormedField K]
  [NormedAlgebra ℚ_[p] K] [IsUltrametricDist K] [CompleteSpace K]
  [CharZero K] {n : ℕ} (hn : 1 ≤ n) (hp2 : p ≠ 2)
  {χ : DirichletCharacter (↥(PadicLFunctions.integerRing K)) (p ^ n)}
  (hχ : χ.IsPrimitive) {ζ : ↥(PadicLFunctions.integerRing K)}
  (hζ : IsPrimitiveRoot ζ (p ^ n)) {k : ℕ} (hk : 0 < k) (b : ℤ_[p]ˣ)
  (ν : PadicMeasure p ℤ_[p]ˣ)
  (hν :
    (algebraMap (PadicMeasure p ℤ_[p]ˣ) (PadicMeasure.QuotientField p))
          (PadicMeasure.dirac p b - 1) *
        PadicMeasure.padicZeta p hp2 =
      (algebraMap (PadicMeasure p ℤ_[p]ˣ)
          (PadicMeasure.QuotientField p))
        ν) :
  ↑(((PadicLFunctions.MeasureR.baseChange p K)
          ((PadicMeasure.iota p) ν))
        (χ.toContinuousMapZp * PadicLFunctions.MeasureR.powCM p K k)) =
    (↑(χ ((PadicInt.toZModPow n) ↑b)) * (algebraMap ℚ_[p] K) (↑↑b ^ k) -
        1) *
      PadicLFunctions.LvalNeg (PadicLFunctions.MeasureR.toFieldChar χ)
        (k - 1)
    theorem PadicLFunctions.MeasureR.tame_conductor.{u_1}
  {p : ℕ} [hp : Fact (Nat.Prime p)]
  {K : Type u_1} [NormedField K]
  [NormedAlgebra ℚ_[p] K]
  [IsUltrametricDist K] [CompleteSpace K]
  [CharZero K] {n : ℕ} (hn : 1 ≤ n)
  (hp2 : p ≠ 2)
  {χ :
    DirichletCharacter
      (↥(PadicLFunctions.integerRing K))
      (p ^ n)}
  (hχ : χ.IsPrimitive)
  {ζ : ↥(PadicLFunctions.integerRing K)}
  (hζ : IsPrimitiveRoot ζ (p ^ n)) {k : ℕ}
  (hk : 0 < k) (b : ℤ_[p]ˣ)
  (ν : PadicMeasure p ℤ_[p]ˣ)
  (hν :
    (algebraMap (PadicMeasure p ℤ_[p]ˣ)
            (PadicMeasure.QuotientField
              p))
          (PadicMeasure.dirac p b - 1) *
        PadicMeasure.padicZeta p hp2 =
      (algebraMap (PadicMeasure p ℤ_[p]ˣ)
          (PadicMeasure.QuotientField p))
        ν) :
  ↑(((PadicLFunctions.MeasureR.baseChange
            p K)
          ((PadicMeasure.iota p) ν))
        (χ.toContinuousMapZp *
          PadicLFunctions.MeasureR.powCM p
            K k)) =
    (↑(χ ((PadicInt.toZModPow n) ↑b)) *
          (algebraMap ℚ_[p] K) (↑↑b ^ k) -
        1) *
      PadicLFunctions.LvalNeg
        (PadicLFunctions.MeasureR.toFieldChar
          χ)
        (k - 1)
    **RJW Theorem 5.1** (`thm:tame conductor`, TeX 1619–1622), witness form
mirroring `PadicMeasure.kubotaLeopoldt`'s encoding: for every unit `b` and
every measure-witness `ν` of `([b]−[1])·ζ_p`, the χ-twisted `k`-th moment of
`ν` (base-changed) equals `(χ(b)·b^k − 1)·L(χ, 1−k)`.

"Let χ be a (primitive) Dirichlet character of conductor `p^n` ... Then, for
`k > 0`, we have `∫_{ℤ_p^×}χ(x)x^k · ζ_p = L(χ,1−k)`."

`hζ` mirrors the source's ambient `ε_{p^n}` (statement replan, as in
`twist_muA_moments`).
  • theoremdefined in PadicLFunctions/Interpolation/TameConductor.lean
    complete
    theorem PadicLFunctions.MeasureR.tame_conductor_theta.{u_1} {p : ℕ}
  [hp : Fact (Nat.Prime p)] {K : Type u_1} [NormedField K]
  [NormedAlgebra ℚ_[p] K] [IsUltrametricDist K] [CompleteSpace K]
  [CharZero K] {n : ℕ} (hn : 1 ≤ n)
  {χ : DirichletCharacter (↥(PadicLFunctions.integerRing K)) (p ^ n)}
  (hχ : χ.IsPrimitive) {ζ : ↥(PadicLFunctions.integerRing K)}
  (hζ : IsPrimitiveRoot ζ (p ^ n)) {a : ℕ} (hpa : ¬p ∣ a) {k : ℕ}
  (hk : 0 < k) :
  ↑(((PadicLFunctions.MeasureR.baseChange p K)
          ((PadicMeasure.iota p) (PadicMeasure.zetaNum p a)))
        (χ.toContinuousMapZp * PadicLFunctions.MeasureR.powCM p K k)) =
    -(1 - ↑(χ ↑a) * ↑a ^ k) *
      PadicLFunctions.LvalNeg (PadicLFunctions.MeasureR.toFieldChar χ)
        (k - 1)
    theorem PadicLFunctions.MeasureR.tame_conductor_theta.{u_1}
  {p : ℕ} [hp : Fact (Nat.Prime p)]
  {K : Type u_1} [NormedField K]
  [NormedAlgebra ℚ_[p] K]
  [IsUltrametricDist K] [CompleteSpace K]
  [CharZero K] {n : ℕ} (hn : 1 ≤ n)
  {χ :
    DirichletCharacter
      (↥(PadicLFunctions.integerRing K))
      (p ^ n)}
  (hχ : χ.IsPrimitive)
  {ζ : ↥(PadicLFunctions.integerRing K)}
  (hζ : IsPrimitiveRoot ζ (p ^ n)) {a : ℕ}
  (hpa : ¬p ∣ a) {k : ℕ} (hk : 0 < k) :
  ↑(((PadicLFunctions.MeasureR.baseChange
            p K)
          ((PadicMeasure.iota p)
            (PadicMeasure.zetaNum p a)))
        (χ.toContinuousMapZp *
          PadicLFunctions.MeasureR.powCM p
            K k)) =
    -(1 - ↑(χ ↑a) * ↑a ^ k) *
      PadicLFunctions.LvalNeg
        (PadicLFunctions.MeasureR.toFieldChar
          χ)
        (k - 1)
    **RJW Theorem 5.1**, θ-form — the source's own engine (TeX 1757–1761:
"`∫_{ℤ_p^×}χ(x)x^k · x^{-1}μ_a = −(1−χ(a)a^k)L(χ,1−k)`"): the χ-twisted
`k`-th moment of the base change of the §4 unit-side measure
`zetaNum a = x⁻¹·Res_{ℤ_p^×}(μ_a)` is `−(1−χ(a)a^k)·L(χ,1−k)`.

`hζ` mirrors the source's ambient `ε_{p^n}` (statement replan, as in
`twist_muA_moments`).
  • theoremdefined in PadicLFunctions/Interpolation/TameConductor.lean
    complete
    theorem PadicLFunctions.MeasureR.twist_muA_moments.{u_1} {p : ℕ}
  [hp : Fact (Nat.Prime p)] {K : Type u_1} [NormedField K]
  [NormedAlgebra ℚ_[p] K] [IsUltrametricDist K] [CompleteSpace K]
  [CharZero K] {n : ℕ} (hn : 1 ≤ n)
  {χ : DirichletCharacter (↥(PadicLFunctions.integerRing K)) (p ^ n)}
  (hχ : χ.IsPrimitive) {ζ : ↥(PadicLFunctions.integerRing K)}
  (hζ : IsPrimitiveRoot ζ (p ^ n)) {a : ℕ} (hpa : ¬p ∣ a) (k : ℕ) :
  ↑((PadicLFunctions.MeasureR.twist p K χ.toContinuousMapZp
          ((PadicLFunctions.MeasureR.baseChange p K)
            (PadicMeasure.muA p a)))
        (PadicLFunctions.MeasureR.powCM p K k)) =
    -(1 - ↑(χ ↑a) * ↑a ^ (k + 1)) *
      PadicLFunctions.LvalNeg (PadicLFunctions.MeasureR.toFieldChar χ) k
    theorem PadicLFunctions.MeasureR.twist_muA_moments.{u_1}
  {p : ℕ} [hp : Fact (Nat.Prime p)]
  {K : Type u_1} [NormedField K]
  [NormedAlgebra ℚ_[p] K]
  [IsUltrametricDist K] [CompleteSpace K]
  [CharZero K] {n : ℕ} (hn : 1 ≤ n)
  {χ :
    DirichletCharacter
      (↥(PadicLFunctions.integerRing K))
      (p ^ n)}
  (hχ : χ.IsPrimitive)
  {ζ : ↥(PadicLFunctions.integerRing K)}
  (hζ : IsPrimitiveRoot ζ (p ^ n)) {a : ℕ}
  (hpa : ¬p ∣ a) (k : ℕ) :
  ↑((PadicLFunctions.MeasureR.twist p K
          χ.toContinuousMapZp
          ((PadicLFunctions.MeasureR.baseChange
              p K)
            (PadicMeasure.muA p a)))
        (PadicLFunctions.MeasureR.powCM p
          K k)) =
    -(1 - ↑(χ ↑a) * ↑a ^ (k + 1)) *
      PadicLFunctions.LvalNeg
        (PadicLFunctions.MeasureR.toFieldChar
          χ)
        k
    L5.1.10: the χ-twisted moments of the base-changed `μ_a` (RJW
eq:special value theorem 1, TeX 1727–1730, uniform `LvalNeg` form): for `χ`
primitive mod `p^n` (`n ≥ 1`), `a` coprime to `p`, `k : ℕ`,
`∫ χ(x)x^k dμ_a = −(1 − χ(a)·a^{k+1})·L(χ,−k)`.

The hypothesis `hζ` (a primitive `p^n`-th root of unity in the coefficient
ring) mirrors the source's ambient `ε_{p^n} ∈ Q̄_p` (TeX 1657–1660: the fixed
compatible system of `p`-power roots of unity) — recorded statement-replan:
the skeleton omitted it, but the proof route (Lem 5.4) and the source both
live over a field containing `μ_{p^n}`.
Proof for Theorem 5.1.1
Proof uses 2
Proof dependency previews
Preview
Definition 5.1.2
Loading preview
Proof dependency preview content is loaded from the Blueprint HTML cache.

Since \chi vanishes on p\Zp, integrating over \Zpx is the same as integrating over \Zp, and by the definition of the twist Definition 5.1.2 this equals \int_{\Zp} x^k \cdot \mu_{\chi,a}, where \mu_{\chi,a} is the twist of the measure \mua by \chi. Under e^t = T+1 this integral is (\partial^k F_{\chi,a})(0) = f_{\chi,a}^{(k)}(0). By Lemma 5.1.6 we obtain \int_{\Zpx}\chi(x)x^k\cdot\mua = -(1-\chi(a)a^{k+1})L(\chi,-k), and integrating against x^{-1} shifts this to \int_{\Zpx}\chi(x)x^k \cdot x^{-1}\mua = -(1-\chi(a)a^{k})L(\chi,1-k). The smoothing measure \theta_a used in the construction of \zetap satisfies \int_{\Zpx}\chi(x)x^k\cdot\theta_a = -(1-\chi(a)a^{k}); dividing the previous identity by this Euler-type factor cancels the (1-\chi(a)a^k) exactly and leaves \int_{\Zpx}\chi(x)x^k\cdot\zetap = L(\chi,1-k), as claimed.

We first record the twisting operation and the classical Gauss-sum input it requires, then compute the Mahler transform of a twist.

Definition5.1.2
uses 0
Used by 2
Reverse dependency previews
Preview
Theorem 5.1.1
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N

Let \mu be a measure on \Zp and \chi a locally constant character of \Zpx. The twist of \mu by \chi is the measure \mu_\chi on \Zp defined by \int_{\Zp} f(x)\cdot\mu_\chi = \int_{\Zp}\chi(x)f(x)\cdot\mu. Because \chi is supported on \Zpx, the measure \mu_\chi is automatically supported on \Zpx.

The formalisation defines the twist by an arbitrary continuous function (MeasureR.twist, specialised to Dirichlet characters through their zero-extension DirichletCharacter.toContinuousMapZp); the automatic support statement is the restriction-invariance lemma twist_res_units.

Lean code for Definition5.1.2●2 declarations
  • defdefined in PadicLFunctions/Interpolation/Twist.lean
    complete
    def PadicLFunctions.MeasureR.twist.{u_1} (p : ℕ) [hp : Fact (Nat.Prime p)]
  (K : Type u_1) [NormedField K] [IsUltrametricDist K]
  (g : C(ℤ_[p], ↥(PadicLFunctions.integerRing K)))
  (μ : PadicLFunctions.MeasureR K ℤ_[p]) :
  PadicLFunctions.MeasureR K ℤ_[p]
    def PadicLFunctions.MeasureR.twist.{u_1}
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (K : Type u_1) [NormedField K]
  [IsUltrametricDist K]
  (g :
    C(ℤ_[p],
      ↥(PadicLFunctions.integerRing K)))
  (μ : PadicLFunctions.MeasureR K ℤ_[p]) :
  PadicLFunctions.MeasureR K ℤ_[p]
    L5.1.2: the twist of a measure by a continuous `R`-valued function
(specialised to characters): `(twist g μ)(f) = μ(g·f)` — RJW eq:twist by chi
(TeX 1637–1640) reads `∫ f dμ_χ = ∫ χ f dμ`.
  • theoremdefined in PadicLFunctions/Interpolation/Twist.lean
    complete
    theorem PadicLFunctions.MeasureR.twist_res_units.{u_1} (p : ℕ)
  [hp : Fact (Nat.Prime p)] (K : Type u_1) [NormedField K]
  [IsUltrametricDist K] {n : ℕ} (hn : 1 ≤ n)
  (χ : DirichletCharacter (↥(PadicLFunctions.integerRing K)) (p ^ n))
  (μ : PadicLFunctions.MeasureR K ℤ_[p]) :
  PadicLFunctions.MeasureR.res p K ⋯
      (PadicLFunctions.MeasureR.twist p K χ.toContinuousMapZp μ) =
    PadicLFunctions.MeasureR.twist p K χ.toContinuousMapZp μ
    theorem PadicLFunctions.MeasureR.twist_res_units.{u_1}
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (K : Type u_1) [NormedField K]
  [IsUltrametricDist K] {n : ℕ}
  (hn : 1 ≤ n)
  (χ :
    DirichletCharacter
      (↥(PadicLFunctions.integerRing K))
      (p ^ n))
  (μ : PadicLFunctions.MeasureR K ℤ_[p]) :
  PadicLFunctions.MeasureR.res p K ⋯
      (PadicLFunctions.MeasureR.twist p K
        χ.toContinuousMapZp μ) =
    PadicLFunctions.MeasureR.twist p K
      χ.toContinuousMapZp μ
    L5.1.3 (integral form, at the use site of Thm 5.1): for `n ≥ 1`, a
`χ`-twisted integral over `ℤ_p` equals the integral over `ℤ_p^×` — i.e.
restriction to the units does not change the twist (RJW TeX 1641: "as `χ` is
supported on `ℤ_p^×`, the twisted measure `μ_χ` is automatically supported on
`ℤ_p^×` as well"; TeX 1752–1753).
Definition5.1.3
uses 0
Used by 3
Reverse dependency previews
Preview
Lemma 5.1.4
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N

Let \chi be a primitive Dirichlet character of conductor p^n, n \geq 1. The Gauss sum of \chi is G(\chi) := \sum_{c \in (\Z/p^n\Z)^\times} \chi(c)\,\eps_{p^n}^{\,c}, where (\eps_{p^n})_n is the fixed compatible system of primitive p-power roots of unity in \Qpbar (one may take \eps_{p^n} = e^{2\pi i/p^n} under a fixed isomorphism \Qpbar \cong \C).

Lean code for Definition5.1.3●1 definition
  • defdefined in Mathlib/NumberTheory/GaussSum.lean
    complete
    def gaussSum.{u, v} {R : Type u} [CommRing R] [Fintype R] {R' : Type v}
  [CommRing R'] (χ : MulChar R R') (ψ : AddChar R R') : R'
    def gaussSum.{u, v} {R : Type u} [CommRing R]
  [Fintype R] {R' : Type v} [CommRing R']
  (χ : MulChar R R') (ψ : AddChar R R') :
  R'
    Definition of the Gauss sum associated to a multiplicative and an additive character.
Lemma5.1.4
uses 1used by 1XL∃∀N

The Gauss sum of a primitive Dirichlet character \chi of conductor p^n satisfies two basic identities. (i) G(\chi)\,G(\chi^{-1}) = \chi(-1)\,p^n; in particular G(\chi) is nonzero. (ii) For every a \in \Zpx, G(\chi) = \chi(a)\sum_{c\in(\Z/p^n\Z)^\times}\chi(c)\,\eps_{p^n}^{\,ac}. This rests on Definition 5.1.3.

Proof for Lemma 5.1.4
uses 0

These are standard facts on Gauss sums. For (ii), substituting c \mapsto a^{-1}c in the defining sum and using multiplicativity of \chi rewrites \sum_c \chi(c)\eps_{p^n}^{ac} as \chi(a)^{-1}\sum_c \chi(c)\eps_{p^n}^{c} = \chi(a)^{-1}G(\chi), which rearranges to the stated identity (the change of variables is a bijection of (\Z/p^n\Z)^\times since a is a unit). For (i), expand G(\chi)G(\chi^{-1}) as a double sum over (\Z/p^n\Z)^\times, change variables to separate the additive characters, and evaluate the resulting character sums; the cross terms cancel and the diagonal contributes \chi(-1)p^n. Nonvanishing of G(\chi) is immediate from (i) since \chi(-1)p^n \neq 0.

Lemma5.1.5
Statement uses 4
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 5.1.6
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N

Let \chi be a primitive Dirichlet character of conductor p^n, n \geq 1, and \mu a measure on \Zp. Then the Mahler transform of the twist \mu_\chi is \Am_{\mu_\chi}(T) = \frac{1}{G(\chi^{-1})}\sum_{c\in(\Z/p^n\Z)^\times} \chi(c)^{-1}\,\Am_\mu\big((1+T)\eps_{p^n}^{\,c} - 1\big). This uses Definition 5.1.2, Definition 5.1.3, Lemma 5.1.4 and Definition 3.4.3.

The formalisation states this multiplied through by the Gauss sum G(\chi^{-1}) and as an identity of measures (mahler_twist_formula): G(\chi^{-1})\cdot\mu_\chi = \sum_c \chi^{-1}(c)\,\kappa_{\eps^c-1}\mu, the sum running over all residues (the character kills the non-units); applying the Mahler transform recovers the display.

Lean code for Lemma5.1.5●1 theorem
  • theoremdefined in PadicLFunctions/Interpolation/Twist.lean
    complete
    theorem PadicLFunctions.MeasureR.mahler_twist_formula.{u_1} {p : ℕ}
  [hp : Fact (Nat.Prime p)] {K : Type u_1} [NormedField K]
  [NormedAlgebra ℚ_[p] K] [IsUltrametricDist K] [CompleteSpace K]
  {n : ℕ}
  {χ : DirichletCharacter (↥(PadicLFunctions.integerRing K)) (p ^ n)}
  (hχ : χ.IsPrimitive) {ζ : ↥(PadicLFunctions.integerRing K)}
  (hζ : IsPrimitiveRoot ζ (p ^ n))
  (μ : PadicLFunctions.MeasureR K ℤ_[p]) :
  gaussSum χ⁻¹ (AddChar.zmodChar (p ^ n) ⋯) •
      PadicLFunctions.MeasureR.twist p K χ.toContinuousMapZp μ =
    ∑ c ∈ Finset.range (p ^ n),
      χ⁻¹ ↑c •
        PadicLFunctions.MeasureR.twist p K
          (PadicLFunctions.MeasureR.charCM (ζ ^ c - 1) ⋯) μ
    theorem PadicLFunctions.MeasureR.mahler_twist_formula.{u_1}
  {p : ℕ} [hp : Fact (Nat.Prime p)]
  {K : Type u_1} [NormedField K]
  [NormedAlgebra ℚ_[p] K]
  [IsUltrametricDist K] [CompleteSpace K]
  {n : ℕ}
  {χ :
    DirichletCharacter
      (↥(PadicLFunctions.integerRing K))
      (p ^ n)}
  (hχ : χ.IsPrimitive)
  {ζ : ↥(PadicLFunctions.integerRing K)}
  (hζ : IsPrimitiveRoot ζ (p ^ n))
  (μ : PadicLFunctions.MeasureR K ℤ_[p]) :
  gaussSum χ⁻¹
        (AddChar.zmodChar (p ^ n) ⋯) •
      PadicLFunctions.MeasureR.twist p K
        χ.toContinuousMapZp μ =
    ∑ c ∈ Finset.range (p ^ n),
      χ⁻¹ ↑c •
        PadicLFunctions.MeasureR.twist p K
          (PadicLFunctions.MeasureR.charCM
            (ζ ^ c - 1) ⋯)
          μ
    L5.1.8 (RJW Lem 5.4, cleared — statement form pinned by the planning
trace at decomposition L5.1.8 attack [2]): for `χ` primitive mod `p^n`
(`n ≥ 1`) and `ζ` a primitive `p^n`-th root of unity,
`G(χ⁻¹) · 𝓐(μ_χ) = ∑_{c units} χ⁻¹(c) · 𝓐(κ_{ζ^c−1}·μ)`.

Source (verbatim, TeX 1675–1678): "The Mahler transform of `μ_χ` is
`𝓐_{μ_χ}(T) = (1/G(χ⁻¹)) ∑_c χ(c)⁻¹ 𝓐_μ((1+T)ε^c − 1)`" — multiplied
through by the Gauss sum.
Proof for Lemma 5.1.5
uses 1

Since \chi is constant modulo p^n, the twist decomposes as a weighted sum of restrictions, \mu_\chi = \sum_{c\in(\Z/p^n\Z)^\times}\chi(c)\,\Res_{c+p^n\Zp}(\mu). Applying the formula for the Mahler transform of a restriction to b + p^n\Zp, \Am_{\Res_{b+p^n\Zp}(\mu)}(T) = \frac{1}{p^n}\sum_{\xi\in\mu_{p^n}} \xi^{-b}\,\Am_\mu\big((1+T)\xi - 1\big), and summing over b, we get \Am_{\mu_\chi}(T) = p^{-n}\sum_{b}\chi(b)\sum_{\xi\in\mu_{p^n}}\xi^{-b} \Am_\mu((1+T)\xi-1). Writing each \xi = \eps_{p^n}^{c} and interchanging the sums, the inner sum over b becomes \sum_b \chi(b)\eps_{p^n}^{-bc}, which by Lemma 5.1.4(ii) equals G(\chi)\chi(-c)^{-1}. Thus \Am_{\mu_\chi}(T) = p^{-n}\sum_c G(\chi)\chi(-c)^{-1}\Am_\mu((1+T)\eps_{p^n}^c-1), and substituting G(\chi)/p^n = \chi(-1)/G(\chi^{-1}) from Lemma 5.1.4(i) together with \chi(-c)^{-1} = \chi(-1)\chi(c)^{-1} gives the claimed formula.

Specialising to \mu = \mua — the measure with \Am_{\mua}(T) = \tfrac1T - \tfrac{a}{(1+T)^a - 1} from which \zetap was built — and substituting e^t = T+1 motivates the study of the auxiliary function f_{\chi,a}(t) = \frac{1}{G(\chi^{-1})}\sum_{c\in(\Z/p^n\Z)^\times}\chi(c)^{-1} \left[\frac{1}{e^t\eps_{p^n}^{\,c} - 1} - \frac{a}{e^{at}\eps_{p^n}^{\,ac} - 1}\right].

-- Deliberately unwired (§5 board, 2026-06-10): the Mellin/analytic-continuation -- half of this lemma is §2 material (deferred), following the -- kl-values-of-zeta pattern. The L-value content the §5 statements consume is -- encoded algebraically as LvalNeg (minus the (k+1)-st generalised Bernoulli -- number over (k+1), GenBernoulli.lean), with the complex comparison -- PadicLFunctions.LFunction_neg_nat (GenBernoulliComplex.lean, all k ≥ 0; -- the k = 0 case rests on the sawtooth boundary value -- sinZeta_one_eq_boundary, Sawtooth.lean).

Lemma5.1.6
Statement uses 2
Statement dependency previews
Preview
Definition 2.1.3
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
Used by 2
Reverse dependency previews
Preview
Theorem 5.1.1
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
XL∃∀N

With f_{\chi,a} as above and L(f,s) = \frac{1}{\Gamma(s)}\int_0^\infty f(t)t^{s-1}dt the complex Mellin transform (whose special-value formula L(f,-n)=(-1)^n f^{(n)}(0) was established earlier), we have L(f_{\chi,a}, s) = \chi(-1)\big(1-\chi(a)a^{1-s}\big)\,L(\chi,s). Moreover, for k \geq 0, f_{\chi,a}^{(k)}(0) = \begin{cases} -\big(1-\chi(a)a^{k+1}\big)L(\chi,-k) & \chi(-1)(-1)^k = -1,\\ 0 & \chi(-1)(-1)^k = 1.\end{cases} This uses Lemma 5.1.5 and Definition 2.1.3.

Proof for Lemma 5.1.6
uses 0

Expanding each summand as a geometric series, \frac{1}{e^t\eps_{p^n}^c - 1} = \sum_{k\geq 1} e^{-kt}\eps_{p^n}^{-kc}, and feeding this into the Mellin integral L(f_{\chi,a},s) = \frac{1}{\Gamma(s)}\int_0^\infty f_{\chi,a}(t)t^{s-1}dt, the inner character sum \sum_c \chi(c)^{-1}\eps_{p^n}^{-akc} collapses to \chi(-ak)G(\chi^{-1}) (and similarly for the first term), cancelling the G(\chi^{-1}) in the denominator. The integral reduces to \frac{1}{\Gamma(s)}\int_0^\infty\sum_{k\geq1}\chi(-k)(e^{-kt}-\chi(a)e^{-akt}) t^{s-1}dt. For \Re(s)\gg 0 one may interchange sum and integral; the k-th term integrates to (1-\chi(a)a^{1-s})k^{-s}, yielding \chi(-1)(1-\chi(a) a^{1-s})\sum_{k\geq1}\chi(-k)k^{-s} = \chi(-1)(1-\chi(a)a^{1-s})L(\chi,s). This is entirely classical: p never appears. The Mellin special-value formula then gives f_{\chi,a}^{(k)}(0) = (-1)^k\chi(-1)(1-\chi(a)a^{k+1})L(\chi,-k).

For the parity dichotomy, the identity \frac{1}{e^{-t}\eps_{p^n}^c - 1} = -1 - \frac{1}{e^t\eps_{p^n}^{-c}-1} applied twice, followed by the substitution c\mapsto -c, shows f_{\chi,a}(-t) = -\chi(-1)f_{\chi,a}(t). Comparing k-th derivatives at 0 gives (-1)^k f_{\chi,a}^{(k)}(0) = -\chi(-1)f_{\chi,a}^{(k)} (0), forcing f_{\chi,a}^{(k)}(0) = 0 unless \chi(-1)(-1)^k = -1. (In particular this recovers the classical vanishing L(\chi,-k)=0 when \chi(-1)(-1)^k = 1.)