Concrete lower and upper small-prime Rosser weights

Iwaniec, A new form of the error term in the linear sieve (1980), p.313, defines the lower coefficient by the even-prefix cubic tests and the upper coefficient by the odd-prefix tests. Here a prefix ending in p is the set of prime factors at least p: its product times p² is the displayed cubic expression. The level is real, so the cutoff at D^ε is strict, without rounding.

The small weight of p.316, Lemma 4, is this coefficient restricted to the small sieve prime product. The finite cancellation argument is independent of the density assertion in that lemma. No density or asymptotic estimate is asserted here.

def MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.LowerAdmissibleSet (L : ℝ) (s : Finset ℕ) : Prop

The even-prefix test for the lower Rosser coefficient, with real level.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.LowerAdmissibleSet L s = ∀ p ∈ s, Even {q ∈ s | p ≤ q}.card → ↑({q ∈ s | p ≤ q}.prod id) * ↑p ^ 2 < L

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerWeight (M : ℕ) (L : ℝ) : ArithmeticFunction ℝ

The coefficient is (-1)^ω(n) on admissible divisors below the level and zero elsewhere. In applications M is a squarefree prime product.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerWeight M L = { toFun := fun (n : ℕ) => if n ∈ M.divisors ∧ ↑n < L ∧ MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.LowerAdmissibleSet L n.primeFactors then (-1) ^ n.primeFactors.card else 0, map_zero' := ⋯ }

@[simp]

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerWeight_apply (M n : ℕ) (L : ℝ) : (lowerWeight M L) n = if n ∈ M.divisors ∧ ↑n < L ∧ LowerAdmissibleSet L n.primeFactors then (-1) ^ n.primeFactors.card else 0

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerWeight_eq_producer (M : ℕ) (L : ℝ) : ⇑(lowerWeight M L) = LinearSieve.lowerRosserWeight M ⌈L⌉₊

Exact real-level/natural-ceiling bridge, before finite certificates.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerWeight_active {M n : ℕ} {L : ℝ} (h : (lowerWeight M L) n ≠ 0) : n ∈ M.divisors ∧ ↑n < L ∧ LowerAdmissibleSet L n.primeFactors

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerWeight_boundedOne (M : ℕ) (L : ℝ) : BoundedOne (lowerWeight M L)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerWeight_lt_level {M n : ℕ} {L : ℝ} (h : (lowerWeight M L) n ≠ 0) : ↑n < L

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerWeight_eq_zero_of_level_le {M n : ℕ} {L : ℝ} (h : L ≤ ↑n) : (lowerWeight M L) n = 0

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerWeight_supportedAt (M : ℕ) (L : ℝ) : SupportedAt (lowerWeight M L) L

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerWeight_dvd {M n : ℕ} {L : ℝ} (h : (lowerWeight M L) n ≠ 0) : n ∣ M

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerWeight_squarefree {M n : ℕ} {L : ℝ} (hM : Squarefree M) (h : (lowerWeight M L) n ≠ 0) : Squarefree n

@[simp]

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerWeight_one {M : ℕ} {L : ℝ} (hM : M ≠ 0) (hL : 1 < L) : (lowerWeight M L) 1 = 1

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerWeight_prime {M p : ℕ} {L : ℝ} (hM : M ≠ 0) (hp : Nat.Prime p) (hpd : p ∣ M) (hpL : ↑p < L) : (lowerWeight M L) p = -1

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerWeight_primeSupported (B : Finset ℕ) (L : ℝ) (hB : ∀ p ∈ B, Nat.Prime p) : PrimeSupported B (lowerWeight (B.prod id) L)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.primeProduct_squarefree (B : Finset ℕ) (hB : ∀ p ∈ B, Nat.Prime p) : Squarefree (B.prod id)

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerSmallWeight (P : Finset ℕ) (D ε : ℝ) : ArithmeticFunction ℝ

The actual lower small-prime function, fixed before the box and its splits.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerSmallWeight P D ε = MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerWeight ((MathlibNt.SieveTheory.LiLiuPrereqWF.geometricSmallPrimes P D ε).prod id) (D ^ ε)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.smallPrimes_prime (P : Finset ℕ) (D ε : ℝ) (p : ℕ) : p ∈ geometricSmallPrimes P D ε → Nat.Prime p

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerSmallWeight_boundedOne (P : Finset ℕ) (D ε : ℝ) : BoundedOne (lowerSmallWeight P D ε)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerSmallWeight_primeSupported (P : Finset ℕ) (D ε : ℝ) : PrimeSupported (geometricSmallPrimes P D ε) (lowerSmallWeight P D ε)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerSmallWeight_lt_level {P : Finset ℕ} {D ε : ℝ} {n : ℕ} (hn : (lowerSmallWeight P D ε) n ≠ 0) : ↑n < D ^ ε

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerSmallWeight_eq_zero_of_level_le {P : Finset ℕ} {D ε : ℝ} {n : ℕ} (hn : D ^ ε ≤ ↑n) : (lowerSmallWeight P D ε) n = 0

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerSmallWeight_supportedAt (P : Finset ℕ) (D ε : ℝ) : SupportedAt (lowerSmallWeight P D ε) (D ^ ε)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerSmallWeight_squarefree {P : Finset ℕ} {D ε : ℝ} {n : ℕ} (hn : (lowerSmallWeight P D ε) n ≠ 0) : Squarefree n

@[simp]

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerSmallWeight_one (P : Finset ℕ) {D ε : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) : (lowerSmallWeight P D ε) 1 = 1

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.smallPrime_lt_level (P : Finset ℕ) {D ε : ℝ} (hD : 1 ≤ D) (hε : 0 ≤ ε) (hε1 : ε ≤ 1) {p : ℕ} (hp : p ∈ geometricSmallPrimes P D ε) : ↑p < D ^ ε

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerSmallWeight_prime (P : Finset ℕ) {D ε : ℝ} (hD : 1 ≤ D) (hε : 0 ≤ ε) (hε1 : ε ≤ 1) {p : ℕ} (hp : p ∈ geometricSmallPrimes P D ε) : (lowerSmallWeight P D ε) p = -1

Every small prime has coefficient -1; this is not a delta weight.

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerBoxTerm (P : Finset ℕ) (D ε : ℝ) (input : List ℕ) : ArithmeticFunction ℝ

One concrete lower-small-weight geometric box term.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerBoxTerm P D ε input = MathlibNt.SieveTheory.LiLiuPrereqWF.geometricBoxTerm P D ε (ε ^ 9) input (MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerSmallWeight P D ε)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.iwaniec_lowerBoxTerm_wellFactorable (P : Finset ℕ) {upper : Bool} {D ε : ℝ} (input : List ℕ) (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) (hadm : LiLiuPrereqWFAdmissibility.Admissible upper (geometricLower D ε (ε ^ 9)) D input) : WellFactorable (lowerBoxTerm P D ε input) (D ^ (1 + ε + ε ^ 9))

No supplied function, support, or boundedness hypothesis remains. The actual small weight and the box term precede all real level splits.

Finite lower-sieve direction

The following least-prime pairing is a narrow real-level adaptation of the finite argument in LinearSieve.lean, not an import of its analytic closure.

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.setWeight (L : ℝ) (s : Finset ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.setWeight L s = if ↑(s.prod id) < L ∧ MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.LowerAdmissibleSet L s then if Even s.card then 1 else -1 else 0

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.admissible_insert_min_of_even {L : ℝ} {q : ℕ} {s : Finset ℕ} (hqs : q ∉ s) (hqmin : ∀ p ∈ s, q ≤ p) (hs : LowerAdmissibleSet L s) (heven : Even s.card) : LowerAdmissibleSet L (insert q s)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.admissible_of_insert_min {L : ℝ} {q : ℕ} {s : Finset ℕ} (hqs : q ∉ s) (hqmin : ∀ p ∈ s, q ≤ p) (hs : LowerAdmissibleSet L (insert q s)) : LowerAdmissibleSet L s

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.prod_insert_min_lt_of_even {L : ℝ} {q : ℕ} {s : Finset ℕ} (hqs : q ∉ s) (hqprime : Nat.Prime q) (hqL : ↑q < L) (hqmin : ∀ p ∈ s, q ≤ p) (hs : LowerAdmissibleSet L s) (heven : Even s.card) : ↑((insert q s).prod id) < L

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.sum_powerset_insert_pairs (f : Finset ℕ → ℝ) {q : ℕ} {T : Finset ℕ} (hqT : q ∉ T) : ∑ s ∈ (insert q T).powerset, f s = ∑ s ∈ T.powerset, (f s + f (insert q s))

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

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerWeight_prod_eq_setWeight {M : ℕ} {L : ℝ} (hM : Squarefree M) {s : Finset ℕ} (hsub : s ⊆ M.primeFactors) : (lowerWeight M L) (s.prod id) = setWeight L s

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerWeight_divisor_sum {M n : ℕ} {L : ℝ} (hM : Squarefree M) (hL : ∀ p ∈ M.primeFactors, ↑p < L) (hn : n ∣ M) : ∑ d ∈ n.divisors, (lowerWeight M L) d ≤ if n = 1 then 1 else 0

Unconditional finite lower-divisor-sum inequality for the explicit coefficient. The hypotheses concern only the squarefree sieve prime product and the prime cutoff, not a certificate or a sieve conclusion.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerSmallWeight_divisor_sum (P : Finset ℕ) {D ε : ℝ} {n : ℕ} (hD : 1 ≤ D) (hε : 0 ≤ ε) (hε1 : ε ≤ 1) (hn : n ∣ (geometricSmallPrimes P D ε).prod id) : ∑ d ∈ n.divisors, (lowerSmallWeight P D ε) d ≤ if n = 1 then 1 else 0

The actual lower small weight satisfies the finite lower-sieve direction on every divisor of its small prime product, in particular for 0 < ε < 1/8.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerWeight_divisor_sum_le_coprime {M n : ℕ} {L : ℝ} (hM : Squarefree M) (hL : ∀ p ∈ M.primeFactors, ↑p < L) : ∑ d ∈ n.divisors, (lowerWeight M L) d ≤ if n.Coprime M then 1 else 0

The finite lower-sieve direction on all natural numbers, obtained by restricting the divisor sum to gcd(n,M). Prime powers cause no loss.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerSmallWeight_divisor_sum_le_coprime (P : Finset ℕ) {D ε : ℝ} (hD : 1 ≤ D) (hε : 0 ≤ ε) (hε1 : ε ≤ 1) (n : ℕ) : ∑ d ∈ n.divisors, (lowerSmallWeight P D ε) d ≤ if n.Coprime ((geometricSmallPrimes P D ε).prod id) then 1 else 0

The concrete small-prime weight is a lower bound for the indicator of integers coprime to its sieve prime product. This is finite, not a density estimate.

Concrete upper small weight

def MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.UpperAdmissibleSet (L : ℝ) (s : Finset ℕ) : Prop

The odd-prefix cubic test for the upper Rosser coefficient.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.UpperAdmissibleSet L s = ∀ p ∈ s, ¬Even {q ∈ s | p ≤ q}.card → ↑({q ∈ s | p ≤ q}.prod id) * ↑p ^ 2 < L

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperWeight (M : ℕ) (L : ℝ) : ArithmeticFunction ℝ

The upper coefficient with a strict real cutoff and odd-prefix tests.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperWeight M L = { toFun := fun (n : ℕ) => if n ∈ M.divisors ∧ ↑n < L ∧ MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.UpperAdmissibleSet L n.primeFactors then (-1) ^ n.primeFactors.card else 0, map_zero' := ⋯ }

@[simp]

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperWeight_apply (M n : ℕ) (L : ℝ) : (upperWeight M L) n = if n ∈ M.divisors ∧ ↑n < L ∧ UpperAdmissibleSet L n.primeFactors then (-1) ^ n.primeFactors.card else 0

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperWeight_eq_producer (M : ℕ) (L : ℝ) : ⇑(upperWeight M L) = LinearSieve.upperRosserWeight M ⌈L⌉₊

Exact real-level/natural-ceiling bridge, before finite certificates.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperWeight_active {M n : ℕ} {L : ℝ} (h : (upperWeight M L) n ≠ 0) : n ∈ M.divisors ∧ ↑n < L ∧ UpperAdmissibleSet L n.primeFactors

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperWeight_boundedOne (M : ℕ) (L : ℝ) : BoundedOne (upperWeight M L)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperWeight_lt_level {M n : ℕ} {L : ℝ} (h : (upperWeight M L) n ≠ 0) : ↑n < L

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperWeight_eq_zero_of_level_le {M n : ℕ} {L : ℝ} (h : L ≤ ↑n) : (upperWeight M L) n = 0

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperWeight_supportedAt (M : ℕ) (L : ℝ) : SupportedAt (upperWeight M L) L

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperWeight_dvd {M n : ℕ} {L : ℝ} (h : (upperWeight M L) n ≠ 0) : n ∣ M

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperWeight_squarefree {M n : ℕ} {L : ℝ} (hM : Squarefree M) (h : (upperWeight M L) n ≠ 0) : Squarefree n

@[simp]

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperWeight_one {M : ℕ} {L : ℝ} (hM : M ≠ 0) (hL : 1 < L) : (upperWeight M L) 1 = 1

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperWeight_prime {M p : ℕ} {L : ℝ} (hM : M ≠ 0) (hp : Nat.Prime p) (hpd : p ∣ M) (hpL : ↑p ^ 3 < L) : (upperWeight M L) p = -1

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperWeight_primeSupported (B : Finset ℕ) (L : ℝ) (hB : ∀ p ∈ B, Nat.Prime p) : PrimeSupported B (upperWeight (B.prod id) L)

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSmallWeight (P : Finset ℕ) (D ε : ℝ) : ArithmeticFunction ℝ

The actual upper small-prime function, fixed before the box and its splits.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSmallWeight P D ε = MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperWeight ((MathlibNt.SieveTheory.LiLiuPrereqWF.geometricSmallPrimes P D ε).prod id) (D ^ ε)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSmallWeight_boundedOne (P : Finset ℕ) (D ε : ℝ) : BoundedOne (upperSmallWeight P D ε)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSmallWeight_primeSupported (P : Finset ℕ) (D ε : ℝ) : PrimeSupported (geometricSmallPrimes P D ε) (upperSmallWeight P D ε)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSmallWeight_lt_level {P : Finset ℕ} {D ε : ℝ} {n : ℕ} (hn : (upperSmallWeight P D ε) n ≠ 0) : ↑n < D ^ ε

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSmallWeight_eq_zero_of_level_le {P : Finset ℕ} {D ε : ℝ} {n : ℕ} (hn : D ^ ε ≤ ↑n) : (upperSmallWeight P D ε) n = 0

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSmallWeight_supportedAt (P : Finset ℕ) (D ε : ℝ) : SupportedAt (upperSmallWeight P D ε) (D ^ ε)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSmallWeight_squarefree {P : Finset ℕ} {D ε : ℝ} {n : ℕ} (hn : (upperSmallWeight P D ε) n ≠ 0) : Squarefree n

@[simp]

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSmallWeight_one (P : Finset ℕ) {D ε : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) : (upperSmallWeight P D ε) 1 = 1

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSmallWeight_prime (P : Finset ℕ) {D ε : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) {p : ℕ} (hp : p ∈ geometricSmallPrimes P D ε) : (upperSmallWeight P D ε) p = -1

Under the small-parameter hypothesis every small prime passes the upper cubic test, so the concrete upper weight is not a delta weight.

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperBoxTerm (P : Finset ℕ) (D ε : ℝ) (input : List ℕ) : ArithmeticFunction ℝ

One concrete upper-small-weight geometric box term.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperBoxTerm P D ε input = MathlibNt.SieveTheory.LiLiuPrereqWF.geometricBoxTerm P D ε (ε ^ 9) input (MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSmallWeight P D ε)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.iwaniec_upperBoxTerm_wellFactorable (P : Finset ℕ) {upper : Bool} {D ε : ℝ} (input : List ℕ) (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) (hadm : LiLiuPrereqWFAdmissibility.Admissible upper (geometricLower D ε (ε ^ 9)) D input) : WellFactorable (upperBoxTerm P D ε input) (D ^ (1 + ε + ε ^ 9))

The upper small weight needs no supplied function or support certificate. The conclusion holds for either admissible geometric-box parity.

Finite upper-sieve direction

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSetWeight (L : ℝ) (s : Finset ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSetWeight L s = if ↑(s.prod id) < L ∧ MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.UpperAdmissibleSet L s then if Even s.card then 1 else -1 else 0

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperAdmissible_insert_min_of_odd {L : ℝ} {q : ℕ} {s : Finset ℕ} (hqs : q ∉ s) (hqmin : ∀ p ∈ s, q ≤ p) (hs : UpperAdmissibleSet L s) (hodd : ¬Even s.card) : UpperAdmissibleSet L (insert q s)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperAdmissible_of_insert_min {L : ℝ} {q : ℕ} {s : Finset ℕ} (hqs : q ∉ s) (hqmin : ∀ p ∈ s, q ≤ p) (hs : UpperAdmissibleSet L (insert q s)) : UpperAdmissibleSet L s

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.prod_insert_min_lt_of_odd {L : ℝ} {q : ℕ} {s : Finset ℕ} (hqs : q ∉ s) (hqprime : Nat.Prime q) (hqmin : ∀ p ∈ s, q ≤ p) (hs : UpperAdmissibleSet L s) (hodd : ¬Even s.card) : ↑((insert q s).prod id) < L

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperWeight_prod_eq_setWeight {M : ℕ} {L : ℝ} (hM : Squarefree M) {s : Finset ℕ} (hsub : s ⊆ M.primeFactors) : (upperWeight M L) (s.prod id) = upperSetWeight L s

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperWeight_divisor_sum {M n : ℕ} {L : ℝ} (hM : Squarefree M) (hL : 1 < L) (hn : n ∣ M) : (if n = 1 then 1 else 0) ≤ ∑ d ∈ n.divisors, (upperWeight M L) d

The finite upper-sieve direction on divisors of a squarefree sieve product. Only 1 < L is required: there is no prime cutoff hypothesis.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSmallWeight_divisor_sum_of_le_one (P : Finset ℕ) {D ε : ℝ} {n : ℕ} (hD : 2 ≤ D) (hε : 0 < ε) (hε1 : ε ≤ 1) (hn : n ∣ (geometricSmallPrimes P D ε).prod id) : (if n = 1 then 1 else 0) ≤ ∑ d ∈ n.divisors, (upperSmallWeight P D ε) d

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSmallWeight_divisor_sum (P : Finset ℕ) {D ε : ℝ} {n : ℕ} (hD : 2 ≤ D) (hε : 0 < ε) (hn : n ∣ (geometricSmallPrimes P D ε).prod id) : (if n = 1 then 1 else 0) ≤ ∑ d ∈ n.divisors, (upperSmallWeight P D ε) d

The wider legacy API is retained: ε need not be at most one.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperWeight_divisor_sum_ge_coprime {M n : ℕ} {L : ℝ} (hM : Squarefree M) (hL : 1 < L) (hn : n ≠ 0) : (if n.Coprime M then 1 else 0) ≤ ∑ d ∈ n.divisors, (upperWeight M L) d

The finite upper-sieve direction on positive integers, including prime powers, by restriction to gcd(n,M). The exclusion of zero is essential for the empty-divisors convention when M = 1.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSmallWeight_divisor_sum_ge_coprime (P : Finset ℕ) {D ε : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) {n : ℕ} (hn : n ≠ 0) : (if n.Coprime ((geometricSmallPrimes P D ε).prod id) then 1 else 0) ≤ ∑ d ∈ n.divisors, (upperSmallWeight P D ε) d

The concrete small-prime upper coefficient bounds the coprimality indicator on every positive integer; no density estimate is asserted.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerSmallWeight_wellFactorable (P : Finset ℕ) {D ε : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) : WellFactorable (lowerSmallWeight P D ε) (D ^ (1 + ε + ε ^ 9))

The short lower weight itself is common WF at the external level.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSmallWeight_wellFactorable (P : Finset ℕ) {D ε : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) : WellFactorable (upperSmallWeight P D ε) (D ^ (1 + ε + ε ^ 9))

The short upper weight itself is common WF at the external level.