theorem AnalyticNumberTheory.LargeSieve.primitiveCharacter_ne_one {q : ℕ} (hq : 1 < q) (χ : PrimitiveCharacter q) : ↑χ ≠ 1

A primitive character of modulus greater than one is nonprincipal.

theorem AnalyticNumberTheory.LargeSieve.primitiveCharacter_sum_zmod_eq_zero {q : ℕ} [NeZero q] (hq : 1 < q) (χ : PrimitiveCharacter q) : ∑ a : ZMod q, ↑χ a = 0

The sum of a primitive character over the residue ring is zero when q > 1.

theorem AnalyticNumberTheory.LargeSieve.primitiveCharacter_sum_range_period_eq_zero {q : ℕ} (hq : 1 < q) (χ : PrimitiveCharacter q) : ∑ n ∈ Finset.range q, ↑χ ↑n = 0

The usual natural representatives 0, ..., q-1 also give a zero complete period.

theorem AnalyticNumberTheory.LargeSieve.primitiveCharacter_prefix_norm_le {q M : ℕ} (hq : 1 < q) (χ : PrimitiveCharacter q) : ‖∑ n ∈ Finset.range M, ↑χ ↑n‖ ≤ ↑q

Every prefix of a primitive character has the elementary complete-period bound q.

theorem AnalyticNumberTheory.LargeSieve.primitiveCharacter_interval_norm_le_two_mul {q A B : ℕ} (hq : 1 < q) (χ : PrimitiveCharacter q) : ‖∑ n ∈ Finset.Ico A B, ↑χ ↑n‖ ≤ 2 * ↑q

Every half-open interval has norm at most 2q, by subtraction of two prefixes.

theorem AnalyticNumberTheory.LargeSieve.primitiveCharacter_logWeight_range_norm_le {q M : ℕ} (hq : 1 < q) (χ : PrimitiveCharacter q) : ‖∑ k ∈ Finset.range M, ↑(Real.log (↑k + 1)) * ↑χ ↑(k + 1)‖ ≤ 4 * ↑q * Real.log (↑M + 1)

Abel summation with the elementary interval bound gives a completely algebraic logarithmic-weight estimate. The constant 4 comes from using the safe 2q interval estimate for shifted prefixes.

theorem AnalyticNumberTheory.LargeSieve.primitiveCharacter_logWeight_Icc_norm_le {q M : ℕ} (hq : 1 < q) (χ : PrimitiveCharacter q) : ‖∑ m ∈ Finset.Icc 1 M, ↑(Real.log ↑m) * ↑χ ↑m‖ ≤ 4 * ↑q * Real.log (↑M + 1)

The same logarithmic-weight estimate in the conventional 1 ≤ m ≤ M form.