The narrow conductor-local primitive large-sieve input

The full-cutoff primitive large sieve bounds a retained conductor block by the same L + Q² constant as the full block. That statement cannot create the R⁻¹ diagonal needed after deleting conductors d ≤ R. This file therefore freezes the missing analytic input at the square-ledger level, before any unsquared high mean is formed.

noncomputable def AnalyticNumberTheory.LargeSieve.conductorLocalRowEnergy (b : ℤ → ℂ) (M : ℤ) (L : ℕ) : ℝ

Coefficient energy of one primitive prefix row.

Equations

• AnalyticNumberTheory.LargeSieve.conductorLocalRowEnergy b M L = ∑ n ∈ Finset.Icc (M + 1) (M + ↑L), ‖b n‖ ^ 2

def AnalyticNumberTheory.LargeSieve.ConductorLocalPrimitiveLargeSieve (K : ℝ) : Prop

The precise missing analytic strengthening of the primitive prefix-maximal large sieve. It is a square-ledger statement for an arbitrary coefficient row. In particular it neither mentions nor assumes a Vaughan high mean.

The L/R diagonal is the only new information relative to the existing full-cutoff theorem; the Q² lane is unchanged.

Equations

• AnalyticNumberTheory.LargeSieve.ConductorLocalPrimitiveLargeSieve K = ∀ (R Q L : ℕ) (b : ℤ → ℂ) (M : ℤ), 0 < R → 0 < Q → (AnalyticNumberTheory.LargeSieve.highConductorHarmonicTail R Q * AnalyticNumberTheory.LargeSieve.highConductorPrimitiveSquareLedger R Q fun (d : ℕ) (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter d) => √(AnalyticNumberTheory.LargeSieve.primitiveCharacterPrefixMaxSquare b M L d χ)) ≤ K ^ 2 * ↑(L.log2 + 1) ^ 2 * (↑L * AnalyticNumberTheory.LargeSieve.conductorLocalRowEnergy b M L / ↑R + ↑Q ^ 2 * AnalyticNumberTheory.LargeSieve.conductorLocalRowEnergy b M L)

theorem AnalyticNumberTheory.LargeSieve.highConductorPrimitiveRowMean_le_of_conductorLocal {K : ℝ} (hK : 0 ≤ K) (hLS : ConductorLocalPrimitiveLargeSieve K) (R Q L N : ℕ) (b : ℤ → ℂ) (M : ℤ) (hR : 0 < R) (hQ : 0 < Q) (hdiag : ↑L * conductorLocalRowEnergy b M L ≤ ↑N ^ 2) (henergy : conductorLocalRowEnergy b M L ≤ ↑N) : (highConductorPrimitiveMean R Q fun (d : ℕ) (χ : PrimitiveCharacter d) => √(primitiveCharacterPrefixMaxSquare b M L d χ)) ≤ K * ↑(L.log2 + 1) * (↑N / √↑R + ↑Q * √↑N)

Square-ledger extraction. Once the actual row geometry supplies L * energy ≤ N² and energy ≤ N, the local primitive large sieve gives the required N/√R + Q√N scale.