Reduced Farey indices for primitive-character Gauss expansions

This module supplies the finite, multiplicity-free frequency index needed after expanding primitive Dirichlet characters by Gauss sums. An index is an exact pair (q,a) with 1 ≤ q ≤ Q, a < q, and Nat.Coprime a q; its real frequency is a/q.

The main output is structural rather than a Bombieri--Davenport conclusion: the index-to-frequency map is injective, its image lies in the existing rationalPoints Q, and additive large-sieve energy over the exact reduced indices is bounded by largeSieveBound. Thus later primitive-character arguments may sum Gauss frequencies across moduli without introducing the forbidden multiplicities from unreduced rational representatives.

def AnalyticNumberTheory.LargeSieve.reducedResidues (q : ℕ) : Finset ℕ

Canonical reduced residues 0 ≤ a < q.

Equations

• AnalyticNumberTheory.LargeSieve.reducedResidues q = {a ∈ Finset.range q | a.Coprime q}

@[simp]

theorem AnalyticNumberTheory.LargeSieve.mem_reducedResidues {q a : ℕ} : a ∈ reducedResidues q ↔ a < q ∧ a.Coprime q

theorem AnalyticNumberTheory.LargeSieve.primitive_gaussSum_mulShift_eq_sum_reducedResidues {q : ℕ} [NeZero q] (χ : PrimitiveCharacter q) (n : ℤ) : gaussSum (↑χ) ((primitiveGaussAddChar q).mulShift ↑n) = ∑ a ∈ reducedResidues q, ↑χ ↑a * charReal (↑n * ↑a / ↑q)

A primitive-character Gauss term is supported exactly on canonical reduced residues. This is the pointwise transform that produces the Farey frequencies indexed below; no non-unit residue survives.

theorem AnalyticNumberTheory.LargeSieve.sum_reducedResidues_eq_invChar_mul_gaussSum {q : ℕ} [NeZero q] (χ : PrimitiveCharacter q) (n : ℤ) : ∑ a ∈ reducedResidues q, ↑χ ↑a * charReal (↑n * ↑a / ↑q) = (↑χ)⁻¹ ↑n * gaussSum (↑χ) (primitiveGaussAddChar q)

Gauss shifting identifies the preceding reduced-residue sum with the primitive character coefficient times its Gauss sum.

def AnalyticNumberTheory.LargeSieve.reducedFareyIndices (Q : ℕ) : Finset (ℕ × ℕ)

Exact finite cross-modulus index for reduced Farey/Gauss frequencies. The first coordinate is the modulus and the second the canonical residue.

Equations

• AnalyticNumberTheory.LargeSieve.reducedFareyIndices Q = {qa ∈ (Finset.Icc 1 Q).product (Finset.range Q) | qa.2 < qa.1 ∧ qa.2.Coprime qa.1}

@[simp]

theorem AnalyticNumberTheory.LargeSieve.mem_reducedFareyIndices {Q q a : ℕ} : (q, a) ∈ reducedFareyIndices Q ↔ 1 ≤ q ∧ q ≤ Q ∧ a < q ∧ a.Coprime q

noncomputable def AnalyticNumberTheory.LargeSieve.reducedFareyPoint (qa : ℕ × ℕ) : ℝ

The real additive frequency attached to a modulus-residue pair.

Equations

• AnalyticNumberTheory.LargeSieve.reducedFareyPoint qa = ↑qa.2 / ↑qa.1

@[simp]

theorem AnalyticNumberTheory.LargeSieve.reducedFareyPoint_pair (q a : ℕ) : reducedFareyPoint (q, a) = ↑a / ↑q

theorem AnalyticNumberTheory.LargeSieve.reducedFareyPoint_mem_rationalPoints {Q : ℕ} {qa : ℕ × ℕ} (hqa : qa ∈ reducedFareyIndices Q) : reducedFareyPoint qa ∈ rationalPoints Q

Every exact reduced index gives one of the pre-existing rational points.

theorem AnalyticNumberTheory.LargeSieve.reducedFareyPoint_injOn (Q : ℕ) : Set.InjOn reducedFareyPoint ↑(reducedFareyIndices Q)

Reduced canonical fractions have unique numerator and denominator. This is the no-multiplicity fact missing from the unreduced rationalPoints parameterization.

noncomputable def AnalyticNumberTheory.LargeSieve.reducedFareyPoints (Q : ℕ) : Finset ℝ

Multiplicity-free reduced Farey point set.

Equations

• AnalyticNumberTheory.LargeSieve.reducedFareyPoints Q = Finset.image AnalyticNumberTheory.LargeSieve.reducedFareyPoint (AnalyticNumberTheory.LargeSieve.reducedFareyIndices Q)

theorem AnalyticNumberTheory.LargeSieve.reducedFareyPoints_subset_rationalPoints (Q : ℕ) : reducedFareyPoints Q ⊆ rationalPoints Q

The reduced set is a subset of the existing rational point set.

theorem AnalyticNumberTheory.LargeSieve.sum_reducedFareyPoints_eq_sum_indices {Q : ℕ} {β : Type u_1} [AddCommMonoid β] (f : ℝ → β) : ∑ x ∈ reducedFareyPoints Q, f x = ∑ qa ∈ reducedFareyIndices Q, f (reducedFareyPoint qa)

Exact reindexing: because reduced fractions are unique, summing over the finite (q,a) Gauss-frequency index is summing over its point set once.

theorem AnalyticNumberTheory.LargeSieve.reducedFareyPoints_wellSpaced (Q : ℕ) (hQ : 0 < Q) : wellSpacedReal (reducedFareyPoints Q) (1 / ↑Q ^ 2)

The exact reduced Farey points retain the standard 1/Q² spacing.

theorem AnalyticNumberTheory.LargeSieve.largeSieveReducedFareyIndices (M : ℤ) (N Q : ℕ) (hQ : 0 < Q) (b : ℤ → ℂ) : ∑ qa ∈ reducedFareyIndices Q, ‖∑ n ∈ Finset.Icc (M + 1) (M + ↑N), charReal (↑n * reducedFareyPoint qa) * b n‖ ^ 2 ≤ largeSieveBound N (1 / ↑Q ^ 2) * ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖b n‖ ^ 2

Spacing-consumption bridge on the exact finite reduced indices.

This is ready for the Gauss-expanded primitive-character sum: each canonical coprime (q,a) occurs exactly once across all 1 ≤ q ≤ Q, and the right side is the existing additive large-sieve bound.