6.2. The complex value at s = 1🔗

Theorem6.2.1

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 6.2.2

Loading preview

Reverse dependency preview content is loaded from the Blueprint HTML cache.

✓L∃∀N

For \Re(s)>1 one has L(\theta,s) = \frac{1}{G(\theta^{-1})}\sum_{c\in(\Z/N\Z)^\times}\theta^{-1}(c)\sum_{n\geq 1}\frac{\varepsilon_N^{\,nc}}{n^{s}}. This rests on Definition 2.1.3.

Lean code for Theorem6.2.1●1 theorem

theoremdefined in PadicLFunctions/ValuesAtOneComplex.lean

complete

theorem PadicLFunctions.ValuesAtOneComplex.LSeries_eq_gaussSum_inv_mul_sum
  {N : ℕ} [NeZero N] {θ : DirichletCharacter ℂ N} (hθ : θ.IsPrimitive)
  (_hθ1 : θ ≠ 1) {ε : ℂ} (hε : IsPrimitiveRoot ε N) {s : ℂ}
  (hs : 1 < s.re) :
  LSeries (fun n ↦ θ ↑n) s =
    (gaussSum θ⁻¹ (AddChar.zmodChar N ⋯))⁻¹ *
      ∑ c, θ⁻¹ ↑c * LSeries (fun n ↦ ε ^ (n * (↑c).val)) s

theorem PadicLFunctions.ValuesAtOneComplex.LSeries_eq_gaussSum_inv_mul_sum
  {N : ℕ} [NeZero N]
  {θ : DirichletCharacter ℂ N}
  (hθ : θ.IsPrimitive) (_hθ1 : θ ≠ 1)
  {ε : ℂ} (hε : IsPrimitiveRoot ε N)
  {s : ℂ} (hs : 1 < s.re) :
  LSeries (fun n ↦ θ ↑n) s =
    (gaussSum θ⁻¹
          (AddChar.zmodChar N ⋯))⁻¹ *
      ∑ c,
        θ⁻¹ ↑c *
          LSeries
            (fun n ↦ ε ^ (n * (↑c).val)) s

C6-c1 (eq:classical 6.1, TeX 2030–2038): the Gauss-sum/Fourier
rearrangement of the L-series for `Re s > 1`.
RJW Thm 6.1(i) / Washington Thm 4.9 / decomposition R6 C6.

The pointwise Fourier inversion `θ(n)·G(θ⁻¹) = Σ_c θ⁻¹(c)·ε^{n·c}` comes
from `gaussSum_mulShift_of_isPrimitive` applied to `θ⁻¹` (whose inverse is
`θ`); each inner coefficient function `n ↦ ε^{n·c.val}` has unit norm so its
L-series is summable for `Re s > 1` (`LSeriesSummable_of_bounded_of_one_lt_re`),
letting the finite `c`-sum pass through (`LSeries_sum`, `LSeries_smul`).

Statement note (T611): the skeleton's `hθ1 : θ ≠ 1` is retained for API parity
with `LFunction_one_eq` and to match the paper's non-trivial-`θ` setting, but is
*not used* by this rearrangement (it holds for any primitive `θ`); named `_hθ1`.

Proof for Theorem 6.2.1

uses 0

Start from L(\theta,s)=\sum_{a\in(\Z/N\Z)^\times}\theta(a)\sum_{n\equiv a\ (N)}n^{-s} and detect the congruence n\equiv a by the orthogonality of additive characters: \tfrac1N\sum_{c\in\Z/N\Z}\varepsilon_N^{(a-n)c} equals 1 when n\equiv a\ (N) and 0 otherwise. Substituting and exchanging the (absolutely convergent) sums collects the inner sum over a into a Gauss sum, \sum_a\theta(a)\varepsilon_N^{ac}=G(\theta)\theta^{-1}(c), giving \tfrac{G(\theta)}{N}\sum_c\theta^{-1}(c)\sum_{n\geq1}\varepsilon_N^{-nc}n^{-s}. The standard Gauss-sum identity G(\theta)G(\theta^{-1})=\theta(-1)N together with \theta^{-1}(c)=0 for (c,N)\neq1 rewrites the prefactor as \theta(-1)/G(\theta^{-1}), and the change of variables c\mapsto -c removes \theta(-1) and flips the sign in the exponent, yielding the stated formula.

Theorem6.2.2

uses 0used by 0✓L∃∀N

Theorem Theorem 6.1.1 (i) holds: evaluating Theorem 6.2.1 at s=1 gives the asserted closed formula for L(\theta,1).

Lean code for Theorem6.2.2●1 theorem

theoremdefined in PadicLFunctions/ValuesAtOneComplex.lean

complete

theorem PadicLFunctions.ValuesAtOneComplex.LFunction_one_eq {N : ℕ} [NeZero N]
  {θ : DirichletCharacter ℂ N} (hθ : θ.IsPrimitive) (hθ1 : θ ≠ 1)
  {ε : ℂ} (hε : IsPrimitiveRoot ε N) :
  DirichletCharacter.LFunction θ 1 =
    -(gaussSum θ⁻¹ (AddChar.zmodChar N ⋯))⁻¹ *
      ∑ c, θ⁻¹ ↑c * Complex.log (1 - ε ^ (↑c).val)

theorem PadicLFunctions.ValuesAtOneComplex.LFunction_one_eq
  {N : ℕ} [NeZero N]
  {θ : DirichletCharacter ℂ N}
  (hθ : θ.IsPrimitive) (hθ1 : θ ≠ 1)
  {ε : ℂ} (hε : IsPrimitiveRoot ε N) :
  DirichletCharacter.LFunction θ 1 =
    -(gaussSum θ⁻¹
            (AddChar.zmodChar N ⋯))⁻¹ *
      ∑ c,
        θ⁻¹ ↑c *
          Complex.log (1 - ε ^ (↑c).val)

**RJW Theorem 6.1(i)** (`s=1 theorem`(i), TeX 1989–1991): "We have
`L(θ,1) = −G(θ⁻¹)⁻¹ Σ_{c∈(ℤ/N)ˣ} θ⁻¹(c)·log(1−ε_N^c)`."

Proof for Theorem 6.2.2

uses 1

Since \theta is non-trivial we have N>1, so \varepsilon_N^{\,c}\neq1 for every c\in(\Z/N\Z)^\times, and the Taylor expansion of the logarithm -\log(1-\varepsilon_N^{\,c})=\sum_{n\geq1}\varepsilon_N^{\,nc}n^{-1} converges. Setting s=1 in Theorem 6.2.1 therefore replaces the inner sum by -\log(1-\varepsilon_N^{\,c}), producing L(\theta,1)=-\tfrac{1}{G(\theta^{-1})}\sum_c\theta^{-1}(c)\log(1-\varepsilon_N^{\,c}), as claimed.

The expression refines according to the parity of \theta. If \theta is even then pairing c with -c gives \theta^{-1}(c)\log(1-\varepsilon_N^{\,c})+\theta^{-1}(-c)\log(1-\varepsilon_N^{-c}) =2\theta^{-1}(c)\log\abs{1-\varepsilon_N^{\,c}}, so L(\theta,1) may be written with \log\abs{1-\varepsilon_N^{\,c}} in place of \log(1-\varepsilon_N^{\,c}). If \theta is odd, the functional equation gives instead L(\theta,1)=-i\pi\,G(\theta^{-1})^{-1}B_{1,\theta^{-1}}, where B_{1,\theta^{-1}} is the first twisted Bernoulli number.