The nonprincipal carrier required by the first line of Pan (2.4), and the literal bad-prime correction used in (2.12). The existing panIymLow is not changed and is not asserted to be small.

noncomputable def AnalyticNumberTheory.LargeSieve.PanLow.nonprincipalPrimitiveCharacters (q : ℕ) : Finset (PrimitiveCharacter q)

Puncture the principal character before applying SW.

Equations

• AnalyticNumberTheory.LargeSieve.PanLow.nonprincipalPrimitiveCharacters q = {χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q | ↑χ ≠ 1}

noncomputable def AnalyticNumberTheory.LargeSieve.PanLow.nonprincipalLow (g d : ℕ → ℂ) (N A₁ A₂ Q : ℕ) : ℝ

Pan's whole-a norm on the explicitly nonprincipal low carrier.

Equations

• AnalyticNumberTheory.LargeSieve.PanLow.nonprincipalLow g d N A₁ A₂ Q = ∑ q ∈ Finset.Icc 1 Q, (↑q.totient)⁻¹ * ∑ χ ∈ AnalyticNumberTheory.LargeSieve.PanLow.nonprincipalPrimitiveCharacters q, ‖AnalyticNumberTheory.LargeSieve.panSourceCharacterAmplitude g d N A₁ A₂ χ‖

@[simp]

theorem AnalyticNumberTheory.LargeSieve.PanLow.nonprincipalPrimitiveCharacters_one : nonprincipalPrimitiveCharacters 1 = ∅

theorem AnalyticNumberTheory.LargeSieve.PanLow.nonprincipalPrimitiveCharacters_eq_univ {q : ℕ} (hq : 2 ≤ q) : nonprincipalPrimitiveCharacters q = Finset.univ

theorem AnalyticNumberTheory.LargeSieve.PanLow.nonprincipalLow_eq_two_le (g d : ℕ → ℂ) (N A₁ A₂ Q : ℕ) : nonprincipalLow g d N A₁ A₂ Q = ∑ q ∈ Finset.Icc 2 Q, (↑q.totient)⁻¹ * ∑ χ : PrimitiveCharacter q, ‖panSourceCharacterAmplitude g d N A₁ A₂ χ‖

Primitivity eliminates principal characters for q ≥ 2; q = 1 disappears, not by an SW estimate but because its explicitly nonprincipal carrier is empty.

noncomputable def AnalyticNumberTheory.LargeSieve.PanLow.coprimePrimePrefix {q : ℕ} (χ : DirichletCharacter ℂ q) (y m : ℕ) : ℂ

The actual prime prefix with the restriction (n,m)=1.

Equations

• AnalyticNumberTheory.LargeSieve.PanLow.coprimePrimePrefix χ y m = ∑ n ∈ Finset.range (y + 1), if Nat.Prime n ∧ n.Coprime m then χ ↑n else 0

theorem AnalyticNumberTheory.LargeSieve.PanLow.primePrefix_sub_coprimePrimePrefix {q : ℕ} (χ : DirichletCharacter ℂ q) (y m : ℕ) : primePrefix χ y - coprimePrimePrefix χ y m = ∑ n ∈ Finset.range (y + 1) with Nat.Prime n ∧ ¬n.Coprime m, χ ↑n

Exactly the discarded primes dividing m, not a von Mangoldt surrogate.

theorem AnalyticNumberTheory.LargeSieve.PanLow.norm_primePrefix_sub_coprimePrimePrefix_le {q : ℕ} (χ : DirichletCharacter ℂ q) (y m : ℕ) (hm : 0 < m) : ‖primePrefix χ y - coprimePrimePrefix χ y m‖ ≤ ↑m.primeFactors.card

Uniform bad-prime bound by omega(m). The positive-m hypothesis is essential.

theorem AnalyticNumberTheory.LargeSieve.PanLow.norm_primePrefix_sub_coprimePrimePrefix_le_log2 {q : ℕ} (χ : DirichletCharacter ℂ q) (y m : ℕ) (hm : 0 < m) : ‖primePrefix χ y - coprimePrimePrefix χ y m‖ ≤ ↑m.log2

Existing arithmetic count makes the correction at most log₂(m).

theorem AnalyticNumberTheory.LargeSieve.PanLow.coprimePrimePrefix_eq_Icc {q : ℕ} (χ : DirichletCharacter ℂ q) (y m : ℕ) : coprimePrimePrefix χ y m = ∑ n ∈ Finset.Icc 1 y, (if Nat.Prime n ∧ n.Coprime m then 1 else 0) * χ ↑n

The same actual prime indicator in the Icc normalization used by Pan.

theorem AnalyticNumberTheory.LargeSieve.PanLow.primePrefix_eq_Icc {q : ℕ} (χ : DirichletCharacter ℂ q) (y : ℕ) : primePrefix χ y = ∑ n ∈ Finset.Icc 1 y, (if Nat.Prime n then 1 else 0) * χ ↑n

The unrestricted actual prime coefficient in Pan's Icc normalization.

theorem AnalyticNumberTheory.LargeSieve.PanLow.source_prime_coprime_difference_le (g : ℕ → ℂ) (N A₁ A₂ m : ℕ) (hm : 0 < m) (hg : ∀ a ∈ Finset.Ioc A₁ A₂, ‖g a‖ ≤ 1) {q : ℕ} (χ : PrimitiveCharacter q) : ‖∑ a ∈ Finset.Ioc A₁ A₂, g a * ↑χ ↑a * primePrefix (↑χ) (N / a) - panSourceCharacterAmplitude g (fun (n : ℕ) => if Nat.Prime n ∧ n.Coprime m then 1 else 0) N A₁ A₂ χ‖ ≤ ↑(Finset.Ioc A₁ A₂).card * ↑m.primeFactors.card

Whole-a norm retained; the triangle inequality is used only for paying the low-conductor bad-prime correction. No high-conductor estimate is claimed.