Analytic control of the actual same-box collisions

The original dimension-one product hypothesis controls each geometric interval, including its closed lower and strict upper endpoint. Summing over the actual distinct prime pairs retains the rough Euler normalization. No count of prime subsets or bound on a different family is used.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.CollisionAnalytic.sum_le_inverseProduct_sub_one (S : Finset ℕ) (g : ℕ → ℝ) (hg : ∀ p ∈ S, 0 ≤ g p ∧ g p < 1) : ∑ p ∈ S, g p ≤ ∏ p ∈ S, (1 - g p)⁻¹ - 1

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.CollisionAnalytic.interval_sum_le (P S : Finset ℕ) {g : ℕ → ℝ} {K w z : ℝ} (hg : ∀ p ∈ P, 0 ≤ g p ∧ g p < 1) (hdim : SmallRosser.DimensionOneProductBound P g K) (hw : 2 ≤ w) (hwz : w < z) (hS : S ⊆ {p ∈ P | Nat.Prime p ∧ w ≤ ↑p ∧ ↑p < z}) : ∑ p ∈ S, g p ≤ Real.log z / Real.log w * (1 + K / Real.log w) - 1

The interval product hypothesis pays an actual subinterval prime sum. The -1 is essential to keep the geometric width small.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.CollisionAnalytic.rough_parameters {D ε : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) (hlarge : 1 ≤ ε ^ 2 * Real.log D) : 2 ≤ D ^ ε ^ 2 ∧ D ^ ε ^ 2 < D ∧ 0 < Real.log D ∧ Real.log (D ^ ε ^ 2) = ε ^ 2 * Real.log D

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.CollisionAnalytic.rough_prime_lower (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) (D ε : ℝ) {p : ℕ} (hp : p ∈ P \ geometricSmallPrimes P D ε) : D ^ ε ^ 2 ≤ ↑p

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.CollisionAnalytic.sameBox_partner_sum_le (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) {D ε K : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) (hlarge : 1 ≤ ε ^ 2 * Real.log D) (hK : 0 ≤ K) {g : ℕ → ℝ} (hg : ∀ p ∈ P, 0 ≤ g p ∧ g p < 1) (hdim : SmallRosser.DimensionOneProductBound P g K) {p : ℕ} (hp : p ∈ P \ geometricSmallPrimes P D ε) : have R := P \ geometricSmallPrimes P D ε; have b := fun (q : ℕ) => geometricLower D ε (ε ^ 9) (geometricSieveLabel D ε q); ∑ q ∈ R with p < q ∧ b p = b q, g q ≤ ε ^ 9 + 2 * K / (ε ^ 2 * Real.log D)

No geometric-grid cardinality is needed: the distinct later partners of p lie in [p,p^(1+epsilon^9)).

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.CollisionAnalytic.roughCollisionPairMass_le_dimensionOne (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) {D ε K : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) (hlarge : 1 ≤ ε ^ 2 * Real.log D) (hK : 0 ≤ K) (hcut : ∀ p ∈ P \ geometricSmallPrimes P D ε, ↑p < √D) {g : ℕ → ℝ} (hg : ∀ p ∈ P, 0 ≤ g p ∧ g p < 1) (hdim : SmallRosser.DimensionOneProductBound P g K) : have R := P \ geometricSmallPrimes P D ε; have b := fun (p : ℕ) => geometricLower D ε (ε ^ 9) (geometricSieveLabel D ε p); roughCollisionPairMass b R g ≤ (ε ^ 9 + 2 * K / (ε ^ 2 * Real.log D)) * ((1 + K / (ε ^ 2 * Real.log D)) / ε ^ 2)

A same-carrier pair bound from the original product hypothesis.