Normalized exponential bounds on intervals of small primes

The weights and cubic boundary kernels are the ones already constructed. An exponential tilt bounds the kernels, and an Euler-product majorant retains the normalization needed by the dimension-one hypothesis. The resulting estimate is useful on w ≤ p < u when log u / log w is bounded. It does not control the remaining small-minimum boundaries.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerBoundaryDensity_le_tilt (P : Finset ℕ) {D ε : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) {g : ℕ → ℝ} {q : ℕ} {B : Finset ℕ} (hq : q ∈ geometricSmallPrimes P D ε) (hB : B ⊆ geometricSmallPrimes P D ε) (hg : ∀ p ∈ B, 0 ≤ g p) : lowerBoundaryDensity (D ^ ε) g q B ≤ Real.exp (3 - 1 / ε) * ∏ p ∈ B, (1 + 3 * g p)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperBoundaryDensity_le_tilt (P : Finset ℕ) {D ε : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) {g : ℕ → ℝ} {q : ℕ} {B : Finset ℕ} (hq : q ∈ geometricSmallPrimes P D ε) (hB : B ⊆ geometricSmallPrimes P D ε) (hg : ∀ p ∈ B, 0 ≤ g p) : upperBoundaryDensity (D ^ ε) g q B ≤ Real.exp (3 - 1 / ε) * ∏ p ∈ B, (1 + 3 * g p)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerDensityDefect_le_tilt (P : Finset ℕ) {D ε : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) {g : ℕ → ℝ} (ps : List ℕ) (hnd : ps.Nodup) (hps : ∀ p ∈ ps, p ∈ geometricSmallPrimes P D ε) (hg : ∀ p ∈ ps, 0 ≤ g p ∧ g p ≤ 1) : lowerDensityDefect (D ^ ε) g ps ≤ Real.exp (3 - 1 / ε) / 4 * (∏ p ∈ ps.toFinset, (1 + 3 * g p) - ∏ p ∈ ps.toFinset, (1 - g p))

The factor 1/4 is the exact telescoping coefficient for the tilt 3.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperDensityDefect_le_tilt (P : Finset ℕ) {D ε : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) {g : ℕ → ℝ} (ps : List ℕ) (hnd : ps.Nodup) (hps : ∀ p ∈ ps, p ∈ geometricSmallPrimes P D ε) (hg : ∀ p ∈ ps, 0 ≤ g p ∧ g p ≤ 1) : upperDensityDefect (D ^ ε) g ps ≤ Real.exp (3 - 1 / ε) / 4 * (∏ p ∈ ps.toFinset, (1 + 3 * g p) - ∏ p ∈ ps.toFinset, (1 - g p))

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.tiltedProduct_le_euler_mul_fourth {g : ℕ → ℝ} (B : Finset ℕ) {A : ℝ} (hg : ∀ p ∈ B, 0 ≤ g p ∧ g p < 1) (hA : (∏ p ∈ B, (1 - g p))⁻¹ ≤ A) : ∏ p ∈ B, (1 + 3 * g p) ≤ (∏ p ∈ B, (1 - g p)) * A ^ 4

A product estimate rather than an unnormalized prime-mass bound.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.smallDensityDefects_le_normalized_product (P : Finset ℕ) {D ε : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) {g : ℕ → ℝ} (ps : List ℕ) {A : ℝ} (hnd : ps.Nodup) (hps : ∀ p ∈ ps, p ∈ geometricSmallPrimes P D ε) (hg : ∀ p ∈ ps, 0 ≤ g p ∧ g p < 1) (hA : (∏ p ∈ ps.toFinset, (1 - g p))⁻¹ ≤ A) : lowerDensityDefect (D ^ ε) g ps ≤ (∏ p ∈ ps.toFinset, (1 - g p)) * (Real.exp (3 - 1 / ε) / 4 * (A ^ 4 - 1)) ∧ upperDensityDefect (D ^ ε) g ps ≤ (∏ p ∈ ps.toFinset, (1 - g p)) * (Real.exp (3 - 1 / ε) / 4 * (A ^ 4 - 1))

Both actual errors, divided by their own Euler product. No density estimate is an input; hA is an ordinary interval-product bound.

def MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.DimensionOneProductBound (P : Finset ℕ) (g : ℕ → ℝ) (K : ℝ) : Prop

The finite-carrier form of I80 (1), with the same constant K. The left endpoint is closed and the right endpoint is strict.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.DimensionOneProductBound P g K = ∀ (w z : ℝ), 2 ≤ w → w < z → ∏ p ∈ P with Nat.Prime p ∧ w ≤ ↑p ∧ ↑p < z, (1 - g p)⁻¹ ≤ Real.log z / Real.log w * (1 + K / Real.log w)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.dimensionOne_smallInterval_inverseProduct (P : Finset ℕ) {D ε w K : ℝ} {g : ℕ → ℝ} (hdim : DimensionOneProductBound P g K) (hw : 2 ≤ w) (hwu : w < D ^ ε ^ 2) : (∏ p ∈ geometricSmallPrimes P D ε with w ≤ ↑p, (1 - g p))⁻¹ ≤ Real.log (D ^ ε ^ 2) / Real.log w * (1 + K / Real.log w)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.smallIntervalDensityDefects_le_dimensionOne (P : Finset ℕ) {D ε w K : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) {g : ℕ → ℝ} (hg : ∀ p ∈ geometricSmallPrimes P D ε, 0 ≤ g p ∧ g p < 1) (hdim : DimensionOneProductBound P g K) (hw : 2 ≤ w) (hwu : w < D ^ ε ^ 2) : have B := {p ∈ geometricSmallPrimes P D ε | w ≤ ↑p}; have A := Real.log (D ^ ε ^ 2) / Real.log w * (1 + K / Real.log w); lowerDensityDefect (D ^ ε) g (B.sort fun (x1 x2 : ℕ) => x1 ≤ x2) ≤ (∏ p ∈ B, (1 - g p)) * (Real.exp (3 - 1 / ε) / 4 * (A ^ 4 - 1)) ∧ upperDensityDefect (D ^ ε) g (B.sort fun (x1 x2 : ℕ) => x1 ≤ x2) ≤ (∏ p ∈ B, (1 - g p)) * (Real.exp (3 - 1 / ε) / 4 * (A ^ 4 - 1))

An actual normalized analytic bound for both interval errors. For w = 2 its logarithmic factor grows with D; no full fundamental lemma is inferred from that specialization.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.smallIntervalDensityDefects_le_exp (P : Finset ℕ) {D ε w K : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) {g : ℕ → ℝ} (hg : ∀ p ∈ geometricSmallPrimes P D ε, 0 ≤ g p ∧ g p < 1) (hdim : DimensionOneProductBound P g K) (hw : 2 ≤ w) (hwu : w < D ^ ε ^ 2) (hK0 : 0 ≤ K) (hK : K ≤ Real.log w) (hratio : Real.log (D ^ ε ^ 2) ≤ 2 * Real.log w) : have B := {p ∈ geometricSmallPrimes P D ε | w ≤ ↑p}; lowerDensityDefect (D ^ ε) g (B.sort fun (x1 x2 : ℕ) => x1 ≤ x2) ≤ (∏ p ∈ B, (1 - g p)) * (255 / 4 * Real.exp 3 * Real.exp (-(1 / ε))) ∧ upperDensityDefect (D ^ ε) g (B.sort fun (x1 x2 : ℕ) => x1 ≤ x2) ≤ (∏ p ∈ B, (1 - g p)) * (255 / 4 * Real.exp 3 * Real.exp (-(1 / ε)))

Uniform exponential suppression on a logarithmically short interval. The explicit conditions retain the original K: they are satisfied by w = sqrt u once u ≥ 4 and log u ≥ 2 K.