Chen 1973, Lemma 4: a primitive-character sum

This module follows the statement and proof printed on p. 115 of Chen's original 1973 paper. The scan states that k is odd and squarefree and m ≠ 1; its primitive-root sentence tacitly also needs (m,k)=1. We retain that coprimality hypothesis explicitly, as required by the source proof.

The proof has two finite layers. At one prime, the primitive characters are all characters except the principal character, so orthogonality gives the local factor p-2 when m ≡ 1 (mod p) and absolute value 1 otherwise. This module proves the local layer and final elementary product comparison. The downstream module Chen1973Lemma4CRT constructs the CRT equivalence, proves the exact squarefree local-factor product, and discharges the factorization premise.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma4CharacterSum (k m : ℕ) : ℂ

Chen p. 115: Z(m,k), before taking its absolute value.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma4CharacterSum k m = ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter k, ↑χ ↑m

def AnalyticNumberTheory.LargeSieve.chen1973Lemma4LocalMagnitude (p m : ℕ) : ℕ

The magnitude of Chen's one-prime geometric sum.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma4LocalMagnitude p m = if p ∣ m - 1 then p - 2 else 1

theorem AnalyticNumberTheory.LargeSieve.chen1973_isPrimitive_iff_ne_one_of_odd_prime {p : ℕ} (hp : Nat.Prime p) (_hodd : Odd p) (χ : DirichletCharacter ℂ p) : χ.IsPrimitive ↔ χ ≠ 1

For an odd prime modulus, primitivity is exactly nonprincipality. This is the formal version of the range 1 ≤ ν ≤ p-2 in Chen's proof.

theorem AnalyticNumberTheory.LargeSieve.chen1973_primitiveCharacters_prime_eq_erase_one {p : ℕ} (hp : Nat.Prime p) (hodd : Odd p) : primitiveCharacters p = Finset.univ.erase 1

The filtered primitive family at an odd prime is univ.erase 1.

theorem AnalyticNumberTheory.LargeSieve.chen1973_prime_characterSum_eq {p m : ℕ} (hp : Nat.Prime p) (hodd : Odd p) (hmp : m.Coprime p) : chen1973Lemma4CharacterSum p m = (if ↑m = 1 then ↑p.totient else 0) - 1

Chen's local geometric sum, written without choosing a primitive root: all characters give the orthogonality sum, and the principal term is removed.

theorem AnalyticNumberTheory.LargeSieve.chen1973_natCast_zmod_eq_one_iff {p m : ℕ} (_hp : Nat.Prime p) (hm : 0 < m) : ↑m = 1 ↔ p ∣ m - 1

The congruence in the local factor is exactly divisibility of m-1.

theorem AnalyticNumberTheory.LargeSieve.chen1973_prime_characterSum_norm {p m : ℕ} (hp : Nat.Prime p) (hodd : Odd p) (hm : 0 < m) (hmp : m.Coprime p) : ‖chen1973Lemma4CharacterSum p m‖ = ↑(chen1973Lemma4LocalMagnitude p m)

Exact one-prime magnitude in the order used by Chen.

theorem AnalyticNumberTheory.LargeSieve.chen1973_prod_selected_primeFactors_eq_gcd {k n : ℕ} (hk : Squarefree k) (hn : n ≠ 0) : ∏ p ∈ k.primeFactors with p ∣ n, p = k.gcd n

The product of the prime factors of squarefree k which divide n is exactly gcd k n.

theorem AnalyticNumberTheory.LargeSieve.chen1973_localMagnitude_product_le_selected (k m : ℕ) : ∏ p ∈ k.primeFactors, chen1973Lemma4LocalMagnitude p m ≤ ∏ p ∈ k.primeFactors with p ∣ m - 1, p

The finite local product in Chen's last displayed calculation is at most the product of the selected prime divisors.

theorem AnalyticNumberTheory.LargeSieve.chen1973_lemma4_of_squarefree_local_factorization {k m : ℕ} (_hkOdd : Odd k) (hkSq : Squarefree k) (hm : 0 < m) (_hmk : m.Coprime k) (hm1 : m ≠ 1) (hfactor : ‖chen1973Lemma4CharacterSum k m‖ = ↑(∏ p ∈ k.primeFactors, chen1973Lemma4LocalMagnitude p m)) : ‖chen1973Lemma4CharacterSum k m‖ ≤ ↑((m - 1).gcd k)

The elementary last line of Chen's proof. The premise is the exact finite CRT reindexing asserted by the two preceding displayed equalities on p. 115, not a proposition-valued black box.