4.3. Rescaling and removing the dependence on a
Thus far the parameter a has played the role of the smoothing factor that
removes the pole of \zeta at s=1. To eliminate a we must permit simple
poles on the p-adic side, which is exactly what Definition 3.6.1
pseudo-measures allow. The interpolation formula
Proposition 4.2.2 features the factor a^{k+1}-1, whereas
the natural augmentation element \thetaa of the Iwasawa algebra produces
a^k - 1; the gap is bridged by multiplication by x^{-1}.
-
PadicMeasure.zetaNum_moments[complete]
For a an integer coprime to p, let \thetaa \in \Lam(\Zpx) be the element
corresponding to [a] - [1] (in the formalisation: dirac p a - 1; the
x^{-1}-multiplication is unitsCmul/invCM, and the displayed moment formula is
zetaNum_moments), so that
\int_{\Zpx} x^k \cdot \thetaa = a^k - 1.$$
On \Zpx there is a well-defined operation multiplication by x^{-1}, given on
measures by \int_{\Zpx} f(x)\cdot x^{-1}\mu := \int_{\Zpx} x^{-1}f(x)\cdot\mu,
and, combining this shift with Proposition 4.2.2, one
computes
\int_{\Zpx} x^k \cdot x^{-1}\mua = \int_{\Zpx} x^{k-1}\cdot\mua = (-1)^k\,(a^k - 1)\,(1 - p^{k-1})\,\zeta(1-k).$$
This uses the Definition 3.3.3 structure of \Lam(\Zpx).
Lean code for Definition4.3.1●1 theorem
Associated Lean declarations
-
PadicMeasure.zetaNum_moments[complete]
-
PadicMeasure.zetaNum_moments[complete]
-
theoremdefined in PadicLFunctions/KubotaLeopoldt/ZetaP.leancomplete
theorem PadicMeasure.zetaNum_moments (p : ℕ) [hp : Fact (Nat.Prime p)] {a : ℕ} (hpa : ¬p ∣ a) {k : ℕ} (hk : 0 < k) : ↑((PadicMeasure.zetaNum p a) (PadicMeasure.unitsPowCM p k)) = (-1) ^ k * (↑a ^ k - 1) * (1 - ↑p ^ (k - 1)) * ↑(zetaNeg (k - 1))
theorem PadicMeasure.zetaNum_moments (p : ℕ) [hp : Fact (Nat.Prime p)] {a : ℕ} (hpa : ¬p ∣ a) {k : ℕ} (hk : 0 < k) : ↑((PadicMeasure.zetaNum p a) (PadicMeasure.unitsPowCM p k)) = (-1) ^ k * (↑a ^ k - 1) * (1 - ↑p ^ (k - 1)) * ↑(zetaNeg (k - 1))
RJW TeX line 1561: `∫_{ℤ_p^×} x^k · x⁻¹μ_a = (−1)^k (a^k−1)(1−p^{k−1}) ζ(1−k)`.
Let a be a topological generator of \Zpx. The p-adic zeta function
(the Kubota–Leopoldt p-adic L-function) is the element
\zetap := \frac{x^{-1}\,\Res_{\Zpx}\mua}{\thetaa} \in Q(\Zpx)$$
of the fraction ring of the Definition 3.3.3 \Lam(\Zpx), where
\mua is the measure Definition 4.1.4 and \thetaa is the augmentation
element Definition 4.3.1.
Lean code for Definition4.3.2●1 definition
Associated Lean declarations
-
PadicMeasure.padicZeta[complete]
-
PadicMeasure.padicZeta[complete]
-
defdefined in PadicLFunctions/KubotaLeopoldt/ZetaP.leancomplete
def PadicMeasure.padicZeta (p : ℕ) [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) : PadicMeasure.QuotientField p
def PadicMeasure.padicZeta (p : ℕ) [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) : PadicMeasure.QuotientField p
**RJW Def. 4.10 (`DefZetap`)**: the p-adic zeta function `ζ_p = (x⁻¹ Res_{ℤ_p^×} μ_a) / ([a] − [1]) ∈ Q(ℤ_p^×)`, for (a choice of) an integer topological generator `a` of `ℤ_p^×`.
The element \zetap is a well-defined pseudo-measure, independent of the choice
of topological generator a, satisfying
\int_{\Zpx} x^k \cdot \zetap = (1 - p^{k-1})\,\zeta(1-k) \qquad \text{for all } k > 0.$$
Lean code for Proposition4.3.3●1 theorem
Associated Lean declarations
-
PadicMeasure.padicZeta_moments[complete]
-
PadicMeasure.padicZeta_moments[complete]
-
theoremdefined in PadicLFunctions/KubotaLeopoldt/ZetaP.leancomplete
theorem PadicMeasure.padicZeta_moments (p : ℕ) [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) (b : ℤ_[p]ˣ) {k : ℕ} (hk : 0 < k) (ν : 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)) ν) : ↑(ν (PadicMeasure.unitsPowCM p k)) = (↑↑b ^ k - 1) * (1 - ↑p ^ (k - 1)) * ↑(zetaNeg (k - 1))
theorem PadicMeasure.padicZeta_moments (p : ℕ) [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) (b : ℤ_[p]ˣ) {k : ℕ} (hk : 0 < k) (ν : 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)) ν) : ↑(ν (PadicMeasure.unitsPowCM p k)) = (↑↑b ^ k - 1) * (1 - ↑p ^ (k - 1)) * ↑(zetaNeg (k - 1))
**RJW Prop. 4.11 (`PropInterpolation2`), interpolation**: every witness `ν` of `([b]−[1])·ζ_p ∈ Λ(ℤ_p^×)` has moments `∫ x^k ν = (b^k−1)(1−p^{k−1}) ζ(1−k)` — i.e. `∫_{ℤ_p^×} x^k ζ_p = (1−p^{k−1})ζ(1−k)` in the pseudo-measure moment encoding.
Write \nu := x^{-1}\Res_{\Zpx}\mua \in \Lam(\Zpx), so that
\zetap = \nu/\thetaa. Because \thetaa = [a]-[1] for the topological generator
a, every augmentation element [g]-[1] is a \Lam(\Zpx)-multiple of
\thetaa; hence ([g]-[1])\zetap \in \Lam(\Zpx) for all g, so \zetap is a
Definition 3.6.1 pseudo-measure. Integrating against x^k via the
pseudo-measure rule \int x^k\cdot\zetap = (a^k-1)^{-1}\int x^k\cdot\thetaa\zetap = (a^k-1)^{-1}\int x^k\cdot\nu,
and using \int_{\Zpx} x^k\cdot x^{-1}\Res_{\Zpx}\mua = (-1)^k(a^k-1)(1-p^{k-1})\zeta(1-k)
from Proposition 4.2.2 and Definition 4.3.1, the factor
a^k-1 cancels and we obtain
\int_{\Zpx} x^k \cdot \zetap = (-1)^k\,(1-p^{k-1})\,\zeta(1-k).$$
The sign (-1)^k may be dropped. Indeed \zeta(1-k) = -B_k/k, which vanishes
for every odd k \ge 3 (as B_k = 0 there); for even k the sign is already
(-1)^k = +1; and for k=1 the Euler factor 1-p^{k-1} = 1-p^0 = 0 kills the
whole expression. Hence (-1)^k = 1 wherever the right-hand side is non-zero,
and the interpolation formula follows. Finally, independence of a follows from
the rigidity of pseudo-measures on \Zpx: the values \int_{\Zpx} x^k\cdot(-)
for k>0 determine a pseudo-measure uniquely, and the resulting formula does not
involve a, so any two choices of topological generator yield the same \zetap.