Rounded cubic tests with the source's occurrence indexing

Iwaniec's p. 311 admissibility tests use decreasing lower endpoints and zero-based parity; the finite Rosser tests on p. 313 use inclusive prime prefixes and their cardinality. This module identifies these tests by sorting the original natural-number labels, never their endpoint values. Thus equal values of b keep distinct slots in every mapped prefix product.

def MathlibNt.SieveTheory.LiLiuPrereqWF.RoundedSetAdmissible (upper : Bool) (b : ℕ → ℝ) (D : ℝ) (s : Finset ℕ) : Prop

Inclusive decreasing-prime prefixes, evaluated at rounded endpoints. The parity is one-based: odd for the upper side, even for the lower side.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.RoundedSetAdmissible upper b D s = ∀ p ∈ s, ({q ∈ s | p ≤ q}.card % 2 = if upper = true then 1 else 0) → (∏ q ∈ s with p ≤ q, b q) * b p ^ 2 < D

@[simp]

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.roundedSetAdmissible_empty (upper : Bool) (b : ℕ → ℝ) (D : ℝ) : RoundedSetAdmissible upper b D ∅

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.rounded_prefix_eq_take (s : Finset ℕ) (i : ℕ) (hi : i < (s.sort fun (x1 x2 : ℕ) => x1 ≥ x2).length) : {q ∈ s | (s.sort fun (x1 x2 : ℕ) => x1 ≥ x2)[i] ≤ q} = (List.take (i + 1) (s.sort fun (x1 x2 : ℕ) => x1 ≥ x2)).toFinset

The inclusive prime prefix is exactly the first i + 1 original slots.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.rounded_prefix_card (s : Finset ℕ) (i : ℕ) (hi : i < (s.sort fun (x1 x2 : ℕ) => x1 ≥ x2).length) : {q ∈ s | (s.sort fun (x1 x2 : ℕ) => x1 ≥ x2)[i] ≤ q}.card = i + 1

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.rounded_prefix_product (b : ℕ → ℝ) (s : Finset ℕ) (i : ℕ) (hi : i < (s.sort fun (x1 x2 : ℕ) => x1 ≥ x2).length) : (∏ q ∈ s with (s.sort fun (x1 x2 : ℕ) => x1 ≥ x2)[i] ≤ q, b q) * b (s.sort fun (x1 x2 : ℕ) => x1 ≥ x2)[i] ^ 2 = (List.map b (List.take i (s.sort fun (x1 x2 : ℕ) => x1 ≥ x2))).prod * b (s.sort fun (x1 x2 : ℕ) => x1 ≥ x2)[i] ^ 3

No injectivity of b is needed: the product ranges over prime slots.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.roundedSetAdmissible_iff_cubicPrefixBound (upper : Bool) (b : ℕ → ℝ) (D : ℝ) (s : Finset ℕ) : RoundedSetAdmissible upper b D s ↔ LiLiuPrereqWFAdmissibility.CubicPrefixBound upper b D (s.sort fun (x1 x2 : ℕ) => x1 ≥ x2)

Exact equivalence of the finite tests with the source's zero-based cubic tests, including the empty set and coincident endpoint values.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.roundedSetAdmissible_to_admissible {upper : Bool} {b : ℕ → ℝ} {D : ℝ} {s : Finset ℕ} (hone : ∀ p ∈ s, 1 ≤ b p) (hmono : ∀ p ∈ s, ∀ q ∈ s, p ≤ q → b p ≤ b q) (hsq : ∀ p ∈ s, b p ^ 2 < D) (h : RoundedSetAdmissible upper b D s) : LiLiuPrereqWFAdmissibility.Admissible upper b D (s.sort fun (x1 x2 : ℕ) => x1 ≥ x2)

The numerical side conditions plus finite rounded tests give the actual source admissibility, with all original prime occurrences retained.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.roundedSetAdmissible_iff_admissible {upper : Bool} {b : ℕ → ℝ} {D : ℝ} {s : Finset ℕ} (hone : ∀ p ∈ s, 1 ≤ b p) (hmono : ∀ p ∈ s, ∀ q ∈ s, p ≤ q → b p ≤ b q) (hsq : ∀ p ∈ s, b p ^ 2 < D) : RoundedSetAdmissible upper b D s ↔ LiLiuPrereqWFAdmissibility.Admissible upper b D (s.sort fun (x1 x2 : ℕ) => x1 ≥ x2)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.rounded_sorted_map_length (b : ℕ → ℝ) (s : Finset ℕ) : (List.map b (s.sort fun (x1 x2 : ℕ) => x1 ≥ x2)).length = s.card

Mapping endpoints does not remove equal entries.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.roundedSetAdmissible_cast_lower_iff (D : ℝ) (s : Finset ℕ) : RoundedSetAdmissible false (fun (p : ℕ) => ↑p) D s ↔ SmallRosser.LowerAdmissibleSet D s

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.roundedSetAdmissible_cast_upper_iff (D : ℝ) (s : Finset ℕ) : RoundedSetAdmissible true (fun (p : ℕ) => ↑p) D s ↔ SmallRosser.UpperAdmissibleSet D s