Large-D fundamental-lemma density of the original small weights

The actual JR/Suzuki estimate controls the entire defects, including their low-prime contributions. An absolute constant is selected before ε; the explicit threshold is selected before all sieve data, K, and depths. This proves the large-D form of Iwaniec p.316 (22), not the density of the as-yet unassembled full signed box family.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.exists_smallDensityDefects_fundamental_bound : ∃ (C : ℝ), 0 < C ∧ ∀ (ε : ℝ), 0 < ε → ε < 1 / 8 → ∃ (D₀ : ℝ), 2 ≤ D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → ∀ (P : Finset ℕ) (g : ArithmeticFunction ℝ), g.IsMultiplicative → (∀ p ∈ geometricSmallPrimes P D ε, 0 ≤ g p ∧ g p < 1) → ∀ (K : ℝ), 0 ≤ K → DimensionOneProductBound P (⇑g) K → have B := geometricSmallPrimes P D ε; have E := C * (Real.exp (-(1 / ε)) + Real.exp (√K - 1 / ε) * (ε * Real.log D) ^ (-(1 / 3))); lowerDensityDefect (D ^ ε) (⇑g) (B.sort fun (x1 x2 : ℕ) => x1 ≤ x2) ≤ (∏ p ∈ B, (1 - g p)) * E ∧ upperDensityDefect (D ^ ε) (⇑g) (B.sort fun (x1 x2 : ℕ) => x1 ≤ x2) ≤ (∏ p ∈ B, (1 - g p)) * E

The full original defects, with an absolute constant selected before ε, and a threshold selected before the carrier, density, and K.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.exists_smallWeight_source_fundamental_density : ∃ (C : ℝ), 0 < C ∧ ∀ (ε : ℝ), 0 < ε → ε < 1 / 8 → ∃ (D₀ : ℝ), 2 ≤ D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → ∀ (P : Finset ℕ) (ω : ArithmeticFunction ℝ), ω.IsMultiplicative → (∀ p ∈ geometricSmallPrimes P D ε, 0 ≤ ω p / ↑p ∧ ω p / ↑p < 1) → ∀ (K : ℝ), 0 ≤ K → DimensionOneProductBound P (⇑(primeDensity ω)) K → have B := geometricSmallPrimes P D ε; have V := ∏ p ∈ B, (1 - ω p / ↑p); have E := C * (Real.exp (-(1 / ε)) + Real.exp (√K - 1 / ε) * (ε * Real.log D) ^ (-(1 / 3))); |∑ d ∈ (B.prod id).divisors, (lowerSmallWeight P D ε) d * (ω d / ↑d) - V| ≤ V * E ∧ |∑ d ∈ (B.prod id).divisors, (upperSmallWeight P D ε) d * (ω d / ↑d) - V| ≤ V * E

The large-D form of Iwaniec p.316 (22), in the literal ω(d)/d convention and for the already constructed small weights.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.exists_smallWeight_source_density_sandwich : ∃ (C : ℝ), 0 < C ∧ ∀ (ε : ℝ), 0 < ε → ε < 1 / 8 → ∃ (D₀ : ℝ), 2 ≤ D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → ∀ (P : Finset ℕ) (ω : ArithmeticFunction ℝ), ω.IsMultiplicative → (∀ p ∈ geometricSmallPrimes P D ε, 0 ≤ ω p / ↑p ∧ ω p / ↑p < 1) → ∀ (K : ℝ), 0 ≤ K → DimensionOneProductBound P (⇑(primeDensity ω)) K → have B := geometricSmallPrimes P D ε; have V := ∏ p ∈ B, (1 - ω p / ↑p); have E := C * (Real.exp (-(1 / ε)) + Real.exp (√K - 1 / ε) * (ε * Real.log D) ^ (-(1 / 3))); have lo := ∑ d ∈ (B.prod id).divisors, (lowerSmallWeight P D ε) d * (ω d / ↑d); have hi := ∑ d ∈ (B.prod id).divisors, (upperSmallWeight P D ε) d * (ω d / ↑d); V * (1 - E) ≤ lo ∧ lo ≤ V ∧ V ≤ hi ∧ hi ≤ V * (1 + E) ∧ hi - lo ≤ 2 * V * E

Signed small-weight bounds and the exact cost needed when replacing the lower small-weight density by the upper one. This does not perform that replacement inside an unproved full box-family identity.