The actual geometric prime boxes

The lower grid is D^(ε²(1+θ)^j) and each box is the half-open interval from one grid point to the next, intersected with a fixed finite sieve prime set. Thus distinct labels give disjoint prime ranges, while repeated labels retain all their divided-power multiplicity.

The final theorem specializes to Iwaniec's θ = ε⁹ and source numerical admissibility. It includes a fixed supplied small-prime weight. The subsequent LiLiuPrereqWFSmallRosser supplies concrete upper/lower weights and their finite sieve inequalities; their density remains a separate obligation.

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.geometricLower (D ε θ : ℝ) (j : ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.geometricLower D ε θ j = D ^ (ε ^ 2 * (1 + θ) ^ j)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.geometricLower_one_le {D ε θ : ℝ} (hD : 1 ≤ D) (hθ : 0 ≤ θ) (j : ℕ) : 1 ≤ geometricLower D ε θ j

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.geometricLower_monotone {D ε θ : ℝ} (hD : 1 ≤ D) (hθ : 0 ≤ θ) : Monotone (geometricLower D ε θ)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.geometricLower_succ {D ε θ : ℝ} (hD : 0 ≤ D) (j : ℕ) : geometricLower D ε θ (j + 1) = geometricLower D ε θ j ^ (1 + θ)

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.geometricPrimeBox (P : Finset ℕ) (D ε θ : ℝ) (j : ℕ) : Finset ℕ

P is the fixed finite set of sieve primes below the desired cutoff.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.geometricPrimeBox P D ε θ j = {p ∈ P | Nat.Prime p ∧ MathlibNt.SieveTheory.LiLiuPrereqWF.geometricLower D ε θ j ≤ ↑p ∧ ↑p < MathlibNt.SieveTheory.LiLiuPrereqWF.geometricLower D ε θ (j + 1)}

@[simp]

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.mem_geometricPrimeBox (P : Finset ℕ) (D ε θ : ℝ) (j p : ℕ) : p ∈ geometricPrimeBox P D ε θ j ↔ p ∈ P ∧ Nat.Prime p ∧ geometricLower D ε θ j ≤ ↑p ∧ ↑p < geometricLower D ε θ (j + 1)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.geometricPrimeBox_upper (P : Finset ℕ) {D ε θ : ℝ} (hD : 0 ≤ D) (j p : ℕ) (hp : p ∈ geometricPrimeBox P D ε θ j) : ↑p < geometricLower D ε θ j ^ (1 + θ)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.geometricPrimeBox_disjoint (P : Finset ℕ) {D ε θ : ℝ} (hD : 1 ≤ D) (hθ : 0 ≤ θ) {i j : ℕ} (hij : i ≠ j) : Disjoint (geometricPrimeBox P D ε θ i) (geometricPrimeBox P D ε θ j)

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.geometricSmallPrimes (P : Finset ℕ) (D ε : ℝ) : Finset ℕ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.geometricSmallPrimes P D ε = {p ∈ P | Nat.Prime p ∧ ↑p < D ^ ε ^ 2}

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.geometricSmallPrimes_disjoint (P : Finset ℕ) {D ε θ : ℝ} (hD : 1 ≤ D) (hθ : 0 ≤ θ) (s : Finset ℕ) : Disjoint (geometricSmallPrimes P D ε) (s.biUnion (geometricPrimeBox P D ε θ))

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.geometricBoxTerm (P : Finset ℕ) (D ε θ : ℝ) (input : List ℕ) (ψ : ArithmeticFunction ℝ) : ArithmeticFunction ℝ

A fixed normalized box term with its small coefficient function.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.geometricBoxTerm P D ε θ input ψ = ψ * MathlibNt.SieveTheory.LiLiuPrereqWF.boxProduct input.toFinset (MathlibNt.SieveTheory.LiLiuPrereqWF.geometricPrimeBox P D ε θ) fun (a : ℕ) => List.count a input

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.geometricBoxTerm_wellFactorable (P : Finset ℕ) {upper : Bool} {D ε θ : ℝ} (input : List ℕ) (ψ : ArithmeticFunction ℝ) (hD : 1 ≤ D) (hε : 0 ≤ ε) (hθ : 0 ≤ θ) (hεθ : ε ≤ 1 + θ) (hadm : LiLiuPrereqWFAdmissibility.Admissible upper (geometricLower D ε θ) D input) (hψp : PrimeSupported (geometricSmallPrimes P D ε) ψ) (hψb : BoundedOne ψ) (hψs : SupportedAt ψ (D ^ ε)) : WellFactorable (geometricBoxTerm P D ε θ input ψ) (D ^ (1 + ε + θ))

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.iwaniec_boxTerm_wellFactorable (P : Finset ℕ) {upper : Bool} {D ε : ℝ} (input : List ℕ) (ψ : ArithmeticFunction ℝ) (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) (hadm : LiLiuPrereqWFAdmissibility.Admissible upper (geometricLower D ε (ε ^ 9)) D input) (hψp : PrimeSupported (geometricSmallPrimes P D ε) ψ) (hψb : BoundedOne ψ) (hψs : SupportedAt ψ (D ^ ε)) : WellFactorable (geometricBoxTerm P D ε (ε ^ 9) input ψ) (D ^ (1 + ε + ε ^ 9))

Source parameters: θ = ε⁹, 0 < ε < 1/8, D ≥ 2. No numerical prefix budget, disjointness, or support allocation is left as an input.