Von Mangoldt conductor change-level correction

For the coefficient Λ(n) on the integer interval [1,N], the terms on which changing a Dirichlet character from level q to its conductor can disagree are prime powers p^k with p ∣ q. This gives a polylogarithmic bound for every correction prefix and, after summing over levels and nonprincipal characters, a Q^2 (rather than N-times-energy) correction.

The interval starts at zero: all prefix sums below are over [1,y]. No claim is made here for translated intervals, where a separate count of prime powers in a short interval would be needed.

noncomputable def AnalyticNumberTheory.LargeSieve.vonMangoldtIntegerCoeff (n : ℤ) : ℂ

The integer coefficient which is Λ(n) on positive integers.

Equations

• AnalyticNumberTheory.LargeSieve.vonMangoldtIntegerCoeff n = ↑(ArithmeticFunction.vonMangoldt n.toNat)

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

Prime powers in [1,N] on which level q can disagree with its conductor.

Equations

• AnalyticNumberTheory.LargeSieve.vonMangoldtBadSupport q N = {n ∈ Finset.Icc 1 ↑N | ArithmeticFunction.vonMangoldt n.toNat ≠ 0 ∧ ¬IsCoprime n ↑q}

@[simp]

theorem AnalyticNumberTheory.LargeSieve.mem_vonMangoldtBadSupport {q N : ℕ} {n : ℤ} : n ∈ vonMangoldtBadSupport q N ↔ 1 ≤ n ∧ n ≤ ↑N ∧ ArithmeticFunction.vonMangoldt n.toNat ≠ 0 ∧ ¬IsCoprime n ↑q

def AnalyticNumberTheory.LargeSieve.vonMangoldtBadPrimePowers (q N : ℕ) : Finset ℤ

The explicit family p^(k+1), with p ∣ q prime and k < log₂(N)+1, containing the bad von Mangoldt support.

Equations

• AnalyticNumberTheory.LargeSieve.vonMangoldtBadPrimePowers q N = q.primeFactors.biUnion fun (p : ℕ) => Finset.image (fun (k : ℕ) => ↑(p ^ (k + 1))) (Finset.range (N.log2 + 1))

theorem AnalyticNumberTheory.LargeSieve.vonMangoldtBadSupport_subset_primePowers {q : ℕ} (hq : 0 < q) (N : ℕ) : vonMangoldtBadSupport q N ⊆ vonMangoldtBadPrimePowers q N

A bad von Mangoldt integer is literally a power of a prime divisor of the level.

theorem AnalyticNumberTheory.LargeSieve.card_primeFactors_le_log2 {q : ℕ} (hq : 0 < q) : q.primeFactors.card ≤ q.log2

The number of distinct prime divisors of q is at most log₂ q for positive q.

theorem AnalyticNumberTheory.LargeSieve.card_vonMangoldtBadSupport_le {q : ℕ} (hq : 0 < q) (N : ℕ) : (vonMangoldtBadSupport q N).card ≤ q.primeFactors.card * (N.log2 + 1)

Cardinality form of the prime-power compression.

theorem AnalyticNumberTheory.LargeSieve.vonMangoldt_changeLevelError_norm_le {q : ℕ} (χ : DirichletCharacter ℂ q) {N : ℕ} {n : ℤ} (hn : n ∈ Finset.Icc 1 ↑N) : ‖conductorChangeLevelError χ vonMangoldtIntegerCoeff n‖ ≤ if n ∈ vonMangoldtBadSupport q N then 2 * Real.log ↑N else 0

On [1,N], every von Mangoldt change-level error has norm at most 2 log N; outside the explicit bad support it is zero.

theorem AnalyticNumberTheory.LargeSieve.vonMangoldt_conductorErrorPrefixSquare_le {q : ℕ} (hq : 0 < q) (χ : DirichletCharacter ℂ q) (N : ℕ) {y : ℕ} (hy : y ≤ N) : conductorErrorPrefixSquare χ vonMangoldtIntegerCoeff 0 y ≤ (2 * ↑q.log2 * (↑N.log2 + 1) * Real.log ↑N) ^ 2

Every prefix correction for Λ, on the interval starting at zero, is polylogarithmic in N and q.

theorem AnalyticNumberTheory.LargeSieve.vonMangoldt_conductorErrorPrefixMaxSquare_le {q : ℕ} (hq : 0 < q) (χ : DirichletCharacter ℂ q) (N : ℕ) : conductorErrorPrefixMaxSquare χ vonMangoldtIntegerCoeff 0 N ≤ (2 * ↑q.log2 * (↑N.log2 + 1) * Real.log ↑N) ^ 2

Maximal-prefix version of the preceding bound.

theorem AnalyticNumberTheory.LargeSieve.weighted_vonMangoldt_conductorErrorPrefixMaxSquare_le (N Q : ℕ) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ ∈ nonprincipalCharacters q, conductorErrorPrefixMaxSquare χ vonMangoldtIntegerCoeff 0 N ≤ ↑Q ^ 2 * (2 * ↑Q.log2 * (↑N.log2 + 1) * Real.log ↑N) ^ 2

The full q,χ correction aggregate is Q² times a polylogarithm. This is the Λ-specific estimate replacing the general coefficient N-times-energy bound.

theorem AnalyticNumberTheory.LargeSieve.weighted_allCharacter_nonprincipal_vonMangoldt_prefix_ledger (N Q : ℕ) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ ∈ nonprincipalCharacters q, characterPrefixMaxSquare χ vonMangoldtIntegerCoeff 0 N ≤ 2 * ∑ d ∈ Finset.Icc 2 Q, imprimitiveConductorWeight Q d * ∑ ψ : PrimitiveCharacter d, primitiveCharacterPrefixMaxSquare vonMangoldtIntegerCoeff 0 N d ψ + 2 * ↑Q ^ 2 * (2 * ↑Q.log2 * (↑N.log2 + 1) * Real.log ↑N) ^ 2

Λ-specific all-character nonprincipal maximal reduction: the primitive conductor ledger plus the now-closed Q² polylog correction.