Vaughan's small range and all-character bookkeeping

This module closes the finite small-range lane left by the structured Vaughan ledgers. It also records the exact, purely finite interfaces needed to pass from conductor-level primitive characters to all characters. No prime-number theorem or Bombieri--Vinogradov conclusion is stated or used.

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanSmallSupport (N v : ℕ) : Finset ℤ

The literal support of the small Vaughan coefficient inside [1,N].

Equations

• AnalyticNumberTheory.LargeSieve.vaughanSmallSupport N v = {n ∈ Finset.Icc 1 ↑N | n.toNat ≤ v}

@[simp]

theorem AnalyticNumberTheory.LargeSieve.mem_vaughanSmallSupport {N v : ℕ} {n : ℤ} : n ∈ vaughanSmallSupport N v ↔ 1 ≤ n ∧ n ≤ ↑N ∧ n.toNat ≤ v

theorem AnalyticNumberTheory.LargeSieve.vaughanSmallCoeff_eq_zero_of_v_lt_toNat (b : ℤ → ℂ) (v : ℕ) {n : ℤ} (hn : v < n.toNat) : vaughanSmallCoeff b v n = 0

The small coefficient vanishes off its literal n.toNat ≤ v support.

theorem AnalyticNumberTheory.LargeSieve.vaughanSmallCoeff_eq_of_toNat_le (b : ℤ → ℂ) (v : ℕ) {n : ℤ} (hn : n.toNat ≤ v) : vaughanSmallCoeff b v n = b n * ↑(ArithmeticFunction.vonMangoldt n.toNat)

On its support, the small coefficient is exactly b(n) Λ(n).

theorem AnalyticNumberTheory.LargeSieve.card_vaughanSmallSupport_le (N v : ℕ) : (vaughanSmallSupport N v).card ≤ v

There are at most v positive integers in the small support.

theorem AnalyticNumberTheory.LargeSieve.vaughanSmallCoeff_energy_eq_support (b : ℤ → ℂ) (N v : ℕ) : ∑ n ∈ Finset.Icc 1 ↑N, ‖vaughanSmallCoeff b v n‖ ^ 2 = ∑ n ∈ vaughanSmallSupport N v, ‖b n‖ ^ 2 * ArithmeticFunction.vonMangoldt n.toNat ^ 2

Exact finite energy identity: all terms outside the literal small support are zero, and no estimate has yet been applied.

theorem AnalyticNumberTheory.LargeSieve.vonMangoldt_le_log_v_succ {n : ℤ} {v : ℕ} (hn : 1 ≤ n) (hnv : n.toNat ≤ v) : ArithmeticFunction.vonMangoldt n.toNat ≤ Real.log ↑(v + 1)

The von Mangoldt coefficient on the positive small range is bounded by log(v+1).

theorem AnalyticNumberTheory.LargeSieve.vaughanSmallCoeff_energy_le_log_support (b : ℤ → ℂ) (N v : ℕ) : ∑ n ∈ Finset.Icc 1 ↑N, ‖vaughanSmallCoeff b v n‖ ^ 2 ≤ Real.log ↑(v + 1) ^ 2 * ∑ n ∈ vaughanSmallSupport N v, ‖b n‖ ^ 2

Weighted small-lane energy estimate with the exact support and the explicit log(v+1)^2 loss.

theorem AnalyticNumberTheory.LargeSieve.vaughanSmallCoeff_energy_le_v_mul_log_sq (b : ℤ → ℂ) (N v : ℕ) (B : ℝ) (hB : 0 ≤ B) (hb : ∀ n ∈ vaughanSmallSupport N v, ‖b n‖ ≤ B) : ∑ n ∈ Finset.Icc 1 ↑N, ‖vaughanSmallCoeff b v n‖ ^ 2 ≤ ↑v * B ^ 2 * Real.log ↑(v + 1) ^ 2

Uniform-coefficient form of the small-lane producer. Both the support length v and the logarithmic loss are explicit.

theorem AnalyticNumberTheory.LargeSieve.weighted_vaughan_prefix_large_sieve_small_closed_ledger (b : ℤ → ℂ) (N Q u v : ℕ) (hQ : 0 < Q) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, primitiveCharacterPrefixMaxSquare (vaughanLambdaCoeff b) 0 N q χ ≤ 3 * ↑(N.log2 + 1) ^ 2 * primitiveLargeSieveConstant N Q * (∑ n ∈ Finset.Icc 1 ↑N, ‖b n‖ ^ 2 * vaughanTypeICutoffEnergy n.toNat u v + ∑ n ∈ Finset.Icc 1 ↑N, ‖b n‖ ^ 2 * vaughanTypeIIDivisorEnergy n.toNat u v + Real.log ↑(v + 1) ^ 2 * ∑ n ∈ vaughanSmallSupport N v, ‖b n‖ ^ 2)

The existing Vaughan prefix ledger with its final opaque lane replaced by the proved small-support energy. This remains a coefficient-energy ledger, not a Bombieri--Vinogradov conclusion.

theorem AnalyticNumberTheory.LargeSieve.weighted_vaughan_prefix_large_sieve_small_closed_uniform_ledger (b : ℤ → ℂ) (N Q u v : ℕ) (B : ℝ) (hQ : 0 < Q) (hB : 0 ≤ B) (hb : ∀ n ∈ vaughanSmallSupport N v, ‖b n‖ ≤ B) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, primitiveCharacterPrefixMaxSquare (vaughanLambdaCoeff b) 0 N q χ ≤ 3 * ↑(N.log2 + 1) ^ 2 * primitiveLargeSieveConstant N Q * (∑ n ∈ Finset.Icc 1 ↑N, ‖b n‖ ^ 2 * vaughanTypeICutoffEnergy n.toNat u v + ∑ n ∈ Finset.Icc 1 ↑N, ‖b n‖ ^ 2 * vaughanTypeIIDivisorEnergy n.toNat u v + ↑v * B ^ 2 * Real.log ↑(v + 1) ^ 2)

Uniform-coefficient specialization of the closed small lane, displaying the exact v · B² · log(v+1)² budget.

Exact conductor and principal-character bookkeeping

noncomputable def AnalyticNumberTheory.LargeSieve.nonprincipalCharacters (q : ℕ) : Finset (DirichletCharacter ℂ q)

The nonprincipal characters at level q, as a concrete finite set.

Equations

• AnalyticNumberTheory.LargeSieve.nonprincipalCharacters q = Finset.univ.erase 1

@[simp]

theorem AnalyticNumberTheory.LargeSieve.mem_nonprincipalCharacters {q : ℕ} {χ : DirichletCharacter ℂ q} : χ ∈ nonprincipalCharacters q ↔ χ ≠ 1

theorem AnalyticNumberTheory.LargeSieve.sum_allCharacters_eq_principal_add_nonprincipal {q : ℕ} {A : Type u_1} [AddCommMonoid A] (F : DirichletCharacter ℂ q → A) : ∑ χ : DirichletCharacter ℂ q, F χ = F 1 + ∑ χ ∈ nonprincipalCharacters q, F χ

Exact finite principal/nonprincipal decomposition. This is the interface at which a main term must be split off before any nonprincipal estimate is applied.

theorem AnalyticNumberTheory.LargeSieve.mem_nonprincipalCharacters_iff_conductor_ne_one {q : ℕ} [NeZero q] {χ : DirichletCharacter ℂ q} : χ ∈ nonprincipalCharacters q ↔ χ.conductor ≠ 1

For nonzero level, nonprincipality is equivalently conductor different from one.

noncomputable def AnalyticNumberTheory.LargeSieve.conductorChangeLevelError {q : ℕ} (χ : DirichletCharacter ℂ q) (b : ℤ → ℂ) (n : ℤ) : ℂ

The explicit error made when replacing a level-q character by its primitive character at the conductor.

Equations

• AnalyticNumberTheory.LargeSieve.conductorChangeLevelError χ b n = b n * χ ↑n - b n * χ.primitiveCharacter ↑n

theorem AnalyticNumberTheory.LargeSieve.conductorChangeLevelError_eq_zero_of_isCoprime {q : ℕ} (χ : DirichletCharacter ℂ q) (b : ℤ → ℂ) {n : ℤ} (hn : IsCoprime n ↑q) : conductorChangeLevelError χ b n = 0

The conductor-change error is supported only on integers not coprime to the original level.

theorem AnalyticNumberTheory.LargeSieve.characterTerm_eq_conductorPrimitive_add_error {q : ℕ} (χ : DirichletCharacter ℂ q) (b : ℤ → ℂ) (n : ℤ) : b n * χ ↑n = b n * χ.primitiveCharacter ↑n + conductorChangeLevelError χ b n

Pointwise exact recovery of an arbitrary character term from the conductor-level primitive term plus its explicit bad-prime correction.

theorem AnalyticNumberTheory.LargeSieve.characterInterval_eq_conductorPrimitive_add_error {q : ℕ} (χ : DirichletCharacter ℂ q) (b : ℤ → ℂ) (M : ℤ) (N : ℕ) : ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), b n * χ ↑n = ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), b n * χ.primitiveCharacter ↑n + ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), conductorChangeLevelError χ b n

Finite interval form of conductor/change-level recovery. A primitive character estimate controls the first sum; the second sum is an explicit correction supported on ¬ IsCoprime n q.

theorem AnalyticNumberTheory.LargeSieve.sum_characterIntervals_eq_principal_add_nonprincipal (q : ℕ) (b : ℤ → ℂ) (M : ℤ) (N : ℕ) : ∑ χ : DirichletCharacter ℂ q, ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), b n * χ ↑n = ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), b n * 1 ↑n + ∑ χ ∈ nonprincipalCharacters q, ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), b n * χ ↑n

The principal contribution is the literal χ = 1 summand; every remaining summand has nontrivial conductor. This is a finite identity, not a PNT main-term asymptotic.