Conductor grouping and change-level correction ledger

A finite, quantitative reduction from all nonprincipal Dirichlet characters to primitive characters grouped by conductor. The principal summand is retained literally. No prime-number theorem or Bombieri--Vinogradov assertion occurs.

noncomputable def AnalyticNumberTheory.LargeSieve.conductorBadSupport (q : ℕ) (M : ℤ) (N : ℕ) : Finset ℤ

Integers in the interval on which changing from level q to the conductor can produce an error.

Equations

• AnalyticNumberTheory.LargeSieve.conductorBadSupport q M N = {n ∈ Finset.Icc (M + 1) (M + ↑N) | ¬IsCoprime n ↑q}

@[simp]

theorem AnalyticNumberTheory.LargeSieve.mem_conductorBadSupport {q : ℕ} {M n : ℤ} {N : ℕ} : n ∈ conductorBadSupport q M N ↔ M + 1 ≤ n ∧ n ≤ M + ↑N ∧ ¬IsCoprime n ↑q

theorem AnalyticNumberTheory.LargeSieve.conductorChangeLevelError_eq_zero_of_not_mem {q : ℕ} (χ : DirichletCharacter ℂ q) (b : ℤ → ℂ) (M : ℤ) (N : ℕ) {n : ℤ} (hn : n ∈ Finset.Icc (M + 1) (M + ↑N)) (hbad : n ∉ conductorBadSupport q M N) : conductorChangeLevelError χ b n = 0

The change-level error has exactly zero contribution away from the explicit bad support.

theorem AnalyticNumberTheory.LargeSieve.conductorChangeLevelError_norm_sq_le {q : ℕ} (χ : DirichletCharacter ℂ q) (b : ℤ → ℂ) (n : ℤ) : ‖conductorChangeLevelError χ b n‖ ^ 2 ≤ 4 * ‖b n‖ ^ 2

Pointwise 4‖b(n)‖² bound for the squared change-level correction.

theorem AnalyticNumberTheory.LargeSieve.conductorChangeLevelError_energy_eq_badSupport {q : ℕ} (χ : DirichletCharacter ℂ q) (b : ℤ → ℂ) (M : ℤ) (N : ℕ) : ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖conductorChangeLevelError χ b n‖ ^ 2 = ∑ n ∈ conductorBadSupport q M N, ‖conductorChangeLevelError χ b n‖ ^ 2

Exact support restriction for the finite correction energy.

theorem AnalyticNumberTheory.LargeSieve.conductorChangeLevelError_energy_le_badSupport {q : ℕ} (χ : DirichletCharacter ℂ q) (b : ℤ → ℂ) (M : ℤ) (N : ℕ) : ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖conductorChangeLevelError χ b n‖ ^ 2 ≤ 4 * ∑ n ∈ conductorBadSupport q M N, ‖b n‖ ^ 2

Explicit finite energy bound: only bad-prime-supported coefficients occur, with pointwise constant four.

noncomputable def AnalyticNumberTheory.LargeSieve.conductorErrorPrefixSquare {q : ℕ} (χ : DirichletCharacter ℂ q) (b : ℤ → ℂ) (M : ℤ) (y : ℕ) : ℝ

Squared prefix correction.

Equations

• AnalyticNumberTheory.LargeSieve.conductorErrorPrefixSquare χ b M y = ‖∑ n ∈ Finset.Icc (M + 1) (M + ↑y), AnalyticNumberTheory.LargeSieve.conductorChangeLevelError χ b n‖ ^ 2

noncomputable def AnalyticNumberTheory.LargeSieve.conductorErrorPrefixMaxSquare {q : ℕ} (χ : DirichletCharacter ℂ q) (b : ℤ → ℂ) (M : ℤ) (N : ℕ) : ℝ

Maximum squared prefix correction over 0 ≤ y ≤ N.

Equations

• AnalyticNumberTheory.LargeSieve.conductorErrorPrefixMaxSquare χ b M N = (Finset.image (fun (y : ℕ) => AnalyticNumberTheory.LargeSieve.conductorErrorPrefixSquare χ b M y) (Finset.range (N + 1))).max' ⋯

theorem AnalyticNumberTheory.LargeSieve.conductorErrorPrefixSquare_le_energy {q : ℕ} (χ : DirichletCharacter ℂ q) (b : ℤ → ℂ) (M : ℤ) {N y : ℕ} (hy : y ≤ N) : conductorErrorPrefixSquare χ b M y ≤ ↑N * ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖conductorChangeLevelError χ b n‖ ^ 2

Every correction prefix is controlled by N times its full interval energy.

theorem AnalyticNumberTheory.LargeSieve.conductorErrorPrefixMaxSquare_le_badSupport {q : ℕ} (χ : DirichletCharacter ℂ q) (b : ℤ → ℂ) (M : ℤ) (N : ℕ) : conductorErrorPrefixMaxSquare χ b M N ≤ 4 * ↑N * ∑ n ∈ conductorBadSupport q M N, ‖b n‖ ^ 2

Explicit support bound for the maximal correction.

noncomputable def AnalyticNumberTheory.LargeSieve.characterPrefixSquare {q : ℕ} (χ : DirichletCharacter ℂ q) (b : ℤ → ℂ) (M : ℤ) (y : ℕ) : ℝ

Squared prefix for an arbitrary (possibly imprimitive) character.

Equations

• AnalyticNumberTheory.LargeSieve.characterPrefixSquare χ b M y = ‖∑ n ∈ Finset.Icc (M + 1) (M + ↑y), b n * χ ↑n‖ ^ 2

noncomputable def AnalyticNumberTheory.LargeSieve.characterPrefixMaxSquare {q : ℕ} (χ : DirichletCharacter ℂ q) (b : ℤ → ℂ) (M : ℤ) (N : ℕ) : ℝ

Maximum squared prefix for an arbitrary character.

Equations

• AnalyticNumberTheory.LargeSieve.characterPrefixMaxSquare χ b M N = (Finset.image (fun (y : ℕ) => AnalyticNumberTheory.LargeSieve.characterPrefixSquare χ b M y) (Finset.range (N + 1))).max' ⋯

theorem AnalyticNumberTheory.LargeSieve.characterPrefixMaxSquare_le_conductor_add_error {q : ℕ} (χ : DirichletCharacter ℂ q) (b : ℤ → ℂ) (M : ℤ) (N : ℕ) : characterPrefixMaxSquare χ b M N ≤ 2 * (primitiveCharacterPrefixMaxSquare b M N χ.conductor (conductorPrimitiveCharacter χ) + conductorErrorPrefixMaxSquare χ b M N)

Per-character maximal reduction to its conductor primitive character plus its literal correction maximum.

def AnalyticNumberTheory.LargeSieve.nonprincipalConductors (q : ℕ) : Finset ℕ

Positive divisors at least two: precisely the possible nonprincipal conductors at a positive level.

Equations

• AnalyticNumberTheory.LargeSieve.nonprincipalConductors q = {d ∈ q.divisors | 2 ≤ d}

noncomputable def AnalyticNumberTheory.LargeSieve.imprimitiveConductorWeight (Q d : ℕ) : ℝ

Total q/φ(q) weight with which one primitive character of conductor d appears among levels 1 ≤ q ≤ Q. This is the exact imprimitive multiplicity with the analytic weight retained, rather than replaced by a crude count.

Equations

• AnalyticNumberTheory.LargeSieve.imprimitiveConductorWeight Q d = ∑ q ∈ Finset.Icc 1 Q with d ∣ q, ↑q / ↑q.totient

theorem AnalyticNumberTheory.LargeSieve.sum_nonprincipal_by_conductor {q : ℕ} (hq : 0 < q) (F : (d : ℕ) → PrimitiveCharacter d → ℝ) : ∑ χ ∈ nonprincipalCharacters q, F χ.conductor (conductorPrimitiveCharacter χ) = ∑ d ∈ nonprincipalConductors q, ∑ ψ : PrimitiveCharacter d, F d ψ

At one positive level, characters of nontrivial conductor are in bijection with primitive characters over the divisors d ≥ 2 of that level.

theorem AnalyticNumberTheory.LargeSieve.weighted_sum_nonprincipal_by_conductor (Q : ℕ) (F : (d : ℕ) → PrimitiveCharacter d → ℝ) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ ∈ nonprincipalCharacters q, F χ.conductor (conductorPrimitiveCharacter χ) = ∑ d ∈ Finset.Icc 2 Q, imprimitiveConductorWeight Q d * ∑ ψ : PrimitiveCharacter d, F d ψ

Exact global conductor regrouping. Every primitive character of conductor d receives exactly imprimitiveConductorWeight Q d; hence both ordinary imprimitive multiplicity and the q/φ(q) weight are visible.

theorem AnalyticNumberTheory.LargeSieve.weighted_allCharacter_nonprincipal_prefix_ledger (b : ℤ → ℂ) (M : ℤ) (N Q : ℕ) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ ∈ nonprincipalCharacters q, characterPrefixMaxSquare χ b M N ≤ 2 * ∑ d ∈ Finset.Icc 2 Q, imprimitiveConductorWeight Q d * ∑ ψ : PrimitiveCharacter d, primitiveCharacterPrefixMaxSquare b M N d ψ + 8 * ↑N * ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ _χ ∈ nonprincipalCharacters q, ∑ n ∈ conductorBadSupport q M N, ‖b n‖ ^ 2

The requested all-character nonprincipal maximal ledger. Its first term is then exactly regrouped by the preceding theorem, while the second is the honest bad-prime correction; no principal estimate is inserted.

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

Principal/nonprincipal split with the principal maximal term kept literally. This theorem is bookkeeping only, not a PNT assertion.