4.1. Gauss sums🔗

Definition4.1.1

uses 1

Used by 4

Reverse dependency previews

Preview

Proposition 4.1.2

Loading preview

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

✓L∃∀N

For a Dirichlet character \chi modulo p valued in \mathbb{C}, the Gauss sum is \tau(\chi) \;=\; \sum_{a \in \mathbb{Z}/p\mathbb{Z}} \chi(a)\,e^{2\pi i a / p} \;\in\; \mathbb{C}, where the additive character is a \mapsto e^{2\pi i a/p}.

Definition 2.2.1

Lean code for Definition4.1.1●1 definition

defdefined in Mathlib/NumberTheory/GaussSum.lean

complete

def gaussSum.{u, v} {R : Type u} [CommRing R] [Fintype R] {R' : Type v}
  [CommRing R'] (χ : MulChar R R') (ψ : AddChar R R') : R'

def gaussSum.{u, v} {R : Type u} [CommRing R]
  [Fintype R] {R' : Type v} [CommRing R']
  (χ : MulChar R R') (ψ : AddChar R R') :
  R'

Definition of the Gauss sum associated to a multiplicative and an additive character.

Proposition4.1.2

uses 1used by 1✓L∃∀N

For a non-trivial Dirichlet character \chi modulo p, \tau(\chi)\,\tau(\bar\chi) \;=\; \chi(-1)\,p, \qquad |\tau(\chi)|^2 \;=\; p.

Definition 4.1.1

Lean code for Proposition4.1.2●1 theorem

theoremdefined in BernoulliRegular/GaussSum/Basic.lean

complete

theorem BernoulliRegular.gaussSum_mul_gaussSum_inv_stdAddChar (p : ℕ)
  [hp : Fact (Nat.Prime p)] {χ : DirichletCharacter ℂ p} (hχ : χ ≠ 1) :
  gaussSum χ ZMod.stdAddChar * gaussSum χ⁻¹ ZMod.stdAddChar =
    χ (-1) * ↑p

theorem BernoulliRegular.gaussSum_mul_gaussSum_inv_stdAddChar
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  {χ : DirichletCharacter ℂ p}
  (hχ : χ ≠ 1) :
  gaussSum χ ZMod.stdAddChar *
      gaussSum χ⁻¹ ZMod.stdAddChar =
    χ (-1) * ↑p

**T026**: For a non-trivial Dirichlet character `χ` modulo a prime `p`,
`τ(χ) · τ(χ̄) = χ(-1) · p`, where `τ(χ) = gaussSum χ ZMod.stdAddChar` is
the classical Gauss sum.

Proof for Proposition 4.1.2

uses 0

Expand both Gauss sums and multiply: \tau(\chi)\tau(\bar\chi) = \sum_{a,b}\chi(a)\bar\chi(b)e^{2\pi i(a+b)/p}. After the change of variables a=tb on the terms with b\ne0, the inner sum over b vanishes unless t=-1. The surviving contribution is \chi(-1)p. Moreover \overline{\tau(\chi)}=\chi(-1)\tau(\bar\chi), and therefore |\tau(\chi)|^2 = \tau(\chi)\overline{\tau(\chi)} = \chi(-1)\tau(\chi)\tau(\bar\chi) = p.

The Gauss-sum sign (whether \tau(\chi) = +\sqrt{p} or -\sqrt{p} for a real quadratic character) is fixed by the classical quadratic Gauss-sum evaluation and is used in the L(1,\chi) formula of the next chapter.