Euler-normalized analytic scale for the actual boundary mass

The constant is absolute, and the original dimension-one constant is retained in exp (6*K+2). No threshold is allowed to depend on K.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.BoundaryAnalytic.boundary_scalar {ε L K : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hL : 0 < L) (hK : 0 ≤ K) (ht : 1 ≤ ε ^ 2 * L) : 2 * ((1 + K / (ε ^ 2 * L)) / ε ^ 2) ^ 3 * (3 * ε ^ 7 + 2 * K / (ε ^ 2 * L)) ≤ 10 * (ε + (ε ^ 8)⁻¹ * Real.exp (6 * K + 2) * L ^ (-(1 / 3)))

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.BoundaryAnalytic.roughPlusProduct_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) (hcut : ∀ p ∈ P \ geometricSmallPrimes P D ε, ↑p < √D) {g : ℕ → ℝ} (hg : ∀ p ∈ P, 0 ≤ g p ∧ g p < 1) (hdim : SmallRosser.DimensionOneProductBound P g K) : ∏ p ∈ P \ geometricSmallPrimes P D ε, (1 + g p) ≤ (1 + K / (ε ^ 2 * Real.log D)) / ε ^ 2

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.BoundaryAnalytic.roughPlusProduct_square_le_normalized (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) (hcut : ∀ p ∈ P \ geometricSmallPrimes P D ε, ↑p < √D) {g : ℕ → ℝ} (hg : ∀ p ∈ P, 0 ≤ g p ∧ g p < 1) (hdim : SmallRosser.DimensionOneProductBound P g K) : (∏ p ∈ P \ geometricSmallPrimes P D ε, (1 + g p)) ^ 2 ≤ (∏ p ∈ P \ geometricSmallPrimes P D ε, (1 - g p)) * ((1 + K / (ε ^ 2 * Real.log D)) / ε ^ 2) ^ 3

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.BoundaryAnalytic.roughBoundaryMass_le_target (upper : Bool) (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); roughBoundaryMass upper b (fun (p : ℕ) => b p ^ (1 + ε ^ 9)) D R g ≤ (10 * ∏ p ∈ R, (1 - g p)) * (ε + (ε ^ 8)⁻¹ * Real.exp (6 * K + 2) * Real.log D ^ (-(1 / 3)))

The actual geometric rough boundary mass on the required normalized scale, with absolute constant 10 and exactly the original K.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.BoundaryAnalytic.exists_roughBoundaryMass_le_target : ∃ (C : ℝ), 0 < C ∧ ∀ (ε : ℝ), 0 < ε → ε < 1 / 8 → ∃ (D₀ : ℝ), 2 ≤ D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → ∀ (P : Finset ℕ), (∀ p ∈ P, Nat.Prime p) → (∀ p ∈ P \ geometricSmallPrimes P D ε, ↑p < √D) → ∀ (g : ℕ → ℝ), (∀ p ∈ P, 0 ≤ g p ∧ g p < 1) → ∀ (K : ℝ), 0 ≤ K → SmallRosser.DimensionOneProductBound P g K → ∀ (upper : Bool), have R := P \ geometricSmallPrimes P D ε; have b := fun (p : ℕ) => geometricLower D ε (ε ^ 9) (geometricSieveLabel D ε p); roughBoundaryMass upper b (fun (p : ℕ) => b p ^ (1 + ε ^ 9)) D R g ≤ (C * ∏ p ∈ R, (1 - g p)) * (ε + (ε ^ 8)⁻¹ * Real.exp (6 * K + 2) * Real.log D ^ (-(1 / 3)))

The uniform threshold precedes the carrier, density and K.