Weighted primitive-character Bombieri--Davenport inequality

This module combines primitive Gauss inversion with the multiplicity-free reduced Farey additive large sieve. The only loss relative to the classical N + Q² constant is the explicit dyadic-shell logarithm already present in largeSieveBound.

theorem AnalyticNumberTheory.LargeSieve.character_reducedResidues_bessel {q : ℕ} [NeZero q] (c : ℕ → ℂ) : ∑ χ : PrimitiveCharacter q, ‖∑ a ∈ reducedResidues q, c a * ↑χ ↑a‖ ^ 2 ≤ ↑q.totient * ∑ a ∈ reducedResidues q, ‖c a‖ ^ 2

Character orthogonality for arbitrary coefficients on canonical reduced residues. This is the exact finite Bessel inequality needed after Gauss inversion.

theorem AnalyticNumberTheory.LargeSieve.primitive_interval_gauss_inversion {q : ℕ} [NeZero q] (χ : PrimitiveCharacter q) (b : ℤ → ℂ) (M : ℤ) (N : ℕ) : gaussSum (↑χ)⁻¹ (primitiveGaussAddChar q) * ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), b n * ↑χ ↑n = ∑ a ∈ reducedResidues q, (↑χ)⁻¹ ↑a * ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), charReal (↑n * ↑a / ↑q) * b n

Inversion by the primitive Gauss sum, with the inverse character chosen so that the recovered interval coefficient is χ(n) rather than χ⁻¹(n).

noncomputable def AnalyticNumberTheory.LargeSieve.primitiveCharacterInvEquiv (q : ℕ) : PrimitiveCharacter q ≃ PrimitiveCharacter q

Inversion is an involution on primitive characters.

Equations

• AnalyticNumberTheory.LargeSieve.primitiveCharacterInvEquiv q = { toFun := fun (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) => ⟨(↑χ)⁻¹, ⋯⟩, invFun := fun (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) => ⟨(↑χ)⁻¹, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

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

The exact single-modulus weighted primitive-character inequality after Gauss inversion. Its right side contains only canonical reduced additive frequencies, with constant one.

theorem AnalyticNumberTheory.LargeSieve.sum_reducedResidues_eq_sum_reducedFareyIndices {β : Type u_1} [AddCommMonoid β] (Q : ℕ) (f : ℕ × ℕ → β) : ∑ q ∈ Finset.Icc 1 Q, ∑ a ∈ reducedResidues q, f (q, a) = ∑ qa ∈ reducedFareyIndices Q, f qa

Reindex canonical reduced residues for 1 ≤ q ≤ Q by reduced Farey indices, preserving the modulus range and coprimality condition.

theorem AnalyticNumberTheory.LargeSieve.interval_additive_energy_reindex (b : ℤ → ℂ) (M : ℤ) (N Q : ℕ) : ∑ q ∈ Finset.Icc 1 Q, ∑ a ∈ reducedResidues q, ‖∑ n ∈ Finset.Icc (M + 1) (M + ↑N), charReal (↑n * ↑a / ↑q) * b n‖ ^ 2 = ∑ qa ∈ reducedFareyIndices Q, ‖∑ n ∈ Finset.Icc (M + 1) (M + ↑N), charReal (↑n * reducedFareyPoint qa) * b n‖ ^ 2

Concrete reindexing of the interval additive energy.

theorem AnalyticNumberTheory.LargeSieve.weighted_primitive_bombieri_davenport (b : ℤ → ℂ) (M : ℤ) (N Q : ℕ) (hQ : 0 < Q) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, ‖∑ n ∈ Finset.Icc (M + 1) (M + ↑N), b n * ↑χ ↑n‖ ^ 2 ≤ largeSieveBound N (1 / ↑Q ^ 2) * ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖b n‖ ^ 2

Weighted primitive-character Bombieri--Davenport inequality across all 1 ≤ q ≤ Q, with interval coefficients and the exact additive-stack constant.

theorem AnalyticNumberTheory.LargeSieve.weighted_primitive_bombieri_davenport_explicit (b : ℤ → ℂ) (M : ℤ) (N Q : ℕ) (hQ : 0 < Q) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, ‖∑ n ∈ Finset.Icc (M + 1) (M + ↑N), b n * ↑χ ↑n‖ ^ 2 ≤ (↑N + (2 * ↑⌈Real.log (↑Q ^ 2) / Real.log 2⌉₊ + 12) * ↑Q ^ 2) * ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖b n‖ ^ 2

Fully expanded constant. This records the unique current scale loss: N + (2⌈log₂(Q²)⌉+12)Q², inherited solely from the additive Schur/dyadic stack.