5.3. Analytic functions on Zp via the Mellin transform
We now translate measures on \Zpx into analytic functions on \Zp, recovering
the question posed at the outset: p-adic analytic functions interpolating
\zeta(1-k). The price is that no single analytic function captures all k;
instead there are p-1 branches, one for each residue class modulo p-1.
The obstruction is that the naive definition x \mapsto x^s = \exp(s\log x)
fails: the p-adic exponential does not converge on all of \Zpx.
The p-adic exponential converges on p\Zp. Consequently, for every s \in
\Zp the map 1 + p\Zp \to \Zp, x \mapsto x^s := \exp(s\log x), is
well-defined.
In the formalisation padicExp/padicLog are developed over any complete
ultrametric \Qp-algebra field (convergence, isometry, functional
equations, and the exp/log inversion on the open ball
\|x\|^{p-1} < p^{-1}), padicExp_converges_on_pZp is the first
sentence for odd p, and padicExp_smul_padicLog_eq_onePAdicPow both
realises the well-definedness of x^s = \exp(s\log x) on ℤ_p and proves
it EQUAL to the continuous-character construction PadicInt.onePAdicPow
used throughout §5.3 (uniqueness of continuous additive characters; this
discharges the recorded replan L5.3.3).
Lean code for Lemma5.3.1●2 theorems
Associated Lean declarations
-
theoremdefined in PadicLFunctions/PadicExp.leancomplete
theorem PadicLFunctions.padicExp_converges_on_pZp (p : ℕ) [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) {x : ℤ_[p]} (hx : x ∈ Ideal.span {↑p}) : Summable fun n ↦ (↑n.factorial)⁻¹ • ↑x ^ n
theorem PadicLFunctions.padicExp_converges_on_pZp (p : ℕ) [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) {x : ℤ_[p]} (hx : x ∈ Ideal.span {↑p}) : Summable fun n ↦ (↑n.factorial)⁻¹ • ↑x ^ n
**RJW Lemma 5.14, first half** (TeX 1892–1893): "The p-adic exponential map converges on `pℤ_p`" — for odd `p`, `pℤ_[p]` lies in the convergence ball (`‖x‖ ≤ p⁻¹ < p^{−1/(p−1)}`). Stated on `ℤ_[p]` (the `L = ℚ_[p]`-instance restricted to integers; `exp` of a multiple of `p` is again integral by the isometry). -
theoremdefined in PadicLFunctions/PadicExp.leancomplete
theorem PadicLFunctions.padicExp_smul_padicLog_eq_onePAdicPow (p : ℕ) [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) {x : ℤ_[p]} (hx : x - 1 ∈ Ideal.span {↑p}) (s : ℤ_[p]) : PadicLFunctions.pZpExp p (s * PadicLFunctions.pZpLog p x) = (PadicInt.onePAdicPow p x hx) s
theorem PadicLFunctions.padicExp_smul_padicLog_eq_onePAdicPow (p : ℕ) [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) {x : ℤ_[p]} (hx : x - 1 ∈ Ideal.span {↑p}) (s : ℤ_[p]) : PadicLFunctions.pZpExp p (s * PadicLFunctions.pZpLog p x) = (PadicInt.onePAdicPow p x hx) s
**RJW Lemma 5.14, second half** (TeX 1893–1894): "for any `s ∈ ℤ_p`, the function `1+pℤ_p → ℤ_p` given by `x ↦ x^s := exp(s·log(x))` is well-defined" — and it agrees with the character construction `PadicInt.onePAdicPow` (uniqueness of continuous additive characters with a given value at `1`; decomposition E5).
This is standard local field theory: \exp converges on the disc |z| <
p^{-1/(p-1)}, which for odd p contains p\Zp, while \log maps 1+p\Zp
into p\Zp. Hence \exp(s\log x) makes sense for x \in 1+p\Zp and s \in
\Zp, and standard properties of \exp and \log show it has the expected
behaviour of an exponential.
-
PadicInt.teichmuller[complete] -
PadicInt.angleUnit[complete] -
PadicInt.teichmuller_mul_angleUnit[complete] -
PadicInt.eq_one_of_pow_card_sub_one[complete]
For odd p there is a decomposition \Zpx \cong \mu_{p-1}\times(1+p\Zp). The
Teichmüller character \omega : \Zpx \to \mu_{p-1} sends x to the
Teichmüller lift of its reduction modulo p, and the projection
\ang{\,\cdot\,} : \Zpx \to 1+p\Zp is given by \ang{x} := \omega^{-1}(x)\,x.
Every x\in\Zpx factors as x = \omega(x)\ang{x}. This uses
Lemma 5.3.1.
In the formalisation \omega is PadicInt.teichmuller : ℤ_[p]ˣ →* ℤ_[p]ˣ,
built through mathlib's Perfection.teichmuller₀ (whose construction is the
adic limit of p^n-th powers of lifts, i.e. \omega(x) = \lim_n x^{p^n});
\mu_{p-1}-valuedness is teichmullerFun_pow_card_sub_one, the 1+p\Zp
membership of \ang{x} is angleUnit_sub_one_mem, and uniqueness of the
factorisation is eq_one_of_pow_card_sub_one (\mu_{p-1}\cap(1+p\Zp)=1).
Lean code for Definition5.3.2●4 declarations
Associated Lean declarations
-
PadicInt.teichmuller[complete]
-
PadicInt.angleUnit[complete]
-
PadicInt.teichmuller_mul_angleUnit[complete]
-
PadicInt.eq_one_of_pow_card_sub_one[complete]
-
PadicInt.teichmuller[complete] -
PadicInt.angleUnit[complete] -
PadicInt.teichmuller_mul_angleUnit[complete] -
PadicInt.eq_one_of_pow_card_sub_one[complete]
-
defdefined in PadicLFunctions/Interpolation/Branches.leancomplete
def PadicInt.teichmuller (p : ℕ) [hp : Fact (Nat.Prime p)] : ℤ_[p]ˣ →* ℤ_[p]ˣ
def PadicInt.teichmuller (p : ℕ) [hp : Fact (Nat.Prime p)] : ℤ_[p]ˣ →* ℤ_[p]ˣ
L5.3.1 (packaged): the Teichmüller character `ω : ℤ_[p]ˣ →* ℤ_[p]ˣ`.
-
defdefined in PadicLFunctions/Interpolation/Branches.leancomplete
def PadicInt.angleUnit (p : ℕ) [hp : Fact (Nat.Prime p)] (x : ℤ_[p]ˣ) : ℤ_[p]ˣ
def PadicInt.angleUnit (p : ℕ) [hp : Fact (Nat.Prime p)] (x : ℤ_[p]ˣ) : ℤ_[p]ˣ
L5.3.2: the projection `⟨·⟩ : ℤ_[p]ˣ → 1 + pℤ_[p]`, `⟨x⟩ = ω(x)⁻¹·x` (RJW Def 5.15). Valued in units; the `1 + pℤ_p` membership is the lemma below.
-
theoremdefined in PadicLFunctions/Interpolation/Branches.leancomplete
theorem PadicInt.teichmuller_mul_angleUnit (p : ℕ) [hp : Fact (Nat.Prime p)] (x : ℤ_[p]ˣ) : (PadicInt.teichmuller p) x * PadicInt.angleUnit p x = x
theorem PadicInt.teichmuller_mul_angleUnit (p : ℕ) [hp : Fact (Nat.Prime p)] (x : ℤ_[p]ˣ) : (PadicInt.teichmuller p) x * PadicInt.angleUnit p x = x
The decomposition `x = ω(x)·⟨x⟩` (RJW Def 5.15: "If `x ∈ ℤ_p^×`, then we can write `x = ω(x)⟨x⟩`").
-
theoremdefined in PadicLFunctions/Interpolation/Branches.leancomplete
theorem PadicInt.eq_one_of_pow_card_sub_one (p : ℕ) [hp : Fact (Nat.Prime p)] {u : ℤ_[p]ˣ} (hu : u ^ (p - 1) = 1) (hmem : ↑u - 1 ∈ Ideal.span {↑p}) : u = 1
theorem PadicInt.eq_one_of_pow_card_sub_one (p : ℕ) [hp : Fact (Nat.Prime p)] {u : ℤ_[p]ˣ} (hu : u ^ (p - 1) = 1) (hmem : ↑u - 1 ∈ Ideal.span {↑p}) : u = 1
Uniqueness of the decomposition: an element of `μ_{p−1} ∩ (1+pℤ_p)` is `1`. For `p = 2` this is degenerate-but-true (`p − 1 = 1`); the substantive odd-`p` case rests on `(1+pℤ_p)` being torsion-free for prime-to-`p` exponents (RJW TeX 1900: "Recall that we assume `p` to be odd"). Proved through the character `s ↦ u^s`: `u^{(p−1)s}` is the trivial character by uniqueness, and evaluating at `(p−1)⁻¹` gives `u = 1`.
Because the p-adic exponential converges on p\Zp, the map x \mapsto
\ang{x}^s is well-defined for all s \in \Zp, so for each i the assignment
s \mapsto [x \mapsto \omega(x)^i\ang{x}^s] embeds \Zp into the continuous
characters of \Zpx.
-
PadicLFunctions.branchChar[complete] -
PadicLFunctions.zetaPBranch[complete]
For each i = 1, \dots, p-1 the i-th branch of the p-adic zeta function
is
\zeta_{p,i} : \Zp \to \Cp, \qquad \zeta_{p,i}(s) =
\int_{\Zpx}\omega(x)^i\,\ang{x}^{1-s}\cdot\zetap.
This uses Definition 4.3.2 and Definition 5.3.2.
In the formalisation the character x \mapsto \omega(x)^i\ang{x}^{1-s} is
branchChar (with \ang{x}^s the continuous-character realisation of the
recorded replan L5.3.3), values are taken in \Qp rather than \Cp (the
running \Zp-coefficient convention), and the integral against the
pseudo-measure \zetap is realised through its canonical witness:
zetaPBranch pairs branchChar with zetaNum at the fixed topological
generator and divides by the unit pairing, with junk value at the pole
(i,s) = (0,1) (RJW's "meromorphic").
Lean code for Definition5.3.3●2 definitions
Associated Lean declarations
-
PadicLFunctions.branchChar[complete]
-
PadicLFunctions.zetaPBranch[complete]
-
PadicLFunctions.branchChar[complete] -
PadicLFunctions.zetaPBranch[complete]
-
defdefined in PadicLFunctions/Interpolation/Branches.leancomplete
def PadicLFunctions.branchChar (p : ℕ) [hp : Fact (Nat.Prime p)] (i : ℕ) (s : ℤ_[p]) : C(ℤ_[p]ˣ, ℤ_[p])
def PadicLFunctions.branchChar (p : ℕ) [hp : Fact (Nat.Prime p)] (i : ℕ) (s : ℤ_[p]) : C(ℤ_[p]ˣ, ℤ_[p])
L5.3.4: the continuous character `x ↦ ω(x)^i·⟨x⟩^s` on `ℤ_[p]ˣ`, as a continuous map into `ℤ_[p]` (RJW TeX 1907–1910).
-
defdefined in PadicLFunctions/Interpolation/Branches.leancomplete
def PadicLFunctions.zetaPBranch (p : ℕ) [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) (i : ℕ) (s : ℤ_[p]) : ℚ_[p]
def PadicLFunctions.zetaPBranch (p : ℕ) [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) (i : ℕ) (s : ℤ_[p]) : ℚ_[p]
L5.3.5/L5.3.6: the `i`-th branch of the Kubota–Leopoldt `p`-adic L-function: `ζ_{p,i}(s) = ∫_{ℤ_p^×} ω(x)^i⟨x⟩^{1−s}·ζ_p` (RJW Def 5.16, TeX 1912–1918), realised through the pseudo-measure pairing at the §4 topological generator and its canonical witness `zetaNum` (junk value where the pairing degenerates, i.e. at the pole `(i,s) = (0,1)` — RJW's "meromorphic").
For all k \geq 1 with k \equiv i \pmod{p-1},
\zeta_{p,i}(1-k) = (1 - p^{k-1})\,\zeta(1-k).
This uses Definition 5.3.3, Definition 4.3.2 and
Corollary 2.3.4.
Lean code for Theorem5.3.4●1 theorem
Associated Lean declarations
-
theoremdefined in PadicLFunctions/Interpolation/Branches.leancomplete
theorem PadicLFunctions.zetaPBranch_interpolation (p : ℕ) [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) {i k : ℕ} (hk : 0 < k) (hik : ↑k = ↑i) : PadicLFunctions.zetaPBranch p hp2 i (1 - ↑k) = (1 - ↑p ^ (↑k - 1)) * ↑(zetaNeg (k - 1))
theorem PadicLFunctions.zetaPBranch_interpolation (p : ℕ) [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) {i k : ℕ} (hk : 0 < k) (hik : ↑k = ↑i) : PadicLFunctions.zetaPBranch p hp2 i (1 - ↑k) = (1 - ↑p ^ (↑k - 1)) * ↑(zetaNeg (k - 1))
**RJW Theorem 5.17** (`thm:kubota leopoldt analytic`, TeX 1921–1924): "For all `k ≥ 1` with `k ≡ i mod (p−1)`, we have `ζ_{p,i}(1−k) = (1−p^{k−1})ζ(1−k)`." The right-hand side is §4's rational `zetaNeg (k−1)` (the same value object as `PadicMeasure.kubotaLeopoldt`; the identification with the Riemann zeta function is `zetaNeg_eq_riemannZeta` in `KubotaLeopoldt/ZetaValuesComplex.lean`).
The monomial character x \mapsto x^k factors as \omega(x)^i\ang{x}^k
precisely when k \equiv i \pmod{p-1}, and in that case it equals the value of
\omega(x)^i\ang{x}^{1-s} at s = 1-k. Substituting s = 1-k into the
definition of \zeta_{p,i} therefore gives \zeta_{p,i}(1-k) =
\int_{\Zpx}x^k\cdot\zetap. The defining interpolation property of the
Kubota–Leopoldt pseudo-measure Definition 4.3.2 — the trivial-conductor
case \int_{\Zpx}x^k\cdot\zetap = (1-p^{k-1})\zeta(1-k) — then evaluates this to
(1-p^{k-1})\zeta(1-k).
Note that (as RJW record after the theorem) \zeta_{p,i} is identically zero
whenever i is odd: \zeta(1-k) vanishes for every odd k \geq 1, and the
congruence k \equiv i \pmod{p-1} forces such k to be odd exactly when
i is (as p-1 is even). Identical vanishing on all of \Zp further uses
the continuity of \zeta_{p,i} in s; the formalisation records the
interpolation formula itself.
We package the most general statement using the measure \zeta_\eta.
-
PadicLFunctions.MeasureR.LpFunction[complete]
Let \theta = \chi\eta be a Dirichlet character with \eta of conductor D
prime to p and \chi of conductor p^n, n \geq 0. The p-adic
L-function of \theta is
L_p(\theta, s) := \int_{\Zpx}\chi(x)\,\ang{x}^{1-s}\cdot\zeta_\eta, \qquad s \in
\Zp.
Equivalently, in terms of the unshifted measure \mu_\eta,
L_p(\theta,s) = \int_{\Zpx}\chi\omega^{-1}(x)\,\ang{x}^{-s}\cdot\mu_\eta =
\int_{\Zpx}\chi\omega^{s-1}(x)\,x^{-s}\cdot\mu_\eta.
This uses Definition 5.2.7 and Definition 5.3.2.
In the formalisation LpFunction takes values in an ambient complete
ultrametric \Qp-algebra K (standing in for the notes' \Cp), pairs
zetaEtaCleared with the character χ̃(x)·⟨x⟩^{1−s} and divides the
Gauss-sum clearing back out; the eq:alternative description in terms of
\mu_\eta is the route taken by the interpolation proof.
Lean code for Definition5.3.5●1 definition
Associated Lean declarations
-
PadicLFunctions.MeasureR.LpFunction[complete]
-
PadicLFunctions.MeasureR.LpFunction[complete]
-
defdefined in PadicLFunctions/Interpolation/LpFunction.leancomplete
def PadicLFunctions.MeasureR.LpFunction.{u_1} (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [NormedField K] [NormedAlgebra ℚ_[p] K] [IsUltrametricDist K] [CompleteSpace K] {D : ℕ} [NeZero D] (η : DirichletCharacter (↥(PadicLFunctions.integerRing K)) D) {ζ : ↥(PadicLFunctions.integerRing K)} (hζ : IsPrimitiveRoot ζ D) (hD : ¬p ∣ D) {n : ℕ} (χ : DirichletCharacter (↥(PadicLFunctions.integerRing K)) (p ^ n)) (s : ℤ_[p]) : K
def PadicLFunctions.MeasureR.LpFunction.{u_1} (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [NormedField K] [NormedAlgebra ℚ_[p] K] [IsUltrametricDist K] [CompleteSpace K] {D : ℕ} [NeZero D] (η : DirichletCharacter (↥(PadicLFunctions.integerRing K)) D) {ζ : ↥(PadicLFunctions.integerRing K)} (hζ : IsPrimitiveRoot ζ D) (hD : ¬p ∣ D) {n : ℕ} (χ : DirichletCharacter (↥(PadicLFunctions.integerRing K)) (p ^ n)) (s : ℤ_[p]) : K
RJW Def 5.18 (TeX 1929–1932): the `p`-adic L-function `L_p(θ,s) = ∫_{ℤ_p^×} χ(x)⟨x⟩^{1−s}·ζ_η` of `θ = χη`, as a `K`-value (the Gauss-sum clearing of `μ̃_η` is divided back out; `χ` enters through its locally constant extension to `ℤ_p`, restricted to the units).
For all k \geq 1,
L_p(\theta, 1-k) = \big(1 - \theta\omega^{-k}(p)\,p^{k-1}\big)\,
L(\theta\omega^{-k}, 1-k).
This uses Definition 5.3.5, Lemma 5.2.5,
Lemma 5.2.6 and Definition 2.1.3.
In the formalisation \theta\omega^{-k} is realised at its conductor: the
p-part \chi\omega^{-k} enters through its primitive core χ'
(supplied by exists_primitive_pPow_factorisation), and the right-hand side
is the L-value of \eta\cdot\chi' exactly as in the final display of
Definition 5.2.7; the §5.2 standing hypothesis D > 1 applies.
Lean code for Theorem5.3.6●1 theorem
Associated Lean declarations
-
theoremdefined in PadicLFunctions/Interpolation/LpFunction.leancomplete
theorem PadicLFunctions.MeasureR.Lp_interpolation.{u_1} {p : ℕ} [hp : Fact (Nat.Prime p)] {K : Type u_1} [NormedField K] [NormedAlgebra ℚ_[p] K] [IsUltrametricDist K] [CompleteSpace K] [CharZero K] {D : ℕ} [NeZero D] (hD1 : 1 < D) {η : DirichletCharacter (↥(PadicLFunctions.integerRing K)) D} (hη : η.IsPrimitive) {ζ : ↥(PadicLFunctions.integerRing K)} (hζ : IsPrimitiveRoot ζ D) (hD : ¬p ∣ D) {n : ℕ} {χ : DirichletCharacter (↥(PadicLFunctions.integerRing K)) (p ^ n)} (_hχ : χ.IsPrimitive) {ε : ↥(PadicLFunctions.integerRing K)} (hε : IsPrimitiveRoot ε (p ^ max n 1)) {k : ℕ} (hk : 0 < k) {m : ℕ} (hmle : m ≤ max n 1) {χ' : DirichletCharacter (↥(PadicLFunctions.integerRing K)) (p ^ m)} (hχ'prim : χ'.IsPrimitive) (hχ' : PadicLFunctions.MeasureR.twistedPChar p K χ k = (DirichletCharacter.changeLevel ⋯) χ') {θ' : DirichletCharacter (↥(PadicLFunctions.integerRing K)) (D * p ^ m)} (hθ' : θ' = (DirichletCharacter.changeLevel ⋯) η * (DirichletCharacter.changeLevel ⋯) χ') : PadicLFunctions.MeasureR.LpFunction p K η hζ hD χ (1 - ↑k) = (1 - ↑(θ' ↑p) * ↑p ^ (k - 1)) * PadicLFunctions.LvalNeg (PadicLFunctions.MeasureR.toFieldChar θ') (k - 1)
theorem PadicLFunctions.MeasureR.Lp_interpolation.{u_1} {p : ℕ} [hp : Fact (Nat.Prime p)] {K : Type u_1} [NormedField K] [NormedAlgebra ℚ_[p] K] [IsUltrametricDist K] [CompleteSpace K] [CharZero K] {D : ℕ} [NeZero D] (hD1 : 1 < D) {η : DirichletCharacter (↥(PadicLFunctions.integerRing K)) D} (hη : η.IsPrimitive) {ζ : ↥(PadicLFunctions.integerRing K)} (hζ : IsPrimitiveRoot ζ D) (hD : ¬p ∣ D) {n : ℕ} {χ : DirichletCharacter (↥(PadicLFunctions.integerRing K)) (p ^ n)} (_hχ : χ.IsPrimitive) {ε : ↥(PadicLFunctions.integerRing K)} (hε : IsPrimitiveRoot ε (p ^ max n 1)) {k : ℕ} (hk : 0 < k) {m : ℕ} (hmle : m ≤ max n 1) {χ' : DirichletCharacter (↥(PadicLFunctions.integerRing K)) (p ^ m)} (hχ'prim : χ'.IsPrimitive) (hχ' : PadicLFunctions.MeasureR.twistedPChar p K χ k = (DirichletCharacter.changeLevel ⋯) χ') {θ' : DirichletCharacter (↥(PadicLFunctions.integerRing K)) (D * p ^ m)} (hθ' : θ' = (DirichletCharacter.changeLevel ⋯) η * (DirichletCharacter.changeLevel ⋯) χ') : PadicLFunctions.MeasureR.LpFunction p K η hζ hD χ (1 - ↑k) = (1 - ↑(θ' ↑p) * ↑p ^ (k - 1)) * PadicLFunctions.LvalNeg (PadicLFunctions.MeasureR.toFieldChar θ') (k - 1)
**RJW Theorem 5.19** (`TheoremLeopoldtAnalyticTwist`, TeX 1943–1946): "For all `k ≥ 1`, we have `L_p(θ,1−k) = (1 − θω^{−k}(p)p^{k−1})L(θω^{−k},1−k)`." Here `χ'` is the primitive core of the `p`-part `χ·ω^{−k}` of `θω^{−k}` (a factorisation supplied by `exists_primitive_pPow_factorisation`), and `θ' = η·χ'` realises `θω^{−k}` at its conductor, so `L(θω^{−k},1−k)` is `LvalNeg (toFieldChar θ') (k−1)` exactly as in `zetaEta_twisted_moments`.
Use the equivalent description of Definition 5.3.5. From x =
\omega(x)\ang{x} one computes \chi\omega^{-1}(x)\ang{x}^{k-1} = \chi\omega^{-k}
(x)\,\omega^{k-1}(x)\ang{x}^{k-1} = \chi\omega^{-k}(x)\,x^{k-1}. Hence L_p(\theta,
1-k) = \int_{\Zpx}\chi\omega^{-k}(x)\,x^{k-1}\cdot\mu_\eta. Writing \psi :=
\chi\omega^{-k} for the p-power-conductor character and \theta\omega^{-k} =
\psi\eta, the twisted moment \int_{\Zpx}\psi(x)x^{k-1}\cdot\mu_\eta is computed
exactly as in the non-tame proof: forming the twist \mu_{\psi\eta} =
(\mu_\eta)_\psi with its Mahler transform Lemma 5.2.6 and
applying the restriction-interpolation Lemma 5.2.5 to it
gives \int_{\Zpx}\psi(x)x^{k-1}\cdot\mu_\eta = (1-\theta\omega^{-k}(p)p^{k-1})
L(\theta\omega^{-k},1-k).
Note that (as RJW record after the theorem) directly from the definitions
\zeta_{p,i}(s) = L_p(\omega^i, s), so for arbitrary k > 0 the theorem
gives \zeta_{p,i}(1-k) = (1-\omega^{i-k}(p)p^{k-1})L(\omega^{i-k},1-k),
recovering the branch interpolation when k \equiv i \pmod{p-1} (where
\omega^{i-k} is trivial). The formalisation keeps the two routes separate:
\zeta_{p,i} is built from the §4 pseudo-measure \zetap (tame conductor
D = 1), while L_p integrates against the genuine measure \zeta_\eta
of the D > 1 theory, so this identification is prose-level only.
Finally, the construction \zeta_{p,i} is an instance of a general transform.
- No associated Lean code or declarations.
For any measure \mu on \Zpx and i \in \{1,\dots,p-1\}, the Mellin
transform of \mu at i is the function
\Mellin_{\mu,i}(s) := \int_{\Zpx}\omega(x)^i\,\ang{x}^s\cdot\mu, \qquad s \in
\Zp.
It converts p-adic measures on \Zpx into analytic functions on \Zp; one
has \zeta_{p,i}(s) = \Mellin_{\zetap,i}(1-s). This uses
Definition 5.3.2 and Definition 5.3.3.