Iwaniec's numerical admissibility and lower-endpoint allocation

The numerical conditions are those defining 𝒟⁺ and 𝒟⁻ on p. 311 of H. Iwaniec, A new form of the error term in the linear sieve (1980), as checked in the right page of pages/iwaniec-3.png. The empty sequence is admitted, as stipulated at the bottom of that page.

Here b assigns the lower endpoint to each label. Geometric-grid membership is deliberately separate from these numerical conditions. With zero-based indexing, upper (true) cubic tests occur at even indices, and lower (false) tests occur at odd indices. The head restriction is retained for both sides.

The strict prefix-square estimate proves the numerical input to the two-box induction of Lemma 1, p. 312 (pages/iwaniec-4.png, left page). The resulting partition preserves occurrences, including repeated labels. No assertion that the two subsequences retain the original parity conditions is made here.

def MathlibNt.SieveTheory.LiLiuPrereqWFAdmissibility.CubicPrefixBound {ι : Type u_1} (upper : Bool) (b : ι → ℝ) (D : ℝ) (input : List ι) : Prop

The p. 311 cubic test, with upper/even and lower/odd zero-based parity.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWFAdmissibility.CubicPrefixBound upper b D input = ∀ (i : ℕ) (hi : i < input.length), (i % 2 = if upper = true then 0 else 1) → (List.map b (List.take i input)).prod * b input[i] ^ 3 < D

theorem MathlibNt.SieveTheory.LiLiuPrereqWFAdmissibility.cubicPrefixBound_upper_iff {ι : Type u_1} (b : ι → ℝ) (D : ℝ) (input : List ι) : CubicPrefixBound true b D input ↔ ∀ (ℓ : ℕ) (hℓ : 2 * ℓ < input.length), (List.map b (List.take (2 * ℓ) input)).prod * b input[2 * ℓ] ^ 3 < D

The upper condition is exactly the source's tests at one-based 2ℓ + 1.

theorem MathlibNt.SieveTheory.LiLiuPrereqWFAdmissibility.cubicPrefixBound_lower_iff {ι : Type u_1} (b : ι → ℝ) (D : ℝ) (input : List ι) : CubicPrefixBound false b D input ↔ ∀ (ℓ : ℕ), 1 ≤ ℓ → ∀ (hℓ : 2 * ℓ - 1 < input.length), (List.map b (List.take (2 * ℓ - 1) input)).prod * b input[2 * ℓ - 1] ^ 3 < D

The lower condition is exactly the source's tests at one-based 2ℓ, with ℓ ≥ 1, not at the upper side's odd one-based indices.

structure MathlibNt.SieveTheory.LiLiuPrereqWFAdmissibility.Admissible {ι : Type u_1} (upper : Bool) (b : ι → ℝ) (D : ℝ) (input : List ι) : Prop

Actual numerical admissibility of a decreasing lower-endpoint sequence. The fields are the source's inequalities, not an allocation or prefix-square conclusion. All four conditions are vacuous on the empty sequence.

• one_le (a : ι) : a ∈ input → 1 ≤ b a
• decreasing (i j : ℕ) (hi : i < input.length) (hj : j < input.length) : i ≤ j → b input[j] ≤ b input[i]
• head_lt_sqrt (h : 0 < input.length) : b input[0] < √D
• cubic : CubicPrefixBound upper b D input

@[simp]

theorem MathlibNt.SieveTheory.LiLiuPrereqWFAdmissibility.admissible_nil {ι : Type u_1} (upper : Bool) (b : ι → ℝ) (D : ℝ) : Admissible upper b D []

theorem MathlibNt.SieveTheory.LiLiuPrereqWFAdmissibility.head_lt_sqrt_iff_sq_lt {ι : Type u_1} {b : ι → ℝ} {D : ℝ} {input : List ι} (hone : ∀ a ∈ input, 1 ≤ b a) (h : 0 < input.length) : b input[0] < √D ↔ b input[0] ^ 2 < D

The source head restriction and its squared form are equivalent; the lower-endpoint assumption supplies the necessary nonnegative head.

theorem MathlibNt.SieveTheory.LiLiuPrereqWFAdmissibility.Admissible.head_sq_lt {ι : Type u_1} {upper : Bool} {b : ι → ℝ} {D : ℝ} {input : List ι} (h : Admissible upper b D input) (hinput : 0 < input.length) : b input[0] ^ 2 < D

theorem MathlibNt.SieveTheory.LiLiuPrereqWFAdmissibility.Admissible.prefix_prod_nonneg {ι : Type u_1} {upper : Bool} {b : ι → ℝ} {D : ℝ} {input : List ι} (h : Admissible upper b D input) (i : ℕ) : 0 ≤ (List.map b (List.take i input)).prod

theorem MathlibNt.SieveTheory.LiLiuPrereqWFAdmissibility.Admissible.prefix_square_lt {ι : Type u_1} {upper : Bool} {b : ι → ℝ} {D : ℝ} {input : List ι} (h : Admissible upper b D input) (i : ℕ) (hi : i < input.length) : (List.map b (List.take i input)).prod * b input[i] ^ 2 < D

Every indexed prefix satisfies the strict square budget on the lower endpoints. At a cubic index use bᵢ ≥ 1; at the following index use bᵢ ≤ bᵢ₋₁. The lower side's initial index uses the separate head bound.

theorem MathlibNt.SieveTheory.LiLiuPrereqWFAdmissibility.Admissible.prefixSquareBound {ι : Type u_1} {upper : Bool} {b : ι → ℝ} {D : ℝ} {input : List ι} (h : Admissible upper b D input) : LiLiuPrereqWFBoxAllocation.PrefixSquareBound b D input

Numerical admissibility supplies the existing allocation module's budget, without assuming any prefix-square or allocation statement.

theorem MathlibNt.SieveTheory.LiLiuPrereqWFAdmissibility.Admissible.exists_boxPartition {ι : Type u_1} {upper : Bool} {b : ι → ℝ} {D : ℝ} {input : List ι} (h : Admissible upper b D input) {M N : ℝ} (hM : 1 ≤ M) (hN : 1 ≤ N) (hMN : M * N = D) : ∃ (left : List ι) (right : List ι), LiLiuPrereqWFBoxAllocation.BoxPartition left right input ∧ (List.map b left).prod ≤ M ∧ (List.map b right).prod ≤ N

Allocate every labeled occurrence to exactly one box for any factorization of the level. Products are of the lower endpoints b, not upper endpoints.

theorem MathlibNt.SieveTheory.LiLiuPrereqWFAdmissibility.Admissible.exists_boxPartition_with_properties {ι : Type u_1} {upper : Bool} {b : ι → ℝ} {D : ℝ} {input : List ι} (h : Admissible upper b D input) {M N : ℝ} (hM : 1 ≤ M) (hN : 1 ≤ N) (hMN : M * N = D) : ∃ (left : List ι) (right : List ι), LiLiuPrereqWFBoxAllocation.BoxPartition left right input ∧ left.Sublist input ∧ right.Sublist input ∧ (left ++ right).Perm input ∧ (List.map b left).prod * (List.map b right).prod = (List.map b input).prod ∧ (List.map b left).prod ≤ M ∧ (List.map b right).prod ≤ N

Expanded allocation interface, including subsequence, permutation, and product identities; repeated labels remain distinct occurrences.