Finite Moebius, Selberg, and lower Rosser weights

Finite lower and upper sieve inequalities, lower Rosser coefficients, and Euler-normalized lower density recursions.

0. Finite lower-bound sieve interface

def MathlibNt.SieveTheory.LinearSieve.IsLowerMoebius (muMinus : ℕ → ℝ) : Prop

A sequence of coefficients is lower Möbius when its divisor sums lie below the coprimality indicator. This is the exact finite dual of Mathlib's BoundingSieve.IsUpperMoebius.

Equations

• MathlibNt.SieveTheory.LinearSieve.IsLowerMoebius muMinus = ∀ (n : ℕ), ∑ d ∈ n.divisors, muMinus d ≤ if n = 1 then 1 else 0

theorem MathlibNt.SieveTheory.LinearSieve.sum_of_lowerMoebius_le_siftedSum {S : BoundingSieve} (muMinus : ℕ → ℝ) (hmu : IsLowerMoebius muMinus) : ∑ d ∈ S.prodPrimes.divisors, muMinus d * BoundingSieve.multSum d ≤ BoundingSieve.siftedSum

A lower Möbius sequence gives a lower bound for the sifted sum before any asymptotic estimate is introduced.

theorem MathlibNt.SieveTheory.LinearSieve.mainSum_sub_errSum_le_siftedSum_of_lowerMoebius {S : BoundingSieve} (muMinus : ℕ → ℝ) (hmu : IsLowerMoebius muMinus) : S.totalMass * BoundingSieve.mainSum muMinus - BoundingSieve.errSum muMinus ≤ BoundingSieve.siftedSum

Explicit-error lower sieve inequality. Unlike the historical pointwise interfaces, the loss is the concrete finite quantity errSum muMinus.

0.1. Finite upper Selberg weights

def MathlibNt.SieveTheory.LinearSieve.HasUpperLevelSupport (P D : ℕ) (muPlus : ℕ → ℝ) : Prop

A coefficient sequence has upper-sieve level support when it vanishes on divisors of P outside the strict natural-number level D.

Equations

• MathlibNt.SieveTheory.LinearSieve.HasUpperLevelSupport P D muPlus = ∀ (d : ℕ), d ∣ P → ¬d < D → muPlus d = 0

def MathlibNt.SieveTheory.LinearSieve.IsUpperMoebiusOn (P : ℕ) (muPlus : ℕ → ℝ) : Prop

The upper Möbius condition restricted to divisors of a fixed finite prime product. This is the exact amount of positivity used by a finite sieve.

Equations

• MathlibNt.SieveTheory.LinearSieve.IsUpperMoebiusOn P muPlus = ∀ (n : ℕ), n ∣ P → (if n = 1 then 1 else 0) ≤ ∑ d ∈ n.divisors, muPlus d

theorem MathlibNt.SieveTheory.LinearSieve.siftedSum_le_sum_of_upperMoebiusOn {S : BoundingSieve} (muPlus : ℕ → ℝ) (hmu : IsUpperMoebiusOn S.prodPrimes muPlus) : BoundingSieve.siftedSum ≤ ∑ d ∈ S.prodPrimes.divisors, muPlus d * BoundingSieve.multSum d

A finite upper-Möbius coefficient bounds the sifted sum from above.

def MathlibNt.SieveTheory.LinearSieve.upperErrSum (S : BoundingSieve) (D : ℕ) (muPlus : ℕ → ℝ) : ℝ

The exact finite upper-sieve remainder sum at level D.

Equations

• MathlibNt.SieveTheory.LinearSieve.upperErrSum S D muPlus = ∑ d ∈ S.prodPrimes.divisors with d < D, |muPlus d| * |BoundingSieve.rem d|

theorem MathlibNt.SieveTheory.LinearSieve.errSum_eq_upperErrSum {S : BoundingSieve} {D : ℕ} {muPlus : ℕ → ℝ} (hsupp : HasUpperLevelSupport S.prodPrimes D muPlus) : BoundingSieve.errSum muPlus = upperErrSum S D muPlus

theorem MathlibNt.SieveTheory.LinearSieve.siftedSum_le_mainSum_add_upperErrSum_of_upperMoebiusOn {S : BoundingSieve} (D : ℕ) (muPlus : ℕ → ℝ) (hmu : IsUpperMoebiusOn S.prodPrimes muPlus) (hsupp : HasUpperLevelSupport S.prodPrimes D muPlus) : BoundingSieve.siftedSum ≤ S.totalMass * BoundingSieve.mainSum muPlus + upperErrSum S D muPlus

Finite upper sieve inequality with no Selberg representation: an upper Möbius certificate on divisors and level support are sufficient.

structure MathlibNt.SieveTheory.LinearSieve.UpperSelbergWeightsAtLevel (P D : ℕ) : Type

A finite Selberg upper weight records the underlying lambda, its normalization, and the level support of the resulting lambdaSquared coefficient.

• lambda : ℕ → ℝ
• lambda_one : self.lambda 1 = 1
• muPlus_level_support : HasUpperLevelSupport P D (BoundingSieve.lambdaSquared self.lambda)
• muPlus_abs_le_threePow (d : ℕ) : |BoundingSieve.lambdaSquared self.lambda d| ≤ 3 ^ d.primeFactors.card

def MathlibNt.SieveTheory.LinearSieve.UpperSelbergWeightsAtLevel.muPlus {P D : ℕ} (W : UpperSelbergWeightsAtLevel P D) : ℕ → ℝ

The explicit upper coefficient generated by a finite Selberg weight.

Equations

• W.muPlus = BoundingSieve.lambdaSquared W.lambda

theorem MathlibNt.SieveTheory.LinearSieve.UpperSelbergWeightsAtLevel.isUpperMoebius {P D : ℕ} (W : UpperSelbergWeightsAtLevel P D) : BoundingSieve.IsUpperMoebius W.muPlus

theorem MathlibNt.SieveTheory.LinearSieve.UpperSelbergWeightsAtLevel.hasUpperLevelSupport {P D : ℕ} (W : UpperSelbergWeightsAtLevel P D) : HasUpperLevelSupport P D W.muPlus

theorem MathlibNt.SieveTheory.LinearSieve.siftedSum_le_mainSum_add_upperErrSum {S : BoundingSieve} {D : ℕ} (W : UpperSelbergWeightsAtLevel S.prodPrimes D) : BoundingSieve.siftedSum ≤ S.totalMass * BoundingSieve.mainSum W.muPlus + upperErrSum S D W.muPlus

Finite upper Selberg inequality with the main sum and the exact level-restricted remainder sum kept separate.

0.2. Finite lower Rosser weights

def MathlibNt.SieveTheory.LinearSieve.IsLowerMoebiusOn (P : ℕ) (muMinus : ℕ → ℝ) : Prop

The lower Möbius condition needed by a sieve with the fixed finite product P. Requiring it for all natural numbers, as IsLowerMoebius does, is unnecessarily strong for a finite sieve.

Equations

• MathlibNt.SieveTheory.LinearSieve.IsLowerMoebiusOn P muMinus = ∀ (n : ℕ), n ∣ P → ∑ d ∈ n.divisors, muMinus d ≤ if n = 1 then 1 else 0

theorem MathlibNt.SieveTheory.LinearSieve.sum_of_lowerMoebiusOn_le_siftedSum {S : BoundingSieve} (muMinus : ℕ → ℝ) (hmu : IsLowerMoebiusOn S.prodPrimes muMinus) : ∑ d ∈ S.prodPrimes.divisors, muMinus d * BoundingSieve.multSum d ≤ BoundingSieve.siftedSum

The finite lower-Möbius expansion.

def MathlibNt.SieveTheory.LinearSieve.lowerErrSum (S : BoundingSieve) (D : ℕ) (muMinus : ℕ → ℝ) : ℝ

The error sum at a natural level. It deliberately contains only d < D; this is the finite error term occurring in the lower fundamental lemma.

Equations

• MathlibNt.SieveTheory.LinearSieve.lowerErrSum S D muMinus = ∑ d ∈ S.prodPrimes.divisors with d < D, |muMinus d| * |BoundingSieve.rem d|

def MathlibNt.SieveTheory.LinearSieve.HasLowerLevelSupport (P D : ℕ) (muMinus : ℕ → ℝ) : Prop

A coefficient sequence has level support if it vanishes outside the divisors below the level.

Equations

• MathlibNt.SieveTheory.LinearSieve.HasLowerLevelSupport P D muMinus = ∀ (d : ℕ), d ∣ P → ¬d < D → muMinus d = 0

theorem MathlibNt.SieveTheory.LinearSieve.errSum_eq_lowerErrSum {S : BoundingSieve} {D : ℕ} {muMinus : ℕ → ℝ} (hsupp : HasLowerLevelSupport S.prodPrimes D muMinus) : BoundingSieve.errSum muMinus = lowerErrSum S D muMinus

theorem MathlibNt.SieveTheory.LinearSieve.mainSum_sub_lowerErrSum_le_siftedSum {S : BoundingSieve} (D : ℕ) (muMinus : ℕ → ℝ) (hmu : IsLowerMoebiusOn S.prodPrimes muMinus) (hsupp : HasLowerLevelSupport S.prodPrimes D muMinus) : S.totalMass * BoundingSieve.mainSum muMinus - lowerErrSum S D muMinus ≤ BoundingSieve.siftedSum

Finite lower sieve inequality with its error sum explicitly restricted to the level.

def MathlibNt.SieveTheory.LinearSieve.LowerRosserAdmissibleSet (D : ℕ) (s : Finset ℕ) : Prop

The standard lower Rosser test on a finite set of distinct primes. For a prime p in an even position of the decreasing list, the filter is precisely the prefix p₁,…,p₂l; thus its test is p₁⋯p₂l₋₁ * p₂l^3 < D.

Equations

• MathlibNt.SieveTheory.LinearSieve.LowerRosserAdmissibleSet D s = ∀ p ∈ s, Even {q ∈ s | p ≤ q}.card → {q ∈ s | p ≤ q}.prod id * p ^ 2 < D

def MathlibNt.SieveTheory.LinearSieve.LowerRosserAdmissible (D d : ℕ) : Prop

The lower Rosser test for the prime factors of a natural number.

Equations

• MathlibNt.SieveTheory.LinearSieve.LowerRosserAdmissible D d = MathlibNt.SieveTheory.LinearSieve.LowerRosserAdmissibleSet D d.primeFactors

noncomputable def MathlibNt.SieveTheory.LinearSieve.lowerRosserSetWeight (D : ℕ) (s : Finset ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LinearSieve.lowerRosserSetWeight D s = if s.prod id < D ∧ MathlibNt.SieveTheory.LinearSieve.LowerRosserAdmissibleSet D s then if Even s.card then 1 else -1 else 0

theorem MathlibNt.SieveTheory.LinearSieve.Internal.sum_divisors_eq_sum_primeFactors_powerset {n : ℕ} (hn : Squarefree n) (f : ℕ → ℝ) : ∑ d ∈ n.divisors, f d = ∑ s ∈ n.primeFactors.powerset, f (s.prod id)

noncomputable def MathlibNt.SieveTheory.LinearSieve.lowerRosserWeight (P D d : ℕ) : ℝ

The explicit finite lower Rosser/Jurkat coefficient. The d < D clause is part of the finite-level convention; the source admissibility test is LowerRosserAdmissible.

Equations

• MathlibNt.SieveTheory.LinearSieve.lowerRosserWeight P D d = if d ∈ P.divisors ∧ d < D ∧ MathlibNt.SieveTheory.LinearSieve.LowerRosserAdmissible D d then if Even d.primeFactors.card then 1 else -1 else 0

theorem MathlibNt.SieveTheory.LinearSieve.lowerRosser_insert_min_active_iff_cube_lt {D q : ℕ} {s : Finset ℕ} (hqs : q ∉ s) (hqprime : Nat.Prime q) (hqmin : ∀ p ∈ s, q ≤ p) (hodd : ¬Even s.card) (hs : s.prod id < D ∧ LowerRosserAdmissibleSet D s) : (insert q s).prod id < D ∧ LowerRosserAdmissibleSet D (insert q s) ↔ s.prod id * q ^ 3 < D

For an active odd set, adjoining a new least prime remains active exactly until the cubic lower-Rosser cutoff q ^ 3 * ∏ s < D is crossed.

def MathlibNt.SieveTheory.LinearSieve.LowerRosserBoundarySet (D q : ℕ) (s : Finset ℕ) : Prop

The odd lower-Rosser boundary exposed when a new least prime is inserted.

Equations

• MathlibNt.SieveTheory.LinearSieve.LowerRosserBoundarySet D q s = (¬Even s.card ∧ s.prod id < D ∧ MathlibNt.SieveTheory.LinearSieve.LowerRosserAdmissibleSet D s ∧ ¬((insert q s).prod id < D ∧ MathlibNt.SieveTheory.LinearSieve.LowerRosserAdmissibleSet D (insert q s)))

theorem MathlibNt.SieveTheory.LinearSieve.lowerRosserBoundarySet_iff_cube_le {D q : ℕ} {s : Finset ℕ} (hqs : q ∉ s) (hqprime : Nat.Prime q) (hqmin : ∀ p ∈ s, q ≤ p) : LowerRosserBoundarySet D q s ↔ ¬Even s.card ∧ s.prod id < D ∧ LowerRosserAdmissibleSet D s ∧ D ≤ s.prod id * q ^ 3

The abstract odd lower-Rosser boundary is exactly the cubic shell D ≤ q ^ 3 * ∏ s once q is the new least prime.

theorem MathlibNt.SieveTheory.LinearSieve.lowerRosserSetWeight_insert_min_pair (nu : ℕ → ℝ) {D q : ℕ} {s : Finset ℕ} (hqs : q ∉ s) (hqprime : Nat.Prime q) (hqmin : ∀ p ∈ s, q ≤ p) (hodd : ¬Even s.card) (hs : s.prod id < D ∧ LowerRosserAdmissibleSet D s) : lowerRosserSetWeight D s + nu q * lowerRosserSetWeight D (insert q s) = (1 - nu q) * lowerRosserSetWeight D s - if LowerRosserBoundarySet D q s then nu q else 0

Exact lower-Rosser one-prime pairing on an active odd tail. The ordinary Euler factor survives away from the cubic shell, while crossing the shell contributes one negative boundary term.

noncomputable def MathlibNt.SieveTheory.LinearSieve.lowerRosserSetDensitySum (nu : ℕ → ℝ) (D : ℕ) (P : Finset ℕ) : ℝ

The finite lower Rosser density sum over subsets of a prescribed prime set. This is the lower-sieve counterpart of upperRosserSetDensitySum.

Equations

• MathlibNt.SieveTheory.LinearSieve.lowerRosserSetDensitySum nu D P = ∑ s ∈ P.powerset, MathlibNt.SieveTheory.LinearSieve.lowerRosserSetWeight D s * ∏ p ∈ s, nu p

theorem MathlibNt.SieveTheory.LinearSieve.lowerRosserSetWeight_insert_min_pair_all (nu : ℕ → ℝ) {D q : ℕ} {s : Finset ℕ} (hqs : q ∉ s) (hqprime : Nat.Prime q) (hqD : q < D) (hqmin : ∀ p ∈ s, q ≤ p) : lowerRosserSetWeight D s + nu q * lowerRosserSetWeight D (insert q s) = (1 - nu q) * lowerRosserSetWeight D s - if LowerRosserBoundarySet D q s then nu q else 0

Exact one-prime pairing, including inactive and even tails.

theorem MathlibNt.SieveTheory.LinearSieve.lowerRosserSetDensitySum_insert_min (nu : ℕ → ℝ) {D q : ℕ} {P : Finset ℕ} (hqP : q ∉ P) (hqprime : Nat.Prime q) (hqD : q < D) (hqmin : ∀ p ∈ P, q ≤ p) : lowerRosserSetDensitySum nu D (insert q P) = (1 - nu q) * lowerRosserSetDensitySum nu D P - nu q * ∑ s ∈ P.powerset with (LowerRosserBoundarySet D q) s, ∏ p ∈ s, nu p

Adjoining a new least prime gives the exact Euler factor, minus precisely its odd cubic-boundary contribution.

theorem MathlibNt.SieveTheory.LinearSieve.lowerRosserSetDensityRatio_insert_min (nu : ℕ → ℝ) {D q : ℕ} {P : Finset ℕ} (hq : q ∉ P) (hqprime : Nat.Prime q) (hqD : q < D) (hqmin : ∀ p ∈ P, q ≤ p) (hqFactor : 1 - nu q ≠ 0) (hPFactor : ∏ p ∈ P, (1 - nu p) ≠ 0) : lowerRosserSetDensitySum nu D (insert q P) / ∏ p ∈ insert q P, (1 - nu p) = lowerRosserSetDensitySum nu D P / ∏ p ∈ P, (1 - nu p) - nu q / (1 - nu q) * ((∑ s ∈ P.powerset with (LowerRosserBoundarySet D q) s, ∏ p ∈ s, nu p) / ∏ p ∈ P, (1 - nu p))

Euler-product-normalized form of the one-prime lower recurrence. This is pure finite algebra; the nonzero assumptions are kept explicit and no limiting or contraction statement is used.

Finite Euler-normalized lower recursion

This deliberately stays at one finite recursion step. In particular it does not package an all-depth tail or introduce a continuous majorant.

noncomputable def MathlibNt.SieveTheory.LinearSieve.lowerRosserSetRelativeDensity (nu : ℕ → ℝ) (D : ℕ) (P : Finset ℕ) : ℝ

The lower Rosser density on the relative Euler-product scale.

Equations

• MathlibNt.SieveTheory.LinearSieve.lowerRosserSetRelativeDensity nu D P = MathlibNt.SieveTheory.LinearSieve.lowerRosserSetDensitySum nu D P / ∏ p ∈ P, (1 - nu p)

noncomputable def MathlibNt.SieveTheory.LinearSieve.lowerRosserBoundaryRelativeDensity (nu : ℕ → ℝ) (D q : ℕ) (P : Finset ℕ) : ℝ

The finite odd-boundary correction on the same relative Euler-product scale as lowerRosserSetRelativeDensity.

Equations

• MathlibNt.SieveTheory.LinearSieve.lowerRosserBoundaryRelativeDensity nu D q P = (∑ s ∈ P.powerset with (MathlibNt.SieveTheory.LinearSieve.LowerRosserBoundarySet D q) s, ∏ p ∈ s, nu p) / ∏ p ∈ P, (1 - nu p)

theorem MathlibNt.SieveTheory.LinearSieve.lowerRosserSetRelativeDensity_insert_min (nu : ℕ → ℝ) {D q : ℕ} {P : Finset ℕ} (hqP : q ∉ P) (hqprime : Nat.Prime q) (hqD : q < D) (hqmin : ∀ p ∈ P, q ≤ p) (hqFactor : 1 - nu q ≠ 0) (hPFactor : ∏ p ∈ P, (1 - nu p) ≠ 0) : lowerRosserSetRelativeDensity nu D (insert q P) = lowerRosserSetRelativeDensity nu D P - nu q / (1 - nu q) * lowerRosserBoundaryRelativeDensity nu D q P

Exact normalized successor identity when a new least prime is adjoined. The lower recursion subtracts, rather than adds, its odd-boundary mass.

theorem MathlibNt.SieveTheory.LinearSieve.lowerRosserBoundaryRelativeDensity_nonneg (nu : ℕ → ℝ) {D q : ℕ} {P : Finset ℕ} (hnu : ∀ p ∈ P, 0 ≤ nu p) (hnuOne : ∀ p ∈ P, nu p < 1) : 0 ≤ lowerRosserBoundaryRelativeDensity nu D q P

A finite lower boundary has nonnegative relative density under the local sieve bounds 0 ≤ nu p < 1.

theorem MathlibNt.SieveTheory.LinearSieve.lowerRosserSetRelativeDensity_insert_min_le (nu : ℕ → ℝ) {D q : ℕ} {P : Finset ℕ} (hqP : q ∉ P) (hqprime : Nat.Prime q) (hqD : q < D) (hqmin : ∀ p ∈ P, q ≤ p) (hnuq : 0 ≤ nu q) (hnuqOne : nu q < 1) (hnu : ∀ p ∈ P, 0 ≤ nu p) (hnuOne : ∀ p ∈ P, nu p < 1) : lowerRosserSetRelativeDensity nu D (insert q P) ≤ lowerRosserSetRelativeDensity nu D P

Monotone normalized successor interface: adjoining a least prime can only decrease the relative lower density when 0 ≤ nu < 1.

theorem MathlibNt.SieveTheory.LinearSieve.lowerRosserSetRelativeDensity_empty (nu : ℕ → ℝ) {D : ℕ} (hD : 1 < D) : lowerRosserSetRelativeDensity nu D ∅ = 1

Terminal base for the finite normalized lower recursion.

theorem MathlibNt.SieveTheory.LinearSieve.lowerRosserSetDensitySum_insert_min_cube (nu : ℕ → ℝ) {D q : ℕ} {P : Finset ℕ} (hqP : q ∉ P) (hqprime : Nat.Prime q) (hqD : q < D) (hqmin : ∀ p ∈ P, q ≤ p) : lowerRosserSetDensitySum nu D (insert q P) = (1 - nu q) * lowerRosserSetDensitySum nu D P - nu q * ∑ s ∈ P.powerset with ¬Even s.card ∧ s.prod id < D ∧ LowerRosserAdmissibleSet D s ∧ D ≤ s.prod id * q ^ 3, ∏ p ∈ s, nu p

Cubic-shell form of lowerRosserSetDensitySum_insert_min.

noncomputable def MathlibNt.SieveTheory.LinearSieve.lowerRosserBoundaryMass (nu : ℕ → ℝ) (D q : ℕ) (P : Finset ℕ) : ℝ

The cubic-boundary mass lost when the new least prime q is inserted.

Equations

• MathlibNt.SieveTheory.LinearSieve.lowerRosserBoundaryMass nu D q P = ∑ s ∈ P.powerset with ¬Even s.card ∧ s.prod id < D ∧ MathlibNt.SieveTheory.LinearSieve.LowerRosserAdmissibleSet D s ∧ D ≤ s.prod id * q ^ 3, ∏ p ∈ s, nu p

noncomputable def MathlibNt.SieveTheory.LinearSieve.lowerRosserBoundaryAccum (nu : ℕ → ℝ) (D : ℕ) (P : Finset ℕ) : List ℕ → ℝ

The total (unnormalized) boundary loss in a finite sequence of least-prime insertions. Earlier losses are multiplied by all Euler factors inserted later.

Equations

• MathlibNt.SieveTheory.LinearSieve.lowerRosserBoundaryAccum nu D P [] = 0
• MathlibNt.SieveTheory.LinearSieve.lowerRosserBoundaryAccum nu D P (q :: qs) = (1 - nu q) * MathlibNt.SieveTheory.LinearSieve.lowerRosserBoundaryAccum nu D P qs + nu q * MathlibNt.SieveTheory.LinearSieve.lowerRosserBoundaryMass nu D q (List.foldr insert P qs)

theorem MathlibNt.SieveTheory.LinearSieve.lowerRosserSetDensitySum_foldr_insert (nu : ℕ → ℝ) (D : ℕ) (P : Finset ℕ) (qs : List ℕ) (hprime : ∀ q ∈ qs, Nat.Prime q) (hD : ∀ q ∈ qs, q < D) (hordered : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) qs) (hdisjoint : ∀ q ∈ qs, q ∉ P) (hbase : ∀ q ∈ qs, ∀ p ∈ P, q ≤ p) : lowerRosserSetDensitySum nu D (List.foldr insert P qs) = (List.map (fun (q : ℕ) => 1 - nu q) qs).prod * lowerRosserSetDensitySum nu D P - lowerRosserBoundaryAccum nu D P qs

Exact finite iteration of the lower Rosser density recurrence.

The list is ordered increasingly, so foldr insert P inserts its largest prime first and its smallest prime last. The formula uses no division by Euler factors; consequently it needs no positivity or nonvanishing hypothesis on 1 - nu q.

theorem MathlibNt.SieveTheory.LinearSieve.mainSum_lowerRosserWeight_eq_setDensitySum (S : BoundingSieve) (D : ℕ) : BoundingSieve.mainSum (lowerRosserWeight S.prodPrimes D) = lowerRosserSetDensitySum (⇑S.nu) D S.prodPrimes.primeFactors

The BoundingSieve.mainSum of the explicit lower Rosser coefficient is exactly its finite subset density sum. This is the first finite transport edge from Suzuki's Rosser--Iwaniec coefficient to the density recursion.

theorem MathlibNt.SieveTheory.LinearSieve.abs_lowerRosserWeight_le_one (P D d : ℕ) : |lowerRosserWeight P D d| ≤ 1

theorem MathlibNt.SieveTheory.LinearSieve.lowerRosserWeight_dvd {P D d : ℕ} (h : lowerRosserWeight P D d ≠ 0) : d ∣ P

theorem MathlibNt.SieveTheory.LinearSieve.lowerRosserWeight_lt_level {P D d : ℕ} (h : lowerRosserWeight P D d ≠ 0) : d < D

theorem MathlibNt.SieveTheory.LinearSieve.lowerRosserWeight_hasLowerLevelSupport (P D : ℕ) : HasLowerLevelSupport P D (lowerRosserWeight P D)

def MathlibNt.SieveTheory.LinearSieve.IsLowerRosserCertificate (P D : ℕ) : Prop

A finite Rosser certificate is the combinatorial toggle-min conclusion: even admissible subsets inject into odd admissible subsets. Its consequence is exactly the lower divisor-sum inequality needed by BoundingSieve.

Equations

• MathlibNt.SieveTheory.LinearSieve.IsLowerRosserCertificate P D = MathlibNt.SieveTheory.LinearSieve.IsLowerMoebiusOn P (MathlibNt.SieveTheory.LinearSieve.lowerRosserWeight P D)

theorem MathlibNt.SieveTheory.LinearSieve.lowerRosserWeight_certificate {P D : ℕ} (hP : Squarefree P) (hP0 : P ≠ 0) (hD : ∀ p ∈ P.primeFactors, p < D) : IsLowerRosserCertificate P D

The explicit lower Rosser weight is an unconditional finite lower-Möbius certificate for a squarefree prime product whose prime factors lie below the level.

theorem MathlibNt.SieveTheory.LinearSieve.lowerRosserWeight_divisor_sum {P D n : ℕ} (hcert : IsLowerRosserCertificate P D) (hn : n ∣ P) : ∑ d ∈ n.divisors, lowerRosserWeight P D d ≤ if n = 1 then 1 else 0

A certified lower Rosser weight supplies the finite divisor-sum lower bound, while retaining the explicit source formula above.