7.2. Unwinding the pseudo-measure
Recall from the construction of \zp that, for any topological generator a
of \Zpx,
\zp = \frac{x^{-1}\,\Res_{\Zpx}(\mu_a)}{[a]-[1]},
where the \mu_a are the Kubota–Leopoldt measures. Using
the rule \int_G \chi\cdot\lambda = (\chi(g)-1)^{-1}\int_G \chi\cdot([g]-[1])\lambda
for integrating a pseudo-measure \lambda against a non-trivial character, and
the identity \ang{x} = \Teich^{-1}(x)\,x, the branch \zpi becomes a ratio.
For i \in \set{1,\ldots,p-1} define the denominator
g_{a,i}(s) := \Teich(a)^{i}\,\ang{a}^{1-s} - 1.
Substituting \zp = x^{-1}\Res_{\Zpx}(\mu_a)/([a]-[1]) into the definition of
\zpi and integrating the pseudo-measure yields the closed form
\zpi(s) = \frac{\int_{\Zpx} \Teich(x)^{s+i-1}\,x^{-s}\cdot \mu_a}{g_{a,i}(s)}.
This rests on Definition 4.3.2, Definition 4.1.4 and
Definition 3.6.1.
In the formalisation the closed form is the definition: zetaPBranch was
defined in the interpolation chapter as exactly this ratio
g_{a,i}(s)^{-1}\int\Teich(x)^i\ang{x}^{1-s}\mu_a-numerator at the canonical
topological generator, so no separate unwinding step is needed; g_{a,i}
appears inline as its denominator.
Lean code for Definition7.2.1●1 definition
Associated Lean declarations
-
PadicLFunctions.zetaPBranch[complete]
-
PadicLFunctions.zetaPBranch[complete]
-
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").
-
PadicLFunctions.branch_denom_ne_zero[complete] -
PadicLFunctions.tendsto_branch_denom_div[complete] -
PadicLFunctions.teichmuller_isPrimitiveRoot[complete]
With g_{a,i} as above:
-
(i) If
i \neq p-1, theng_{a,i}(1) \neq 0. Consequently Theorem (i) holds. -
(ii)
g_{a,p-1}(1) = 0, and\lim_{s\to 1} (s-1)^{-1}\,g_{a,p-1}(s) = -\logp(a).
This depends on Definition 7.2.1 and Definition 5.3.2.
The Lean statement of (i), branch_denom_ne_zero, is strengthened from
s=1 to every s (the ultrametric isoceles argument is uniform in
s); (ii) is proved through the exponential/logarithm bridge
\ang{a}^{1-s}=\exp((1-s)\logp\ang{a}) and the quadratic tail bound
\norm{\exp w - 1 - w}\le p\norm{w}^2, rather than the notes' binomial-series
manipulation (decomposition R7, replan 3) — the limit and its value are
identical.
Lean code for Lemma7.2.2●3 theorems
Associated Lean declarations
-
PadicLFunctions.branch_denom_ne_zero[complete]
-
PadicLFunctions.tendsto_branch_denom_div[complete]
-
PadicLFunctions.teichmuller_isPrimitiveRoot[complete]
-
PadicLFunctions.branch_denom_ne_zero[complete] -
PadicLFunctions.tendsto_branch_denom_div[complete] -
PadicLFunctions.teichmuller_isPrimitiveRoot[complete]
-
theoremdefined in PadicLFunctions/ResidueZeta.leancomplete
theorem PadicLFunctions.branch_denom_ne_zero (p : ℕ) [hp : Fact (Nat.Prime p)] {u : ℤ_[p]ˣ} (hgen : ∀ (n : ℕ), Subgroup.zpowers ((PadicMeasure.unitsToZModPow p n) u) = ⊤) {i : ℕ} (hi0 : 0 < i) (hi : i < p - 1) (s : ℤ_[p]) : ↑((PadicLFunctions.branchChar p i s) u) - 1 ≠ 0
theorem PadicLFunctions.branch_denom_ne_zero (p : ℕ) [hp : Fact (Nat.Prime p)] {u : ℤ_[p]ˣ} (hgen : ∀ (n : ℕ), Subgroup.zpowers ((PadicMeasure.unitsToZModPow p n) u) = ⊤) {i : ℕ} (hi0 : 0 < i) (hi : i < p - 1) (s : ℤ_[p]) : ↑((PadicLFunctions.branchChar p i s) u) - 1 ≠ 0
R7.2b: for `0 < i < p−1` the branch denominator never vanishes — `‖ω(u)^i − 1‖ = 1` beats `‖⟨u⟩^{1−s} − 1‖ < 1` (ultrametric isoceles); this is RJW's Lemma 7.2(i) strengthened from `s = 1` to all `s`. -
theoremdefined in PadicLFunctions/ResidueZeta.leancomplete
theorem PadicLFunctions.tendsto_branch_denom_div (p : ℕ) [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) {u : ℤ_[p]ˣ} : Filter.Tendsto (fun s ↦ (↑s - 1)⁻¹ * (↑((PadicLFunctions.branchChar p (p - 1) (1 - s)) u) - 1)) (nhdsWithin 1 {s | s ≠ 1}) (nhds (-↑(PadicLFunctions.pZpLog p ↑(PadicInt.angleUnit p u))))
theorem PadicLFunctions.tendsto_branch_denom_div (p : ℕ) [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) {u : ℤ_[p]ˣ} : Filter.Tendsto (fun s ↦ (↑s - 1)⁻¹ * (↑((PadicLFunctions.branchChar p (p - 1) (1 - s)) u) - 1)) (nhdsWithin 1 {s | s ≠ 1}) (nhds (-↑(PadicLFunctions.pZpLog p ↑(PadicInt.angleUnit p u))))
R7.2c (RJW Lemma 7.2(ii), TeX 2224–2226): the denominator has a simple zero at `s = 1` with derivative `−log_p⟨a⟩`: `(s−1)⁻¹·(⟨a⟩^{1−s} − 1) → −log_p⟨a⟩` as `s → 1`, `s ≠ 1`. -
theoremdefined in PadicLFunctions/ResidueZeta.leancomplete
theorem PadicLFunctions.teichmuller_isPrimitiveRoot (p : ℕ) [hp : Fact (Nat.Prime p)] {u : ℤ_[p]ˣ} (hgen : ∀ (n : ℕ), Subgroup.zpowers ((PadicMeasure.unitsToZModPow p n) u) = ⊤) : IsPrimitiveRoot ((PadicInt.teichmuller p) u) (p - 1)
theorem PadicLFunctions.teichmuller_isPrimitiveRoot (p : ℕ) [hp : Fact (Nat.Prime p)] {u : ℤ_[p]ˣ} (hgen : ∀ (n : ℕ), Subgroup.zpowers ((PadicMeasure.unitsToZModPow p n) u) = ⊤) : IsPrimitiveRoot ((PadicInt.teichmuller p) u) (p - 1)
R7.2a: the Teichmüller value of a topological generator is a primitive `(p−1)`-th root of unity (its reduction generates `(ZMod p)ˣ`).
Since a is a topological generator of \Zpx, its image \Teich(a) is a
primitive (p-1)-th root of unity. At s=1 the factor \ang{a}^{1-s}=1,
so g_{a,i}(1) = \Teich(a)^{i}-1, which vanishes exactly when (p-1)\mid i,
i.e. when i=p-1. This proves (i): the closed form of Definition 7.2.1
then has a non-vanishing denominator at s=1 and is therefore analytic there.
For (ii), with i=p-1 we have \Teich(a)^{p-1}=1, so
g_{a,p-1}(s) = \ang{a}^{1-s}-1. Expanding the binomial series in
(\ang{a}-1) gives
g_{a,p-1}(s) = \sum_{n\ge 1}\binom{1-s}{n}(\ang{a}-1)^n = (1-s)\sum_{n\ge 1}\frac{1}{n}\binom{-s}{n-1}(\ang{a}-1)^n,
using \binom{1-s}{n} = \tfrac{1-s}{n}\binom{-s}{n-1}. As s\to 1 the
remaining sum tends to its value at s=1, namely
\sum_{n\ge 1}\frac{(-1)^{n-1}}{n}(\ang{a}-1)^n = \logp(\ang{a}) = \logp(a),
where \binom{-1}{n-1}=(-1)^{n-1} and \logp(\ang{a})=\logp(a) because
\logp\Teich(a)=0. Hence \lim_{s\to1}(s-1)^{-1}g_{a,p-1}(s) = -\logp(a).
Combining Lemma 7.2.2(ii) with the closed form
Definition 7.2.1 of \zeta_{p,p-1},
\lim_{s\to 1} (s-1)\,\zeta_{p,p-1}(s) = -\frac{\int_{\Zpx} x^{-1}\cdot \mu_a}{\logp(a)}.
(Not a standalone Lean declaration: this limit-algebra step — the inverse of
the denominator limit times the continuous numerator — is inlined in the proof
of tendsto_sub_one_mul_zetaPBranch, together with the nonvanishing
\logp(a)=\logp\ang{a}\neq 0 for a topological generator.)
In the closed form \zeta_{p,p-1}(s) = \big(\int_{\Zpx}\Teich(x)^{s+p-2}x^{-s}\mu_a\big)/g_{a,p-1}(s)
of Definition 7.2.1, the numerator is analytic in s and at s=1
equals \int_{\Zpx} x^{-1}\cdot\mu_a (since \Teich(x)^{p-1}=1 makes the
integrand \Teich(x)^{p-1}x^{-1}=x^{-1}). The denominator g_{a,p-1}(s)
vanishes to first order at s=1. Multiplying by (s-1) and using
Lemma 7.2.2(ii), which gives (s-1)/g_{a,p-1}(s) \to 1/(-\logp(a)),
the analytic numerator passes through the limit and yields the stated formula.