AnalyticNumberTheory.LargeSieve.CharacterIndicators

Dirichlet-character expansion of an arithmetic-progression indicator

For units n, l modulo q, the indicator 1_{n ≡ l [MOD q]} has the Dirichlet-character expansion

Σ_{χ mod q} χ(n)·conj(χ(l)) = φ(q)·1_{n ≡ l [MOD q]}.

This is the standard step in Pan's proof that converts congruence counts to means of character sums (Liu 2022 §II; Halberstam--Richert Ch. 10). It connects the Parseval/orthogonality arguments for Type I/II bounds to arithmetic-progression counts. This module assembles the pointwise character orthogonality charOrthSum from Multiplicative.lean and translates equality in ZMod into congruence of natural numbers using ZMod.natCast_eq_natCast_iff.

Main results:

• charOrthSum_unit: the orthogonality sum on units a b : ZMod q is if a = b then φ(q) else 0;
• charIndicator_zmod: the indicator form on ZMod, Σ_χ χ(a)·star(χ(b)) = φ(q)·1_{a=b};
• charIndicator: the natural-number congruence form, Σ_χ χ(n)·star(χ(l)) = if n ≡ l [MOD q] then φ(q) else 0;
• charIndicator_mul: the multiplicative indicator form φ(q)·1_{n≡l};
• charIndicator_ap: the normalized pointwise expansion 1_{n≡l} = φ(q)⁻¹·Σ_χ χ(n)·star(χ(l));
• charSum_ap: arithmetic-progression sums as character sums, the Parseval interface for Type I/II estimates: Σ_{n≤N, n≡l [MOD q]} a_n = φ(q)⁻¹·Σ_χ star(χ(l))·Σ_{n≤N} a_n·χ(n).

References: Liu, "On the weighted Pan theorem" (2022) §II--§III; Halberstam--Richert, "Sieve Methods" (1974) Ch. 10; Montgomery (1971) Ch. 1.

1. Orthogonality sums on units of ZMod: indicator form

theorem AnalyticNumberTheory.LargeSieve.charOrthSum_unit {q : ℕ} (hq : 0 < q) {a b : ZMod q} (ha : IsUnit a) (hb : IsUnit b) : ∑ χ : DirichletCharacter ℂ q, χ a * star (χ b) = if a = b then ↑q.totient else 0

The character orthogonality sum on units is if a = b then φ(q) else 0 (ZMod form). Under ha hb, the three conditions in charOrthSum (unit, unit, and equality) reduce to a = b.

theorem AnalyticNumberTheory.LargeSieve.charIndicator_zmod {q : ℕ} (hq : 0 < q) {a b : ZMod q} (ha : IsUnit a) (hb : IsUnit b) : ∑ χ : DirichletCharacter ℂ q, χ a * star (χ b) = ↑q.totient * if a = b then 1 else 0

Indicator form (ZMod): for units a b, Σ_χ χ(a)·star(χ(b)) = φ(q)·1_{a=b}.

2. Natural-number congruence form

theorem AnalyticNumberTheory.LargeSieve.charIndicator {q : ℕ} (hq : 0 < q) {n l : ℕ} (hn : IsUnit ↑n) (hl : IsUnit ↑l) : ∑ χ : DirichletCharacter ℂ q, χ ↑n * star (χ ↑l) = if n ≡ l [MOD q] then ↑q.totient else 0

Character expansion of an arithmetic-progression indicator (natural-number form): for units n, l, Σ_χ χ(n)·star(χ(l)) = if n ≡ l [MOD q] then φ(q) else 0. Equality in ZMod is equivalent to congruence modulo q (ZMod.natCast_eq_natCast_iff).

theorem AnalyticNumberTheory.LargeSieve.charIndicator_mul {q : ℕ} (hq : 0 < q) {n l : ℕ} (hn : IsUnit ↑n) (hl : IsUnit ↑l) : ∑ χ : DirichletCharacter ℂ q, χ ↑n * star (χ ↑l) = ↑q.totient * if n ≡ l [MOD q] then 1 else 0

Multiplicative indicator form: Σ_χ χ(n)·star(χ(l)) = φ(q)·1_{n≡l}.

3. Normalized pointwise expansion and arithmetic-progression sums

theorem AnalyticNumberTheory.LargeSieve.charIndicator_ap {q : ℕ} (hq : 0 < q) {l : ℕ} (hl : IsUnit ↑l) (n : ℕ) : (if n ≡ l [MOD q] then 1 else 0) = (↑q.totient)⁻¹ * ∑ χ : DirichletCharacter ℂ q, χ ↑n * star (χ ↑l)

Normalized pointwise expansion: for a unit l and any n : ℕ, 1_{n≡l} = φ(q)⁻¹·Σ_χ χ(n)·star(χ(l)). If n is not a unit, χ(n) = 0 makes the right-hand side zero; if n ≡ l, then n is automatically a unit.

theorem AnalyticNumberTheory.LargeSieve.charSum_ap {q : ℕ} (hq : 0 < q) {l : ℕ} (hl : IsUnit ↑l) (a : ℕ → ℂ) (N : ℕ) : (∑ n ∈ Finset.range (N + 1), a n * if n ≡ l [MOD q] then 1 else 0) = (↑q.totient)⁻¹ * ∑ χ : DirichletCharacter ℂ q, star (χ ↑l) * ∑ n ∈ Finset.range (N + 1), a n * χ ↑n

Arithmetic-progression sums as character sums (the Parseval interface for Type I/II estimates): for a unit l, Σ_{n≤N, n≡l [MOD q]} a_n = φ(q)⁻¹·Σ_χ star(χ(l))·Σ_{n≤N} a_n·χ(n).