Actual prime-character prefixes for the nonprincipal low-conductor lane. No assertion is made about the unpunctured panIymLow (which contains q = 1). Only finite Abel summation and the existing prime-power correction are used.

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

The literal unweighted prime character sum.

Equations

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

theorem AnalyticNumberTheory.LargeSieve.PanLow.complex_abel (c : ℕ → ℂ) (w : ℕ → ℝ) (y : ℕ) : ∑ n ∈ Finset.range (y + 1), ↑(w n) * c n = ↑(w y) * ∑ n ∈ Finset.range (y + 1), c n + ∑ n ∈ Finset.range y, ↑(w n - w (n + 1)) * ∑ k ∈ Finset.range (n + 1), c k

Finite complex Abel identity; the production real kernel is unchanged.

theorem AnalyticNumberTheory.LargeSieve.PanLow.norm_abel_le (c : ℕ → ℂ) (y : ℕ) (M : ℝ) (h : ∀ n ≤ y, ‖∑ k ∈ Finset.range (n + 1), c k‖ ≤ M) : ‖∑ n ∈ Finset.range (y + 1), ↑(reciprocalLogWeight n) * c n‖ ≤ discreteAbelAmplifier y * M

Bounded total variation of the already proved reciprocal-log kernel.

theorem AnalyticNumberTheory.LargeSieve.PanLow.primePrefix_eq_abel_sub_correction {q : ℕ} (χ : DirichletCharacter ℂ q) (y : ℕ) : primePrefix χ y = ∑ n ∈ Finset.range (y + 1), ↑(reciprocalLogWeight n) * (lambdaNatCoeff n * χ ↑n) - ∑ n ∈ Finset.range (y + 1), ↑(if Nat.Prime n then 0 else ArithmeticFunction.vonMangoldt n / Real.log ↑n) * χ ↑n

Exact removal of the nonprime von Mangoldt terms after Abel.

theorem AnalyticNumberTheory.LargeSieve.PanLow.norm_correction_le {q : ℕ} (χ : DirichletCharacter ℂ q) (y : ℕ) : ‖∑ n ∈ Finset.range (y + 1), ↑(if Nat.Prime n then 0 else ArithmeticFunction.vonMangoldt n / Real.log ↑n) * χ ↑n‖ ≤ MathlibNt.SieveTheory.LiuWeight.globalPrimePowerCorrection y

The twisted correction is dominated by the existing untwisted one.

theorem AnalyticNumberTheory.LargeSieve.PanLow.lambda_le_primitive {N y q : ℕ} (hy : y ≤ N) (χ : PrimitiveCharacter q) : ‖lambdaCharacterPrefix y q ↑χ‖ ≤ primitivePrefixAmplitude vonMangoldtIntegerCoeff N q χ

Pointwise lambda prefix bounded by the established primitive maximum.

theorem AnalyticNumberTheory.LargeSieve.PanLow.primePrefix_le_psi_add_correction {N y q : ℕ} (hy : y ≤ N) (χ : PrimitiveCharacter q) : ‖primePrefix (↑χ) y‖ ≤ 2 * (Real.log 2)⁻¹ * primitivePrefixAmplitude vonMangoldtIntegerCoeff N q χ + MathlibNt.SieveTheory.LiuWeight.globalPrimePowerCorrection y

Finite psi-to-prime bridge: no AP or BV premise.

theorem AnalyticNumberTheory.LargeSieve.PanLow.eventually_sqrt_le_log_budget (D : ℕ) : ∀ᶠ (N : ℕ) in Filter.atTop, √↑N ≤ ↑N / Real.log ↑N ^ D

Elementary parameter bridge, obtained from Mathlib's log-versus-power limit.

theorem AnalyticNumberTheory.LargeSieve.PanLow.primePrefix_siegelWalfisz (C D : ℕ) : ∃ (K : ℝ), 0 < K ∧ ∀ᶠ (N : ℕ) in Filter.atTop, 2 ≤ N → ∀ q ∈ Finset.Icc 2 (logConductorThreshold N C), ∀ (χ : PrimitiveCharacter q), ↑χ ≠ 1 → ∀ y ≤ N, ‖primePrefix (↑χ) y‖ ≤ K * ↑N / Real.log ↑N ^ D

Unconditional SW for actual unweighted prime prefixes. Constants and the threshold precede the modulus, character and prefix. No prime-BV hypothesis.

theorem AnalyticNumberTheory.LargeSieve.PanLow.primePrefix_siegelWalfisz_real_conductor (b : ℝ) (D : ℕ) : ∃ (K : ℝ), 0 < K ∧ ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (q : ℕ), 2 ≤ q → ↑q ≤ Real.log ↑N ^ b → ∀ (χ : PrimitiveCharacter q), ↑χ ≠ 1 → ‖primePrefix (↑χ) N‖ ≤ K * ↑N / Real.log ↑N ^ D

The same endpoint with an arbitrary fixed real logarithmic conductor exponent.

theorem AnalyticNumberTheory.LargeSieve.PanLow.primePrefix_siegelWalfisz_endpoint (b A : ℝ) : ∃ (K : ℝ), 0 < K ∧ ∃ (N₀ : ℕ), ∀ N ≥ N₀, ∀ (q : ℕ), 2 ≤ q → ↑q ≤ Real.log ↑N ^ b → ∀ (χ : PrimitiveCharacter q), ↑χ ≠ 1 → ‖primePrefix (↑χ) N‖ ≤ K * ↑N / Real.log ↑N ^ A

Endpoint-only version with real saving exponent, in the paper's notation.