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

5.2. Non-trivial tame conductors🔗

The previous theorem treats tame conductor 1. One can do better: for a Dirichlet character \eta of conductor D > 1 coprime to p, there is a genuine measure interpolating the twisted values L(\chi\eta, 1-k). Because L-functions of non-trivial characters are entire, no smoothing factor is needed and one obtains a measure rather than a pseudo-measure.

Definition5.2.1
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 5
Reverse dependency previews
Preview
Theorem 5.2.2
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N

Let D > 1 be coprime to p and \eta a primitive Dirichlet character of conductor D. Because no smoothing factor is needed (the relevant L-function is entire), set f_\eta(t) := \frac{-1}{G(\eta^{-1})}\sum_{c\in(\Z/D\Z)^\times} \frac{\eta(c)^{-1}}{e^t\eps_D^c - 1}, where the Gauss sum G(\eta^{-1}) is defined as before with p^n replaced by D. Substituting e^t = T+1 and expanding the geometric series gives F_\eta(T) := \frac{-1}{G(\eta^{-1})}\sum_{c\in(\Z/D\Z)^\times} \frac{\eta(c)^{-1}}{(1+T)\eps_D^c - 1} = \frac{-1}{G(\eta^{-1})} \sum_{c\in(\Z/D\Z)^\times}\eta(c)^{-1}\sum_{k\geq 0}\frac{\eps_D^{kc}} {(\eps_D^c-1)^{k+1}}\,T^k. This lies in \cO_L[[T]] for a sufficiently large finite extension L/\Qp containing the values of \eta: the Gauss sum is a p-adic unit because G(\eta)G(\eta^{-1}) = \eta(-1)D with D coprime to p, and \eps_D^c - 1 \in \cO_L^\times (its norm divides D). Let \mu_\eta \in \Lam(\Zp) be the measure with Mahler transform \Am_{\mu_\eta} = F_\eta. This uses Definition 5.1.3 and Definition 3.4.3.

In the formalisation the measure is carried in cleared form: muEtaCleared is -G(\eta^{-1})\,F_\eta read back through the Mahler isomorphism (mahlerTransform_muEtaCleared), so the Gauss-sum normalisation appears explicitly in each statement rather than as a division in the definition. The two unit facts of the node are isUnit_root_mul_one_add_X_sub_one ((1+T)\eps_D^c-1 \in \cO_L[[T]]^\times) and gaussSum_isUnit_of_coprime (G(\eta^{-1}) \in \cO_L^\times); the sum ranges over all of \Z/D\Z, the non-unit terms vanishing since \eta^{-1} is zero there.

Lean code for Definition5.2.1●4 declarations
  • defdefined in PadicLFunctions/Interpolation/NonTame.lean
    complete
    def PadicLFunctions.MeasureR.muEtaCleared.{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) : PadicLFunctions.MeasureR K ℤ_[p]
    def PadicLFunctions.MeasureR.muEtaCleared.{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) :
  PadicLFunctions.MeasureR K ℤ_[p]
    L5.2.2: the measure `μ_η` of RJW §5.2 (TeX 1793–1798): the inverse Mahler
transform of `−G(η⁻¹)⁻¹-normalised ∑_c η(c)⁻¹·((ζ^c)(1+T) − 1)⁻¹`, stated
unnormalised (multiplied through by the unit `−G(η⁻¹)`) per R5-CLEAR; the
genuinely-used object is the *family* below, with the Gauss-normalisation
carried in the statements.
  • theoremdefined in PadicLFunctions/Interpolation/NonTame.lean
    complete
    theorem PadicLFunctions.MeasureR.mahlerTransform_muEtaCleared.{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) :
  PadicLFunctions.MeasureR.mahlerTransform p K
      (PadicLFunctions.MeasureR.muEtaCleared p K η hζ hD) =
    -∑ c ∈ Finset.range D,
        PowerSeries.C (η⁻¹ ↑c) *
          Ring.inverse (PowerSeries.C (ζ ^ c) * (1 + PowerSeries.X) - 1)
    theorem PadicLFunctions.MeasureR.mahlerTransform_muEtaCleared.{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) :
  PadicLFunctions.MeasureR.mahlerTransform
      p K
      (PadicLFunctions.MeasureR.muEtaCleared
        p K η hζ hD) =
    -∑ c ∈ Finset.range D,
        PowerSeries.C (η⁻¹ ↑c) *
          Ring.inverse
            (PowerSeries.C (ζ ^ c) *
                (1 + PowerSeries.X) -
              1)
    The Mahler transform of `muEtaCleared` is the defining series `−G(η⁻¹)F_η`
(EquationFeta, TeX 1793–1795, cleared of its Gauss-sum denominator).
  • theoremdefined in PadicLFunctions/Interpolation/NonTame.lean
    complete
    theorem PadicLFunctions.MeasureR.isUnit_root_mul_one_add_X_sub_one.{u_1} {p : ℕ}
  [hp : Fact (Nat.Prime p)] {K : Type u_1} [NormedField K]
  [NormedAlgebra ℚ_[p] K] [IsUltrametricDist K]
  {ζ : ↥(PadicLFunctions.integerRing K)} {D : ℕ}
  (hζ : IsPrimitiveRoot ζ D) (hD : ¬p ∣ D) {c : ℕ} (hc : ¬D ∣ c) :
  IsUnit (PowerSeries.C (ζ ^ c) * (1 + PowerSeries.X) - 1)
    theorem PadicLFunctions.MeasureR.isUnit_root_mul_one_add_X_sub_one.{u_1}
  {p : ℕ} [hp : Fact (Nat.Prime p)]
  {K : Type u_1} [NormedField K]
  [NormedAlgebra ℚ_[p] K]
  [IsUltrametricDist K]
  {ζ : ↥(PadicLFunctions.integerRing K)}
  {D : ℕ} (hζ : IsPrimitiveRoot ζ D)
  (hD : ¬p ∣ D) {c : ℕ} (hc : ¬D ∣ c) :
  IsUnit
    (PowerSeries.C (ζ ^ c) *
        (1 + PowerSeries.X) -
      1)
    L5.2.1: for `ζ` a primitive `D`-th root of unity with `p ∤ D` and
`D ∤ c`, the power series `ζ^c·(1+X) − 1` is a unit of `R⟦X⟧` (constant
coefficient `ζ^c − 1` is a unit by W3; TeX 1798).
  • theoremdefined in PadicLFunctions/Interpolation/NonTame.lean
    complete
    theorem PadicLFunctions.MeasureR.gaussSum_isUnit_of_coprime.{u_1} {p : ℕ}
  [hp : Fact (Nat.Prime p)] {K : Type u_1} [NormedField K]
  [NormedAlgebra ℚ_[p] K] [IsUltrametricDist K] {D : ℕ} [NeZero D]
  {η : DirichletCharacter (↥(PadicLFunctions.integerRing K)) D}
  (hη : η.IsPrimitive) {ζ : ↥(PadicLFunctions.integerRing K)}
  (hζ : IsPrimitiveRoot ζ D) (hD : ¬p ∣ D) :
  IsUnit (gaussSum η⁻¹ (AddChar.zmodChar D ⋯))
    theorem PadicLFunctions.MeasureR.gaussSum_isUnit_of_coprime.{u_1}
  {p : ℕ} [hp : Fact (Nat.Prime p)]
  {K : Type u_1} [NormedField K]
  [NormedAlgebra ℚ_[p] K]
  [IsUltrametricDist K] {D : ℕ} [NeZero D]
  {η :
    DirichletCharacter
      (↥(PadicLFunctions.integerRing K))
      D}
  (hη : η.IsPrimitive)
  {ζ : ↥(PadicLFunctions.integerRing K)}
  (hζ : IsPrimitiveRoot ζ D)
  (hD : ¬p ∣ D) :
  IsUnit
    (gaussSum η⁻¹ (AddChar.zmodChar D ⋯))
    The Gauss sum `G(η⁻¹)` of a primitive character of conductor `D` coprime
to `p` is a unit of the integer ring (TeX 1798: "the Gauss sum is a `p`-adic
unit (indeed, we have `G(η)G(η⁻¹) = η(−1)D` and `D` is coprime to `p`)").
Theorem5.2.2
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 0✓L∃∀N

Let D > 1 be an integer coprime to p and \eta a primitive Dirichlet character of conductor D. There is a unique measure \zeta_\eta \in \Lam(\Zpx) over the Iwasawa algebra defined over a finite extension L/\Qp containing the values of \eta, such that for every primitive Dirichlet character \chi of conductor p^n, n \geq 0, and every k > 0, \int_{\Zpx}\chi(x)\,x^k\cdot\zeta_\eta = \big(1 - \chi\eta(p)\,p^{k-1}\big) L(\chi\eta, 1-k). This rests on Definition 5.2.7, Lemma 5.2.5, Lemma 5.2.6 and Definition 2.1.3.

The two halves are formalised separately. Existence is zetaEta_twisted_moments: the displayed interpolation property for the explicit measure x^{-1}\Res_{\Zpx}(\mu_\eta), in cleared form (multiplied by the unit G(\eta^{-1})), with the value as the generalised Bernoulli expression LvalNeg and the x^{-1}-shift as the index shift k ↦ k−1. Uniqueness is eq_of_twisted_moments_eq (via the determinacy eq_zero_of_twisted_moments_eq_zero): unit-supported measures with equal χ-twisted moments coincide, under the hypothesis that the coefficient ring contains primitive p^n-th roots of unity for every n — the formal reading of the source's "defined over a (fixed) finite extension L/ℚ_p containing the values" with the χ-quantifier ranging over R-valued characters; the prime-to-p roots needed for character orthogonality come from the Teichmüller lift, which ℤ_p already contains. Ambient primitive roots ε_D, ε_{p^n} are assumed as in the tame case.

Lean code for Theorem5.2.2●3 theorems
  • theoremdefined in PadicLFunctions/Interpolation/NonTame.lean
    complete
    theorem PadicLFunctions.MeasureR.zetaEta_twisted_moments.{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 ^ n))
  {θ :
    DirichletCharacter (↥(PadicLFunctions.integerRing K)) (D * p ^ n)}
  (hθ :
    θ =
      (DirichletCharacter.changeLevel ⋯) η *
        (DirichletCharacter.changeLevel ⋯) χ)
  {k : ℕ} (_hk : 0 < k) :
  ↑((PadicLFunctions.MeasureR.twist p K χ.toContinuousMapZp
          (PadicLFunctions.MeasureR.res p K ⋯
            (PadicLFunctions.MeasureR.muEtaCleared p K η hζ hD)))
        (PadicLFunctions.MeasureR.powCM p K (k - 1))) =
    ↑(gaussSum η⁻¹ (AddChar.zmodChar D ⋯)) *
        (1 - ↑(θ ↑p) * ↑p ^ (k - 1)) *
      PadicLFunctions.LvalNeg (PadicLFunctions.MeasureR.toFieldChar θ)
        (k - 1)
    theorem PadicLFunctions.MeasureR.zetaEta_twisted_moments.{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 ^ n))
  {θ :
    DirichletCharacter
      (↥(PadicLFunctions.integerRing K))
      (D * p ^ n)}
  (hθ :
    θ =
      (DirichletCharacter.changeLevel ⋯)
          η *
        (DirichletCharacter.changeLevel ⋯)
          χ)
  {k : ℕ} (_hk : 0 < k) :
  ↑((PadicLFunctions.MeasureR.twist p K
          χ.toContinuousMapZp
          (PadicLFunctions.MeasureR.res p
            K ⋯
            (PadicLFunctions.MeasureR.muEtaCleared
              p K η hζ hD)))
        (PadicLFunctions.MeasureR.powCM p
          K (k - 1))) =
    ↑(gaussSum η⁻¹
            (AddChar.zmodChar D ⋯)) *
        (1 - ↑(θ ↑p) * ↑p ^ (k - 1)) *
      PadicLFunctions.LvalNeg
        (PadicLFunctions.MeasureR.toFieldChar
          θ)
        (k - 1)
    L5.2.6/L5.2.7 (RJW Def TeX 1866–1868 + final display 1870–1873): the
χ-twisted moments of `ζ_η := x⁻¹·Res_{ℤ_p^×}(μ_η)`, in the moment form the
theorem quantifies (the `x⁻¹`-shift realised by the index shift `k ↦ k−1`):
for `χ` primitive mod `p^n` (`n ≥ 0`) and `k > 0`,
`∫ χ(x)x^k dζ_η = (1 − χη(p)p^{k−1})·L(χη, 1−k)` (cleared). The Euler factor
arises uniformly from `Res = 1 − φ∘ψ` (no case split on `n`: for `n ≥ 1` it
degenerates through `χ(p) = 0`). `hε` mirrors the source's ambient
`ε_{p^n}` (statement replan as in `twist_muA_moments`).
  • theoremdefined in PadicLFunctions/Interpolation/NonTame.lean
    complete
    theorem PadicLFunctions.MeasureR.eq_of_twisted_moments_eq.{u_1} {p : ℕ}
  [hp : Fact (Nat.Prime p)] {K : Type u_1} [NormedField K]
  [NormedAlgebra ℚ_[p] K] [IsUltrametricDist K] [CharZero K]
  (hroots : ∀ (n : ℕ), ∃ ζ, IsPrimitiveRoot ζ (p ^ n))
  (μ ν : PadicLFunctions.MeasureR K ℤ_[p])
  (hμ : PadicLFunctions.MeasureR.res p K ⋯ μ = μ)
  (hν : PadicLFunctions.MeasureR.res p K ⋯ ν = ν)
  (h :
    ∀ (n : ℕ)
      (χ :
        DirichletCharacter (↥(PadicLFunctions.integerRing K)) (p ^ n)),
      χ.IsPrimitive →
        ∀ (k : ℕ),
          0 < k →
            (PadicLFunctions.MeasureR.twist p K χ.toContinuousMapZp μ)
                (PadicLFunctions.MeasureR.powCM p K k) =
              (PadicLFunctions.MeasureR.twist p K χ.toContinuousMapZp ν)
                (PadicLFunctions.MeasureR.powCM p K k)) :
  μ = ν
    theorem PadicLFunctions.MeasureR.eq_of_twisted_moments_eq.{u_1}
  {p : ℕ} [hp : Fact (Nat.Prime p)]
  {K : Type u_1} [NormedField K]
  [NormedAlgebra ℚ_[p] K]
  [IsUltrametricDist K] [CharZero K]
  (hroots :
    ∀ (n : ℕ),
      ∃ ζ, IsPrimitiveRoot ζ (p ^ n))
  (μ ν : PadicLFunctions.MeasureR K ℤ_[p])
  (hμ :
    PadicLFunctions.MeasureR.res p K ⋯ μ =
      μ)
  (hν :
    PadicLFunctions.MeasureR.res p K ⋯ ν =
      ν)
  (h :
    ∀ (n : ℕ)
      (χ :
        DirichletCharacter
          (↥(PadicLFunctions.integerRing
              K))
          (p ^ n)),
      χ.IsPrimitive →
        ∀ (k : ℕ),
          0 < k →
            (PadicLFunctions.MeasureR.twist
                  p K χ.toContinuousMapZp
                  μ)
                (PadicLFunctions.MeasureR.powCM
                  p K k) =
              (PadicLFunctions.MeasureR.twist
                  p K χ.toContinuousMapZp
                  ν)
                (PadicLFunctions.MeasureR.powCM
                  p K k)) :
  μ = ν
    **RJW Theorem 5.7, uniqueness** (TeX 1773–1776 "There exists a unique
measure"): two unit-supported measures with the same χ-twisted moments
agree. With the existence half `zetaEta_twisted_moments` this is the full
statement of the theorem.
  • theoremdefined in PadicLFunctions/Interpolation/NonTame.lean
    complete
    theorem PadicLFunctions.MeasureR.eq_zero_of_twisted_moments_eq_zero.{u_1}
  {p : ℕ} [hp : Fact (Nat.Prime p)] {K : Type u_1} [NormedField K]
  [NormedAlgebra ℚ_[p] K] [IsUltrametricDist K] [CharZero K]
  (hroots : ∀ (n : ℕ), ∃ ζ, IsPrimitiveRoot ζ (p ^ n))
  (μ : PadicLFunctions.MeasureR K ℤ_[p])
  (hsupp : PadicLFunctions.MeasureR.res p K ⋯ μ = μ)
  (h :
    ∀ (n : ℕ)
      (χ :
        DirichletCharacter (↥(PadicLFunctions.integerRing K)) (p ^ n)),
      χ.IsPrimitive →
        ∀ (k : ℕ),
          0 < k →
            (PadicLFunctions.MeasureR.twist p K χ.toContinuousMapZp μ)
                (PadicLFunctions.MeasureR.powCM p K k) =
              0) :
  μ = 0
    theorem PadicLFunctions.MeasureR.eq_zero_of_twisted_moments_eq_zero.{u_1}
  {p : ℕ} [hp : Fact (Nat.Prime p)]
  {K : Type u_1} [NormedField K]
  [NormedAlgebra ℚ_[p] K]
  [IsUltrametricDist K] [CharZero K]
  (hroots :
    ∀ (n : ℕ),
      ∃ ζ, IsPrimitiveRoot ζ (p ^ n))
  (μ : PadicLFunctions.MeasureR K ℤ_[p])
  (hsupp :
    PadicLFunctions.MeasureR.res p K ⋯ μ =
      μ)
  (h :
    ∀ (n : ℕ)
      (χ :
        DirichletCharacter
          (↥(PadicLFunctions.integerRing
              K))
          (p ^ n)),
      χ.IsPrimitive →
        ∀ (k : ℕ),
          0 < k →
            (PadicLFunctions.MeasureR.twist
                  p K χ.toContinuousMapZp
                  μ)
                (PadicLFunctions.MeasureR.powCM
                  p K k) =
              0) :
  μ = 0
    L5.2.8 (determinacy, the uniqueness half of **RJW Thm 5.7**): a measure
on `ℤ_p` supported on the units and killing every `χ(x)·x^k` (all primitive
`χ` of `p`-power conductor valued in `R`, all `k > 0`) is zero — provided `K`
contains enough roots of unity (hypothesis quantified per level). Recorded
design note at decomposition L5.2.8.
Proof for Theorem 5.2.2
Proof uses 4
Proof dependency previews
Preview
Definition 5.2.1
Loading preview
Proof dependency preview content is loaded from the Blueprint HTML cache.

The argument parallels the p-power case but needs no smoothing factor, since L(\eta,s) is entire. Starting from the measure \mu_\eta of Definition 5.2.1, one has by Lemma 5.2.5 the moment formula \int_{\Zpx}x^k\cdot\mu_\eta = (1-\eta(p)p^k)L(\eta,-k). Twisting \mu_\eta by a p-power character \chi and setting \theta := \chi\eta, the measure \mu_\theta := (\mu_\eta)_\chi has the explicit Mahler transform of Lemma 5.2.6, and the same calculation gives \int_{\Zpx}\chi(x)x^k\cdot\mu_\eta = (1-\theta(p)p^k)L(\theta,-k). Finally setting \zeta_\eta := x^{-1}\Res_{\Zpx}(\mu_\eta) from Definition 5.2.7 shifts the exponent of the Euler factor and the argument of L, yielding \int_{\Zpx}\chi(x)x^k\cdot\zeta_\eta = (1-\theta(p)p^{k-1})L(\theta,1-k). Uniqueness follows from the fact that a measure on \Zpx is determined by its moments \int x^k.

Lemma5.2.3
Statement uses 3
Statement dependency previews
Preview
Definition 2.1.3
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 1✓L∃∀N

With f_\eta and \mu_\eta the function and measure of Definition 5.2.1, we have L(f_\eta, s) = -\eta(-1)L(\eta, s), and hence for k \geq 0, \int_{\Zp}x^k\cdot\mu_\eta = L(\eta, -k). This uses Definition 5.2.1 and Definition 2.1.3.

The formalisation proves the displayed moment formula in cleared form: muEtaCleared_moments gives \int x^k \cdot (-G(\eta^{-1})\mu_\eta) = G(\eta^{-1})\,L(\eta,-k) with the value encoded as the generalised Bernoulli expression LvalNeg, by extracting the (k+1)-st coefficient of the formal master identity X_mul_muEtaCleared_subst (t\,G(\eta^{-1})f_\eta(t) equals the generating function of -B_{k,\eta}) — the purely p-adic route through the generalised-Bernoulli generating function genBernoulliPowerSeries_mul, avoiding the complex Mellin detour. The first display (L(f_\eta,s) = -\eta(-1)L(\eta,s), an identity of complex L-functions) is the analytic half quarantined as in Lemma 5.1.6 and is not formalised.

Lean code for Lemma5.2.3●2 theorems
  • theoremdefined in PadicLFunctions/Interpolation/NonTame.lean
    complete
    theorem PadicLFunctions.MeasureR.muEtaCleared_moments.{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) (k : ℕ) :
  ↑((PadicLFunctions.MeasureR.muEtaCleared p K η hζ hD)
        (PadicLFunctions.MeasureR.powCM p K k)) =
    ↑(gaussSum η⁻¹ (AddChar.zmodChar D ⋯)) *
      PadicLFunctions.LvalNeg (PadicLFunctions.MeasureR.toFieldChar η) k
    theorem PadicLFunctions.MeasureR.muEtaCleared_moments.{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)
  (k : ℕ) :
  ↑((PadicLFunctions.MeasureR.muEtaCleared
          p K η hζ hD)
        (PadicLFunctions.MeasureR.powCM p
          K k)) =
    ↑(gaussSum η⁻¹
          (AddChar.zmodChar D ⋯)) *
      PadicLFunctions.LvalNeg
        (PadicLFunctions.MeasureR.toFieldChar
          η)
        k
    L5.2.3 (RJW Lem 5.9, TeX 1801–1804): the moments of `μ_η` are the
`L`-values: `G(η⁻¹) · ∫x^k dμ_η`-cleared form,
`∫ x^k d(muEtaCleared η) = G(η⁻¹) · L(η,−k)`.
  • theoremdefined in PadicLFunctions/Interpolation/NonTame.lean
    complete
    theorem PadicLFunctions.MeasureR.X_mul_muEtaCleared_subst.{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) (hζK : IsPrimitiveRoot (↑ζ) D)
  (hD : ¬p ∣ D) :
  PowerSeries.X *
      PowerSeries.subst (PowerSeries.exp K - 1)
        ((PowerSeries.map (PadicLFunctions.integerRing K).subtype)
          (PadicLFunctions.MeasureR.mahlerTransform p K
            (PadicLFunctions.MeasureR.muEtaCleared p K η hζ hD))) =
    -(PowerSeries.C
          (gaussSum (PadicLFunctions.MeasureR.toFieldChar η)⁻¹
            (AddChar.zmodChar D ⋯)) *
        PowerSeries.mk fun k ↦
          (PadicLFunctions.MeasureR.toFieldChar η).genBernoulli k *
            (↑k.factorial)⁻¹)
    theorem PadicLFunctions.MeasureR.X_mul_muEtaCleared_subst.{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)
  (hζK : IsPrimitiveRoot (↑ζ) D)
  (hD : ¬p ∣ D) :
  PowerSeries.X *
      PowerSeries.subst
        (PowerSeries.exp K - 1)
        ((PowerSeries.map
            (PadicLFunctions.integerRing
                K).subtype)
          (PadicLFunctions.MeasureR.mahlerTransform
            p K
            (PadicLFunctions.MeasureR.muEtaCleared
              p K η hζ hD))) =
    -(PowerSeries.C
          (gaussSum
            (PadicLFunctions.MeasureR.toFieldChar
                η)⁻¹
            (AddChar.zmodChar D ⋯)) *
        PowerSeries.mk fun k ↦
          (PadicLFunctions.MeasureR.toFieldChar
                  η).genBernoulli
              k *
            (↑k.factorial)⁻¹)
    L5.2.3 step 3, the master identity: `X·H_η = −G(η⁻¹)·genBPS_{η_K}` in
`K⟦t⟧`, with `H_η` the exp-substituted `K`-valued Mahler transform of
`muEtaCleared` — the η⁻¹-weighted geometric numerators collapse through the
Gauss sum (modulus-`D` instance of the T509 (v-a) collapse) and the
generating-function identity T504.
Proof for Lemma 5.2.3
uses 1

The L-function identity is proved exactly as in Lemma 5.1.6: expanding 1/(e^t\eps_D^c-1) as a geometric series and collapsing the character sum over (\Z/D\Z)^\times against the additive characters reduces L(f_\eta,s) to -\eta(-1)L(\eta,s) (the overall sign coming from the -1 normalisation in f_\eta). The moment formula follows by identifying the differential operator \partial with d/dt and applying the Mellin special-value theorem: \int_{\Zp} x^k\cdot\mu_\eta = (\partial^k F_\eta)(0) = f_\eta^{(k)}(0) = (-1)^k L(f_\eta,-k) = -(-1)^k\eta(-1)L(\eta,-k). The same parity argument as in Lemma 5.1.6 shows f_\eta(-t) = -\eta(-1)f_\eta(t), so L(\eta,-k) vanishes unless \eta(-1)(-1)^k = -1, on which locus the prefactor -(-1)^k\eta(-1) equals 1; hence \int_{\Zp}x^k\cdot\mu_\eta = L(\eta,-k).

Lemma5.2.4
uses 1used by 1✓L∃∀N

The power series F_\eta of Definition 5.2.1 satisfies \psi(F_\eta) = \eta(p)\,F_\eta, where \psi is the trace-like operator on power series adjoint to \varphi : G(T) \mapsto G((1+T)^p - 1). This uses Definition 5.2.1.

The formalised proof (psi_muEtaCleared, stated for the cleared measure) takes a \mu_p-free route equivalent to the displayed trace computation: the cleared identity \varphi(\eps^{pc}\delta_1 - \delta_0)\cdot\gamma_c = \sum_{j<p}\eps^{cj}\delta_j (geometric telescope), the projection formula \psi(\varphi(\nu)\mu) = \nu\,\psi(\mu) (psi_phi_mul), and \psi(\delta_j) = 0 for j a unit give psi_symm_inverse_denom (\psi(\gamma_c) = \gamma_{pc}); the reindex c ↦ pc on \Z/D then twists the weight by \eta(p). This avoids adjoining the p-th roots of unity that the displayed \frac1p\sum_{\xi\in\mu_p} computation needs, and η need not be primitive.

Lean code for Lemma5.2.4●3 theorems
  • theoremdefined in PadicLFunctions/Interpolation/NonTame.lean
    complete
    theorem PadicLFunctions.MeasureR.psi_muEtaCleared.{u_1} {p : ℕ}
  [hp : Fact (Nat.Prime p)] {K : Type u_1} [NormedField K]
  [NormedAlgebra ℚ_[p] K] [IsUltrametricDist K] [CompleteSpace K]
  {D : ℕ} [NeZero D] (hD1 : 1 < D)
  {η : DirichletCharacter (↥(PadicLFunctions.integerRing K)) D}
  {ζ : ↥(PadicLFunctions.integerRing K)} (hζ : IsPrimitiveRoot ζ D)
  (hD : ¬p ∣ D) :
  PadicLFunctions.MeasureR.psi p K
      (PadicLFunctions.MeasureR.muEtaCleared p K η hζ hD) =
    η ↑p • PadicLFunctions.MeasureR.muEtaCleared p K η hζ hD
    theorem PadicLFunctions.MeasureR.psi_muEtaCleared.{u_1}
  {p : ℕ} [hp : Fact (Nat.Prime p)]
  {K : Type u_1} [NormedField K]
  [NormedAlgebra ℚ_[p] K]
  [IsUltrametricDist K] [CompleteSpace K]
  {D : ℕ} [NeZero D] (hD1 : 1 < D)
  {η :
    DirichletCharacter
      (↥(PadicLFunctions.integerRing K))
      D}
  {ζ : ↥(PadicLFunctions.integerRing K)}
  (hζ : IsPrimitiveRoot ζ D)
  (hD : ¬p ∣ D) :
  PadicLFunctions.MeasureR.psi p K
      (PadicLFunctions.MeasureR.muEtaCleared
        p K η hζ hD) =
    η ↑p •
      PadicLFunctions.MeasureR.muEtaCleared
        p K η hζ hD
    L5.2.4 (RJW Lem 5.10, TeX 1812–1813): "We have `ψ(F_η) = η(p)F_η`."
Proved by the recorded ξ-free route (decomposition L5.2.4: γ-telescope +
projection formula + reindexing `c ↦ pc` on `(ℤ/D)^×`; primitivity of `η`
is not needed).
  • theoremdefined in PadicLFunctions/MeasureR/Toolbox.lean
    complete
    theorem PadicLFunctions.MeasureR.psi_phi_mul.{u_1} {p : ℕ}
  [hp : Fact (Nat.Prime p)] {K : Type u_1} [NormedField K]
  [NormedAlgebra ℚ_[p] K] [IsUltrametricDist K] [CompleteSpace K]
  (ν μ : PadicLFunctions.MeasureR K ℤ_[p]) :
  PadicLFunctions.MeasureR.psi p K
      ((PadicLFunctions.MeasureR.phi p K) ν * μ) =
    ν * PadicLFunctions.MeasureR.psi p K μ
    theorem PadicLFunctions.MeasureR.psi_phi_mul.{u_1}
  {p : ℕ} [hp : Fact (Nat.Prime p)]
  {K : Type u_1} [NormedField K]
  [NormedAlgebra ℚ_[p] K]
  [IsUltrametricDist K] [CompleteSpace K]
  (ν μ :
    PadicLFunctions.MeasureR K ℤ_[p]) :
  PadicLFunctions.MeasureR.psi p K
      ((PadicLFunctions.MeasureR.phi p K)
          ν *
        μ) =
    ν * PadicLFunctions.MeasureR.psi p K μ
    **The projection formula** `ψ(φ(ν)·μ) = ν·ψ(μ)` (the cleared form of
RJW's trace identity Eq. (3.12); used by §5.2's ξ-free route for
`ψ(μ_η) = η(p)μ_η`, decomposition L5.2.4). Proof on test functions through
the convolution formula: both sides integrate
`y ↦ 1_{pℤ_p}(y)·f(x + y/p)` against `μ` in the inner variable.
  • theoremdefined in PadicLFunctions/Interpolation/NonTame.lean
    complete
    theorem PadicLFunctions.MeasureR.psi_symm_inverse_denom.{u_1} {p : ℕ}
  [hp : Fact (Nat.Prime p)] {K : Type u_1} [NormedField K]
  [NormedAlgebra ℚ_[p] K] [IsUltrametricDist K] [CompleteSpace K]
  {ζ : ↥(PadicLFunctions.integerRing K)} {D : ℕ}
  (hζ : IsPrimitiveRoot ζ D) (hD : ¬p ∣ D) {m : ℕ} (hm : ¬D ∣ m) :
  PadicLFunctions.MeasureR.psi p K
      ((PadicLFunctions.MeasureR.mahlerRingEquiv p K).symm
        (Ring.inverse
          (PowerSeries.C (ζ ^ m) * (1 + PowerSeries.X) - 1))) =
    (PadicLFunctions.MeasureR.mahlerRingEquiv p K).symm
      (Ring.inverse
        (PowerSeries.C (ζ ^ (p * m)) * (1 + PowerSeries.X) - 1))
    theorem PadicLFunctions.MeasureR.psi_symm_inverse_denom.{u_1}
  {p : ℕ} [hp : Fact (Nat.Prime p)]
  {K : Type u_1} [NormedField K]
  [NormedAlgebra ℚ_[p] K]
  [IsUltrametricDist K] [CompleteSpace K]
  {ζ : ↥(PadicLFunctions.integerRing K)}
  {D : ℕ} (hζ : IsPrimitiveRoot ζ D)
  (hD : ¬p ∣ D) {m : ℕ} (hm : ¬D ∣ m) :
  PadicLFunctions.MeasureR.psi p K
      ((PadicLFunctions.MeasureR.mahlerRingEquiv
            p K).symm
        (Ring.inverse
          (PowerSeries.C (ζ ^ m) *
              (1 + PowerSeries.X) -
            1))) =
    (PadicLFunctions.MeasureR.mahlerRingEquiv
          p K).symm
      (Ring.inverse
        (PowerSeries.C (ζ ^ (p * m)) *
            (1 + PowerSeries.X) -
          1))
    ψ of the inverse-denominator measure: `ψ(γ_m) = γ_{pm}` (decomposition
L5.2.4 steps (i)–(iii): geometric telescope, then the projection formula
`psi_phi_mul`, then cancellation of the unit `ε^{pm}δ_1 − δ_0`).
Proof for Lemma 5.2.4
uses 0

The key local computation is \frac1p\sum_{\xi\in\mu_p}\frac{1}{(1+T)\xi\eps_D^c - 1} = \frac{1}{(1+T)^p\eps_D^{pc}-1}: expanding the left side as a geometric series, \frac{-1}{p}\sum_{\xi}\sum_{n\geq0}(1+T)^n\eps_D^{nc}\xi^n, the inner sum over \xi\in\mu_p annihilates every term with p \nmid n, leaving -\sum_n (1+T)^{pn}\eps_D^{pcn}, which resums to the right side. Applying this to each summand of F_\eta shows (\varphi\circ\psi)(F_\eta) = \eta(p)\,\varphi(F_\eta) (the index c \mapsto pc rescales the character via \eta(p)); by injectivity of \varphi we conclude \psi(F_\eta) = \eta(p)F_\eta.

Lemma5.2.5
Statement uses 2
Statement dependency previews
Preview
Lemma 5.2.3
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
Used by 3
Reverse dependency previews
Preview
Theorem 5.2.2
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N

For all k \geq 0, \int_{\Zpx}x^k\cdot\mu_\eta = \big(1-\eta(p)\,p^k\big)\,L(\eta,-k). This uses Lemma 5.2.4 and Lemma 5.2.3.

Formalised in cleared form (res_units_muEtaCleared_moments): the Gauss-sum normalisation G(\eta^{-1}) multiplies both sides, and the value L(\eta,-k) is the generalised Bernoulli expression LvalNeg, exactly as in the two preceding nodes.

Lean code for Lemma5.2.5●1 theorem
  • theoremdefined in PadicLFunctions/Interpolation/NonTame.lean
    complete
    theorem PadicLFunctions.MeasureR.res_units_muEtaCleared_moments.{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) (k : ℕ) :
  ↑((PadicLFunctions.MeasureR.res p K ⋯
          (PadicLFunctions.MeasureR.muEtaCleared p K η hζ hD))
        (PadicLFunctions.MeasureR.powCM p K k)) =
    ↑(gaussSum η⁻¹ (AddChar.zmodChar D ⋯)) * (1 - ↑(η ↑p) * ↑p ^ k) *
      PadicLFunctions.LvalNeg (PadicLFunctions.MeasureR.toFieldChar η) k
    theorem PadicLFunctions.MeasureR.res_units_muEtaCleared_moments.{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)
  (k : ℕ) :
  ↑((PadicLFunctions.MeasureR.res p K ⋯
          (PadicLFunctions.MeasureR.muEtaCleared
            p K η hζ hD))
        (PadicLFunctions.MeasureR.powCM p
          K k)) =
    ↑(gaussSum η⁻¹
            (AddChar.zmodChar D ⋯)) *
        (1 - ↑(η ↑p) * ↑p ^ k) *
      PadicLFunctions.LvalNeg
        (PadicLFunctions.MeasureR.toFieldChar
          η)
        k
    L5.2.5 (RJW Lem 5.11, TeX 1831–1834): the unit-restricted moments carry
the Euler factor: `∫_{ℤ_p^×} x^k dμ_η = (1−η(p)p^k)·L(η,−k)` (cleared).
Proof for Lemma 5.2.5
Proof uses 2
Proof dependency previews
Preview
Lemma 5.2.3
Loading preview
Proof dependency preview content is loaded from the Blueprint HTML cache.

Restriction to \Zpx is given by 1 - \varphi\circ\psi, so by Lemma 5.2.4, \Res_{\Zpx}(\mu_\eta) = (1-\varphi\circ\psi)\mu_\eta = \mu_\eta - \eta(p)\varphi(\mu_\eta). Since \int_{\Zp}x^k\cdot\varphi(\mu_\eta) = p^k\int_{\Zp}x^k\cdot\mu_\eta (the operator \varphi corresponds to x\mapsto px), integrating against x^k gives \int_{\Zpx}x^k\cdot\mu_\eta = (1-\eta(p) p^k)\int_{\Zp}x^k\cdot\mu_\eta, and the result follows from Lemma 5.2.3.

Lemma5.2.6
Statement uses 2
Statement dependency previews
Preview
Lemma 5.1.5
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
Used by 2
Reverse dependency previews
Preview
Theorem 5.2.2
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N

Let \chi be a Dirichlet character of conductor p^n, n\geq 0, and set \theta := \chi\eta, a Dirichlet character of conductor Dp^n. Then the measure \mu_\theta := (\mu_\eta)_\chi has Mahler transform F_\theta(T) = \frac{-1}{G(\theta^{-1})}\sum_{c\in(\Z/Dp^n\Z)^\times} \frac{\theta(c)^{-1}}{(1+T)\eps_{Dp^n}^{\,c} - 1}. This uses Lemma 5.1.5 and Definition 5.2.1.

The formalisation keeps the transform in the two-index form mahlerTransform_charTwist_muEtaCleared (the ε_{p^n}^b-line twists of the ε_D^c-denominators, i.e. the CRT-resolved shape of the displayed (\Z/Dp^n)^\times-sum, with θ⁻¹(c) realised as η⁻¹(c)χ⁻¹(b)) and extracts the consequences directly: the master identity X_mul_twist_muEtaCleared_subst (t\,G(\eta^{-1})G(\chi^{-1})f_\theta collapses to the generalised-Bernoulli generating function of \theta, with G(\chi^{-1}) cancelling) and the moment formula twist_muEtaCleared_moments (\int\chi(x)x^m\,d\mu_\eta = G(\eta^{-1})L(\theta,-m), cleared). The single-root closed form is not restated separately.

Lean code for Lemma5.2.6●3 theorems
  • theoremdefined in PadicLFunctions/Interpolation/NonTame.lean
    complete
    theorem PadicLFunctions.MeasureR.mahlerTransform_charTwist_muEtaCleared.{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 : ℕ} {ε : ↥(PadicLFunctions.integerRing K)}
  (hε : IsPrimitiveRoot ε (p ^ N)) (b : ℕ) :
  PadicLFunctions.MeasureR.mahlerTransform p K
      (PadicLFunctions.MeasureR.twist p K
        (PadicLFunctions.MeasureR.charCM (ε ^ b - 1) ⋯)
        (PadicLFunctions.MeasureR.muEtaCleared p K η hζ hD)) =
    -∑ c ∈ Finset.range D,
        PowerSeries.C (η⁻¹ ↑c) *
          Ring.inverse
            (PowerSeries.C (ζ ^ c * ε ^ b) * (1 + PowerSeries.X) - 1)
    theorem PadicLFunctions.MeasureR.mahlerTransform_charTwist_muEtaCleared.{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 : ℕ}
  {ε : ↥(PadicLFunctions.integerRing K)}
  (hε : IsPrimitiveRoot ε (p ^ N))
  (b : ℕ) :
  PadicLFunctions.MeasureR.mahlerTransform
      p K
      (PadicLFunctions.MeasureR.twist p K
        (PadicLFunctions.MeasureR.charCM
          (ε ^ b - 1) ⋯)
        (PadicLFunctions.MeasureR.muEtaCleared
          p K η hζ hD)) =
    -∑ c ∈ Finset.range D,
        PowerSeries.C (η⁻¹ ↑c) *
          Ring.inverse
            (PowerSeries.C
                  (ζ ^ c * ε ^ b) *
                (1 + PowerSeries.X) -
              1)
    The `ε^b`-line twist of `μ̃_η` has the product-root denominators
(L5.2.6's CRT bookkeeping: the `ε_{p^n}`-twists multiply the `ε_D`-units
inside the `γ`s; the `c = 0` line is `0` on both sides since neither
`X` nor a norm-small denominator is invertible).
  • theoremdefined in PadicLFunctions/Interpolation/NonTame.lean
    complete
    theorem PadicLFunctions.MeasureR.X_mul_twist_muEtaCleared_subst.{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) (hζK : IsPrimitiveRoot (↑ζ) D)
  (hD : ¬p ∣ D) {n : ℕ}
  {χ : DirichletCharacter (↥(PadicLFunctions.integerRing K)) (p ^ n)}
  (hχ : χ.IsPrimitive) {ε : ↥(PadicLFunctions.integerRing K)}
  (hε : IsPrimitiveRoot ε (p ^ n)) (hεK : IsPrimitiveRoot (↑ε) (p ^ n))
  {θ :
    DirichletCharacter (↥(PadicLFunctions.integerRing K)) (D * p ^ n)}
  (hθ :
    θ =
      (DirichletCharacter.changeLevel ⋯) η *
        (DirichletCharacter.changeLevel ⋯) χ) :
  PowerSeries.X *
      PowerSeries.subst (PowerSeries.exp K - 1)
        ((PowerSeries.map (PadicLFunctions.integerRing K).subtype)
          (PadicLFunctions.MeasureR.mahlerTransform p K
            (PadicLFunctions.MeasureR.twist p K χ.toContinuousMapZp
              (PadicLFunctions.MeasureR.muEtaCleared p K η hζ hD)))) =
    -(PowerSeries.C
          (gaussSum (PadicLFunctions.MeasureR.toFieldChar η)⁻¹
            (AddChar.zmodChar D ⋯)) *
        PowerSeries.mk fun k ↦
          (PadicLFunctions.MeasureR.toFieldChar θ).genBernoulli k *
            (↑k.factorial)⁻¹)
    theorem PadicLFunctions.MeasureR.X_mul_twist_muEtaCleared_subst.{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)
  (hζK : IsPrimitiveRoot (↑ζ) D)
  (hD : ¬p ∣ D) {n : ℕ}
  {χ :
    DirichletCharacter
      (↥(PadicLFunctions.integerRing K))
      (p ^ n)}
  (hχ : χ.IsPrimitive)
  {ε : ↥(PadicLFunctions.integerRing K)}
  (hε : IsPrimitiveRoot ε (p ^ n))
  (hεK : IsPrimitiveRoot (↑ε) (p ^ n))
  {θ :
    DirichletCharacter
      (↥(PadicLFunctions.integerRing K))
      (D * p ^ n)}
  (hθ :
    θ =
      (DirichletCharacter.changeLevel ⋯)
          η *
        (DirichletCharacter.changeLevel ⋯)
          χ) :
  PowerSeries.X *
      PowerSeries.subst
        (PowerSeries.exp K - 1)
        ((PowerSeries.map
            (PadicLFunctions.integerRing
                K).subtype)
          (PadicLFunctions.MeasureR.mahlerTransform
            p K
            (PadicLFunctions.MeasureR.twist
              p K χ.toContinuousMapZp
              (PadicLFunctions.MeasureR.muEtaCleared
                p K η hζ hD)))) =
    -(PowerSeries.C
          (gaussSum
            (PadicLFunctions.MeasureR.toFieldChar
                η)⁻¹
            (AddChar.zmodChar D ⋯)) *
        PowerSeries.mk fun k ↦
          (PadicLFunctions.MeasureR.toFieldChar
                  θ).genBernoulli
              k *
            (↑k.factorial)⁻¹)
    L5.2.6, the twisted master identity (Lem 5.12 in cleared exp-substituted
form): `X·H_θ = −G(η⁻¹)·genBPS_{θ_K}` with `H_θ` the exp-substituted
`K`-valued Mahler transform of `μ_θ = (μ̃_η)_χ`. The `G(χ⁻¹)`-smearing of
the twist into `ε^b`-lines (T508), each line's product-root clearing, and
the double Gauss collapse at the two coprime moduli; both `e^{Dp^nt} − 1`
and `G(χ⁻¹)` cancel. The ambient roots `hζ`/`hε` mirror the source's
`ε_D`, `ε_{p^n}` (statement replan as in `twist_muA_moments`).
  • theoremdefined in PadicLFunctions/Interpolation/NonTame.lean
    complete
    theorem PadicLFunctions.MeasureR.twist_muEtaCleared_moments.{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 ^ n))
  {θ :
    DirichletCharacter (↥(PadicLFunctions.integerRing K)) (D * p ^ n)}
  (hθ :
    θ =
      (DirichletCharacter.changeLevel ⋯) η *
        (DirichletCharacter.changeLevel ⋯) χ)
  (m : ℕ) :
  ↑((PadicLFunctions.MeasureR.twist p K χ.toContinuousMapZp
          (PadicLFunctions.MeasureR.muEtaCleared p K η hζ hD))
        (PadicLFunctions.MeasureR.powCM p K m)) =
    ↑(gaussSum η⁻¹ (AddChar.zmodChar D ⋯)) *
      PadicLFunctions.LvalNeg (PadicLFunctions.MeasureR.toFieldChar θ) m
    theorem PadicLFunctions.MeasureR.twist_muEtaCleared_moments.{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 ^ n))
  {θ :
    DirichletCharacter
      (↥(PadicLFunctions.integerRing K))
      (D * p ^ n)}
  (hθ :
    θ =
      (DirichletCharacter.changeLevel ⋯)
          η *
        (DirichletCharacter.changeLevel ⋯)
          χ)
  (m : ℕ) :
  ↑((PadicLFunctions.MeasureR.twist p K
          χ.toContinuousMapZp
          (PadicLFunctions.MeasureR.muEtaCleared
            p K η hζ hD))
        (PadicLFunctions.MeasureR.powCM p
          K m)) =
    ↑(gaussSum η⁻¹
          (AddChar.zmodChar D ⋯)) *
      PadicLFunctions.LvalNeg
        (PadicLFunctions.MeasureR.toFieldChar
          θ)
        m
    L5.2.6, the moments of `μ_θ = (μ̃_η)_χ` (RJW TeX 1854–1856: "via a
calculation essentially identical to the cases already seen"):
`∫χ̃(x)x^m dμ̃_η = G(η⁻¹)·L(θ,−m)` (cleared).
Proof for Lemma 5.2.6
uses 1

Apply the twisting formula Lemma 5.1.5 to \mu_\eta, whose Mahler transform is F_\eta(T) = \frac{-1}{G(\eta^{-1})}\sum_{c}\frac{\eta(c)^{-1}} {(1+T)\eps_D^c-1}. The composite sum over (\Z/p^n\Z)^\times and (\Z/D\Z)^\times recombines, via the Chinese Remainder Theorem and the multiplicativity of Gauss sums, into a single sum over (\Z/Dp^n\Z)^\times with the product character \theta^{-1} and the root of unity \eps_{Dp^n} = \eps_D\eps_{p^n}, giving the stated closed form.

Definition5.2.7
Statement uses 2
Statement dependency previews
Preview
Definition 5.2.1
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
Used by 3
Reverse dependency previews
Preview
Theorem 5.2.2
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N

With \mu_\eta the measure of Definition 5.2.1 attached to \eta, define \zeta_\eta := x^{-1}\,\Res_{\Zpx}(\mu_\eta) \in \Lam(\Zpx). This is directly analogous to the construction of \zetap, except that \zeta_\eta is a genuine measure (no pseudo-measure denominator is needed). This uses Definition 5.2.1 and Lemma 5.2.5.

In the formalisation zetaEtaCleared is the genuine measure on ℤ_p^× (pairing g integrates x⁻¹·g, extended by zero, against the G(\eta^{-1})-cleared \mu_\eta), and in the moment statements the x⁻¹-shift is equivalently realised by the index shift k ↦ k−1 (the T036 pattern): zetaEta_twisted_moments states the final display \int\chi(x)x^k\cdot\zeta_\eta = (1-\theta(p)p^{k-1})L(\theta,1-k) directly as the (k-1)-st χ-twisted moment of \Res_{\Zpx}(\mu_\eta) (cleared by G(\eta^{-1})); the Euler factor arises uniformly from \Res = 1 - \varphi\circ\psi, with no case split on n. An ambient primitive p^n-th root of unity is assumed, mirroring the source's \eps_{p^n}.

Lean code for Definition5.2.7●2 declarations
  • defdefined in PadicLFunctions/Interpolation/LpFunction.lean
    complete
    def PadicLFunctions.MeasureR.zetaEtaCleared.{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) : PadicLFunctions.MeasureR K ℤ_[p]ˣ
    def PadicLFunctions.MeasureR.zetaEtaCleared.{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) :
  PadicLFunctions.MeasureR K ℤ_[p]ˣ
    RJW's `ζ_η := x⁻¹·Res_{ℤ_p^×}(μ_η)` (TeX 1866–1868) as a genuine measure
on `ℤ_p^×`, in the cleared normalisation `G(η⁻¹)·ζ_η`: pairing `g` against it
integrates `x⁻¹·g`, extended by zero, against `μ̃_η` (the restriction to the
units is implicit in the extension by zero).
  • theoremdefined in PadicLFunctions/Interpolation/NonTame.lean
    complete
    theorem PadicLFunctions.MeasureR.zetaEta_twisted_moments.{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 ^ n))
  {θ :
    DirichletCharacter (↥(PadicLFunctions.integerRing K)) (D * p ^ n)}
  (hθ :
    θ =
      (DirichletCharacter.changeLevel ⋯) η *
        (DirichletCharacter.changeLevel ⋯) χ)
  {k : ℕ} (_hk : 0 < k) :
  ↑((PadicLFunctions.MeasureR.twist p K χ.toContinuousMapZp
          (PadicLFunctions.MeasureR.res p K ⋯
            (PadicLFunctions.MeasureR.muEtaCleared p K η hζ hD)))
        (PadicLFunctions.MeasureR.powCM p K (k - 1))) =
    ↑(gaussSum η⁻¹ (AddChar.zmodChar D ⋯)) *
        (1 - ↑(θ ↑p) * ↑p ^ (k - 1)) *
      PadicLFunctions.LvalNeg (PadicLFunctions.MeasureR.toFieldChar θ)
        (k - 1)
    theorem PadicLFunctions.MeasureR.zetaEta_twisted_moments.{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 ^ n))
  {θ :
    DirichletCharacter
      (↥(PadicLFunctions.integerRing K))
      (D * p ^ n)}
  (hθ :
    θ =
      (DirichletCharacter.changeLevel ⋯)
          η *
        (DirichletCharacter.changeLevel ⋯)
          χ)
  {k : ℕ} (_hk : 0 < k) :
  ↑((PadicLFunctions.MeasureR.twist p K
          χ.toContinuousMapZp
          (PadicLFunctions.MeasureR.res p
            K ⋯
            (PadicLFunctions.MeasureR.muEtaCleared
              p K η hζ hD)))
        (PadicLFunctions.MeasureR.powCM p
          K (k - 1))) =
    ↑(gaussSum η⁻¹
            (AddChar.zmodChar D ⋯)) *
        (1 - ↑(θ ↑p) * ↑p ^ (k - 1)) *
      PadicLFunctions.LvalNeg
        (PadicLFunctions.MeasureR.toFieldChar
          θ)
        (k - 1)
    L5.2.6/L5.2.7 (RJW Def TeX 1866–1868 + final display 1870–1873): the
χ-twisted moments of `ζ_η := x⁻¹·Res_{ℤ_p^×}(μ_η)`, in the moment form the
theorem quantifies (the `x⁻¹`-shift realised by the index shift `k ↦ k−1`):
for `χ` primitive mod `p^n` (`n ≥ 0`) and `k > 0`,
`∫ χ(x)x^k dζ_η = (1 − χη(p)p^{k−1})·L(χη, 1−k)` (cleared). The Euler factor
arises uniformly from `Res = 1 − φ∘ψ` (no case split on `n`: for `n ≥ 1` it
degenerates through `χ(p) = 0`). `hε` mirrors the source's ambient
`ε_{p^n}` (statement replan as in `twist_muA_moments`).