Real endpoint dilation and the small-weight support budget

Iwaniec's lower endpoints are dilated by b ↦ b^(1+θ). Raising the prefix-square inequalities to this power gives a budget D^(1+θ) for the actual prime upper endpoints. A fixed small-prime weight at level D^ε can then be placed in the larger factor for every split of the single, fixed external level D^(1+ε+θ).

The small weight is an actual supplied arithmetic function, not a sieve conclusion record. This module does not construct the Rosser small weight or assert its sieve direction or density.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.prefixSquareBound_rpow {ι : Type u_1} (input : List ι) (b : ι → ℝ) {D t : ℝ} (hb : ∀ i ∈ input, 0 ≤ b i) (ht : 0 ≤ t) (hprefix : LiLiuPrereqWFBoxAllocation.PrefixSquareBound b D input) : LiLiuPrereqWFBoxAllocation.PrefixSquareBound (fun (i : ι) => b i ^ t) (D ^ t) input

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.admissible_dilated_prefix {ι : Type u_1} {upper : Bool} {input : List ι} {b : ι → ℝ} {D θ : ℝ} (h : LiLiuPrereqWFAdmissibility.Admissible upper b D input) (hθ : 0 ≤ θ) : LiLiuPrereqWFBoxAllocation.PrefixSquareBound (fun (i : ι) => b i ^ (1 + θ)) (D ^ (1 + θ)) input

Both source parities give the support budget after actual endpoint dilation.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.list_smallWeight_boxProduct_factors {ι : Type u_1} [DecidableEq ι] (input : List ι) (B : ι → Finset ℕ) (U : ι → ℝ) (B₀ : Finset ℕ) (ψ : ArithmeticFunction ℝ) {S M N : ℝ} (hS : 0 ≤ S) (hM : 1 ≤ M) (hN : 1 ≤ N) (hU : ∀ i ∈ input.toFinset, 0 ≤ U i) (hB : ∀ i ∈ input.toFinset, ∀ p ∈ B i, Nat.Prime p → ↑p ≤ U i) (hdisj : ∀ ⦃i : ι⦄, i ∈ input.toFinset → ∀ ⦃j : ι⦄, j ∈ input.toFinset → i ≠ j → Disjoint (B i) (B j)) (hsep : Disjoint B₀ (input.toFinset.biUnion B)) (hψ : PrimeSupported B₀ ψ) (hψb : BoundedOne ψ) (hψs : SupportedAt ψ S) (hprefix : LiLiuPrereqWFBoxAllocation.PrefixSquareBound U (M * N) input) : ∃ (f : ArithmeticFunction ℝ) (g : ArithmeticFunction ℝ), BoundedOne f ∧ SupportedAt f (S * M) ∧ BoundedOne g ∧ SupportedAt g N ∧ (ψ * boxProduct input.toFinset B fun (a : ι) => List.count a input) = f * g

Occurrence allocation with the entire fixed small-prime function on the left. The two support levels are S*M and N, with no discarded terms.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.small_level_le_large_factor {S T A B : ℝ} (hS : 1 ≤ S) (hST : S ≤ T) (hA : 1 ≤ A) (hBA : B ≤ A) (hsplit : A * B = S * T) : S ≤ A

If S ≤ T, the larger factor of S*T always has room for level S.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.list_smallWeight_boxProduct_wellFactorable {ι : Type u_1} [DecidableEq ι] (input : List ι) (B : ι → Finset ℕ) (U : ι → ℝ) (B₀ : Finset ℕ) (ψ : ArithmeticFunction ℝ) {S T : ℝ} (hS : 1 ≤ S) (hST : S ≤ T) (hU : ∀ i ∈ input.toFinset, 0 ≤ U i) (hB : ∀ i ∈ input.toFinset, ∀ p ∈ B i, Nat.Prime p → ↑p ≤ U i) (hdisj : ∀ ⦃i : ι⦄, i ∈ input.toFinset → ∀ ⦃j : ι⦄, j ∈ input.toFinset → i ≠ j → Disjoint (B i) (B j)) (hsep : Disjoint B₀ (input.toFinset.biUnion B)) (hψ : PrimeSupported B₀ ψ) (hψb : BoundedOne ψ) (hψs : SupportedAt ψ S) (hprefix : LiLiuPrereqWFBoxAllocation.PrefixSquareBound U T input) : WellFactorable (ψ * boxProduct input.toFinset B fun (a : ι) => List.count a input) (S * T)

A supplied bounded, separated small-prime function is incorporated before all splits. The hypothesis is a numerical endpoint budget, not WF of a weight.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.admissible_smallWeight_wellFactorable {ι : Type u_1} [DecidableEq ι] {upper : Bool} (input : List ι) (B : ι → Finset ℕ) (b : ι → ℝ) (B₀ : Finset ℕ) (ψ : ArithmeticFunction ℝ) {D ε θ : ℝ} (hD : 1 ≤ D) (hε : 0 ≤ ε) (hθ : 0 ≤ θ) (hεθ : ε ≤ 1 + θ) (hadm : LiLiuPrereqWFAdmissibility.Admissible upper b D input) (hB : ∀ i ∈ input.toFinset, ∀ p ∈ B i, Nat.Prime p → ↑p ≤ b i ^ (1 + θ)) (hdisj : ∀ ⦃i : ι⦄, i ∈ input.toFinset → ∀ ⦃j : ι⦄, j ∈ input.toFinset → i ≠ j → Disjoint (B i) (B j)) (hsep : Disjoint B₀ (input.toFinset.biUnion B)) (hψ : PrimeSupported B₀ ψ) (hψb : BoundedOne ψ) (hψs : SupportedAt ψ (D ^ ε)) : WellFactorable (ψ * boxProduct input.toFinset B fun (a : ι) => List.count a input) (D ^ (1 + ε + θ))

The fixed internal level D, the side, boxes and small weight all precede the quantifier over external splits in WellFactorable. This is the real support bridge in I80 p.312, without any split-dependent internal parameter.