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.standardBVSmall_squareLedger_energy_le (N Q C v : ℕ) (hQ : 0 < Q) : primitivePrefixSquareLedgerOn (vaughanSmallCoeff vaughanUnitIntegerCoeff v) N (highConductorSet N Q C) ≤ ↑(N.log2 + 1) ^ 2 * primitiveLargeSieveConstant N Q * (↑v * Real.log ↑(v + 1) ^ 2)

Coefficient-faithful small-lane energy estimate, before choosing a cutoff.

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.standardBVSmall_weightedSquareLedger_le_log (N Q R C v : ℕ) (hN : 8 ≤ N) (hQpos : 0 < Q) (hQsq : Q ^ 2 ≤ N) (hvN : v ≤ N) (hvSqrt : ↑v ≤ √↑N) : (4 * discreteAbelAmplifierPrefixMax N * conductorHarmonicFactor Q ^ 2) ^ 2 * (3 * highConductorHarmonicFactor Q R * primitivePrefixSquareLedgerOn (vaughanSmallCoeff vaughanUnitIntegerCoeff v) N (highConductorSet N Q C)) ≤ 497664 * (15 + 4 / Real.log 2) * ↑N * √↑N * Real.log ↑N ^ 10

Uniform envelope for the complete weighted square ledger. The coefficient is unchanged; only its energy is bounded. The logarithmic costs are respectively 4 (squared conductor amplifier), 1 (high harmonic), 2 (prefix maximum), 1 (large sieve), and 2 (small-coefficient energy).

theorem AnalyticNumberTheory.LargeSieve.standardBVSmall_weightedSquareLedger_payable (cutoff : ℕ → ℕ) (hcutoff : ∀ᶠ (N : ℕ) in Filter.atTop, cutoff N ≤ standardBVBalancedSmallCutoff N) (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 (cutoff N)) N (highConductorSet N Q C)) ≤ (K₀ * X) ^ 2

One payment theorem for all eventually balanced-bounded small cutoffs.

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.