def AnalyticNumberTheory.LargeSieve.standardBVChosenSmallCutoff (N : ℕ) : ℕ

Legacy degenerate cutoff retained only for compatibility shims that still expect the historically zeroed small lane.

Equations

• AnalyticNumberTheory.LargeSieve.standardBVChosenSmallCutoff N = min N 1

noncomputable def AnalyticNumberTheory.LargeSieve.standardBVBalancedSmallCutoff (N : ℕ) : ℕ

Production balanced cutoff for the retained small lane.

Equations

• AnalyticNumberTheory.LargeSieve.standardBVBalancedSmallCutoff N = ⌊↑N ^ (1 / 3)⌋₊

theorem AnalyticNumberTheory.LargeSieve.standardBVBalancedSmallCutoff_le (N : ℕ) : standardBVBalancedSmallCutoff N ≤ N

theorem AnalyticNumberTheory.LargeSieve.standardBVBalancedSmallCutoff_cast_le_sqrt (N : ℕ) : ↑(standardBVBalancedSmallCutoff N) ≤ √↑N

theorem AnalyticNumberTheory.LargeSieve.highConductorSet_subset_Icc_one (N Q C : ℕ) : highConductorSet N Q C ⊆ Finset.Icc 1 Q

theorem AnalyticNumberTheory.LargeSieve.standardBVChosenSmall_squareLedger_le (N Q C : ℕ) (hQ : 0 < Q) : primitivePrefixSquareLedgerOn (vaughanSmallCoeff vaughanUnitIntegerCoeff (standardBVBalancedSmallCutoff N)) N (highConductorSet N Q C) ≤ ↑(N.log2 + 1) ^ 2 * primitiveLargeSieveConstant N Q * (↑(standardBVBalancedSmallCutoff N) * Real.log ↑(standardBVBalancedSmallCutoff N + 1) ^ 2)

Ordinary primitive prefix-maximal large sieve, specialized to the exact production small coefficient.

theorem AnalyticNumberTheory.LargeSieve.standardBVChosenSmallCoeff_eq_zero (N : ℕ) : vaughanSmallCoeff vaughanUnitIntegerCoeff (standardBVChosenSmallCutoff N) = 0

At the chosen endpoint, the exact production small coefficient is zero.

theorem AnalyticNumberTheory.LargeSieve.standardBVChosenSmall_squareLedger_payable (A κ B C : ℕ) : ∃ (K₀ : ℝ), 0 < K₀ ∧ ∀ᶠ (N : ℕ) in Filter.atTop, have Q := MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N ↑B; have R := logConductorThreshold N C; have P := 4 * discreteAbelAmplifierPrefixMax N * conductorHarmonicFactor Q ^ 2; have X := ↑N / Real.log ↑N ^ (A + κ); P ^ 2 * (3 * highConductorHarmonicFactor Q R * primitivePrefixSquareLedgerOn (vaughanSmallCoeff vaughanUnitIntegerCoeff (standardBVBalancedSmallCutoff N)) N (highConductorSet N Q C)) ≤ (K₀ * X) ^ 2

The complete weighted small square ledger is paid unconditionally with the production balanced cutoff and no coefficient zeroing.