Primitive Dirichlet characters for the multiplicative large sieve

This module supplies the finite primitive-character and conductor interface needed before a Bombieri--Davenport large sieve can be stated faithfully. It deliberately does not state a sum over moduli: the pinned analytic-number- theory dependency has only the single-modulus all-character estimate characterSieveModulus_le.

The underlying Mathlib API already defines DirichletCharacter.conductor, DirichletCharacter.IsPrimitive, primitiveCharacter, and changeLevel. The definitions below package those heterogeneous conductor-level objects into a finite subtype that can be used directly by Finset sums. The module also constructs the standard primitive additive character on ZMod q, bridges its Gauss sums to the existing finite Fourier API, and proves both ‖τ(χ)‖ ^ 2 = q and ‖τ(χ)‖ = √q for primitive complex characters.

@[reducible, inline]

abbrev AnalyticNumberTheory.LargeSieve.PrimitiveCharacter (q : ℕ) : Type

Primitive complex Dirichlet characters of the fixed modulus q.

This is a subtype rather than a new character structure, so every existing DirichletCharacter theorem applies to its coercion.

Equations

• AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q = { χ : DirichletCharacter ℂ q // χ.IsPrimitive }

@[instance_reducible]

noncomputable instance AnalyticNumberTheory.LargeSieve.instFintypePrimitiveCharacter (q : ℕ) : Fintype (PrimitiveCharacter q)

The primitive characters of a fixed modulus form a finite type.

Equations

• AnalyticNumberTheory.LargeSieve.instFintypePrimitiveCharacter q = Fintype.ofFinite (AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q)

theorem AnalyticNumberTheory.LargeSieve.primitiveCharacter_card_le_totient_basic (q : ℕ) (hq : 0 < q) : Fintype.card (PrimitiveCharacter q) ≤ q.totient

A positive modulus has at most its totient many primitive characters.

noncomputable def AnalyticNumberTheory.LargeSieve.primitiveCharacters (q : ℕ) : Finset (DirichletCharacter ℂ q)

Primitive characters as a filtered finset of all characters modulo q. This form is useful when applying an all-character estimate.

Equations

• AnalyticNumberTheory.LargeSieve.primitiveCharacters q = Finset.filter DirichletCharacter.IsPrimitive Finset.univ

@[simp]

theorem AnalyticNumberTheory.LargeSieve.mem_primitiveCharacters {q : ℕ} {χ : DirichletCharacter ℂ q} : χ ∈ primitiveCharacters q ↔ χ.IsPrimitive

@[simp]

theorem AnalyticNumberTheory.LargeSieve.primitive_conductor {q : ℕ} (χ : PrimitiveCharacter q) : (↑χ).conductor = q

A member of the primitive subtype has conductor exactly its modulus.

noncomputable def AnalyticNumberTheory.LargeSieve.conductorPrimitiveCharacter {q : ℕ} (χ : DirichletCharacter ℂ q) : PrimitiveCharacter χ.conductor

The conductor-level primitive character associated to an arbitrary Dirichlet character, packaged in the finite primitive subtype.

Equations

• AnalyticNumberTheory.LargeSieve.conductorPrimitiveCharacter χ = ⟨χ.primitiveCharacter, ⋯⟩

@[simp]

theorem AnalyticNumberTheory.LargeSieve.conductorPrimitiveCharacter_val {q : ℕ} (χ : DirichletCharacter ℂ q) : ↑(conductorPrimitiveCharacter χ) = χ.primitiveCharacter

theorem AnalyticNumberTheory.LargeSieve.changeLevel_conductorPrimitiveCharacter {q : ℕ} (χ : DirichletCharacter ℂ q) : (DirichletCharacter.changeLevel ⋯) ↑(conductorPrimitiveCharacter χ) = χ

Exact conductor decomposition: changing the conductor-level primitive character back to the original modulus recovers the original character.

theorem AnalyticNumberTheory.LargeSieve.sum_primitive_eq_filter {q : ℕ} {β : Type u_1} [AddCommMonoid β] (f : DirichletCharacter ℂ q → β) : ∑ χ : PrimitiveCharacter q, f ↑χ = ∑ χ ∈ primitiveCharacters q, f χ

A sum over the primitive subtype is the corresponding filtered sum over all characters.

theorem AnalyticNumberTheory.LargeSieve.sum_primitive_le_sum_all {q : ℕ} (f : DirichletCharacter ℂ q → ℝ) (hf : ∀ (χ : DirichletCharacter ℂ q), 0 ≤ f χ) : ∑ χ : PrimitiveCharacter q, f ↑χ ≤ ∑ χ : DirichletCharacter ℂ q, f χ

Restricting a nonnegative all-character sum to primitive characters can only decrease it.

theorem AnalyticNumberTheory.LargeSieve.characterSievePrimitiveModulus_le {q : ℕ} [NeZero q] (a : ℤ → ℂ) (M : ℤ) (N : ℕ) : ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, ‖∑ n ∈ Finset.Icc (M + 1) (M + ↑N), a n * ↑χ ↑n‖ ^ 2 ≤ ∑ r ∈ Finset.range q, ‖∑ n ∈ Finset.Icc (M + 1) (M + ↑N), charReal (↑n * ↑r / ↑q) * a n‖ ^ 2

The first primitive-character multiplicative large-sieve foundation: the pinned single-modulus all-character estimate restricts to the primitive subtype. This is intentionally only pointwise in q; it is not the missing Bombieri--Davenport sum over moduli.

Primitive Gauss sums

noncomputable def AnalyticNumberTheory.LargeSieve.primitiveGaussAddChar (q : ℕ) [NeZero q] : AddChar (ZMod q) ℂ

The standard primitive additive character x ↦ exp(2πix/q) on ZMod q.

Equations

• AnalyticNumberTheory.LargeSieve.primitiveGaussAddChar q = AddChar.zmodChar q ⋯

@[simp]

theorem AnalyticNumberTheory.LargeSieve.primitiveGaussAddChar_apply (q : ℕ) [NeZero q] (a : ZMod q) : (primitiveGaussAddChar q) a = charReal (↑a.val / ↑q)

theorem AnalyticNumberTheory.LargeSieve.primitiveGaussAddChar_isPrimitive (q : ℕ) [NeZero q] : (primitiveGaussAddChar q).IsPrimitive

The standard additive character on ZMod q is primitive.

theorem AnalyticNumberTheory.LargeSieve.sum_zmod_eq_sum_range {q : ℕ} [NeZero q] {M : Type u_1} [AddCommMonoid M] (f : ZMod q → M) : ∑ a : ZMod q, f a = ∑ r ∈ Finset.range q, f ↑r

Sums over ZMod q can be written using the canonical representatives 0 ≤ r < q.

theorem AnalyticNumberTheory.LargeSieve.zmod_fourier_energy {q : ℕ} [NeZero q] (z : ZMod q → ℂ) : ∑ a : ZMod q, ‖∑ x : ZMod q, charReal (↑a.val * ↑x.val / ↑q) * z x‖ ^ 2 = ↑q * ∑ x : ZMod q, ‖z x‖ ^ 2

Finite Fourier energy identity on ZMod q, specialized to the additive character convention used by Gauss sums.

theorem AnalyticNumberTheory.LargeSieve.dirichletCharacter_sum_norm_sq {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) : ∑ a : ZMod q, ‖χ a‖ ^ 2 = ↑q.totient

The squared L² mass of a complex Dirichlet character is φ(q).

theorem AnalyticNumberTheory.LargeSieve.gaussSum_primitiveGaussAddChar_mulShift {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (a : ZMod q) : gaussSum χ ((primitiveGaussAddChar q).mulShift a) = ∑ x : ZMod q, χ x * charReal (↑a.val * ↑x.val / ↑q)

The Gauss sum against a shifted standard additive character is its explicit finite Fourier sum.

theorem AnalyticNumberTheory.LargeSieve.primitive_gaussSum_norm_sq {q : ℕ} [NeZero q] (χ : PrimitiveCharacter q) : ‖gaussSum (↑χ) (primitiveGaussAddChar q)‖ ^ 2 = ↑q

Primitive complex Dirichlet characters have the classical Gauss-sum norm: |τ(χ)|² = q.

theorem AnalyticNumberTheory.LargeSieve.primitive_gaussSum_norm {q : ℕ} [NeZero q] (χ : PrimitiveCharacter q) : ‖gaussSum (↑χ) (primitiveGaussAddChar q)‖ = √↑q

Norm form of the primitive Gauss-sum identity.