The genuine density sieve for the actual small-prime family

This specializes the checked finite construction to geometricSmallPrimes. Only densities below the actual cutoff are constrained. The product bound is first truncated at that cutoff and then transported through zero deletion. No moving-range or analytic estimate is used here.

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.smallDensityBoundingSieve (P : Finset ℕ) (D ε : ℝ) (g : ArithmeticFunction ℝ) (hgm : g.IsMultiplicative) (hg : ∀ p ∈ geometricSmallPrimes P D ε, 0 ≤ g p ∧ g p < 1) : BoundingSieve

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.smallDensityBoundingSieve P D ε g hgm hg = MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.densityBoundingSieve (MathlibNt.SieveTheory.LiLiuPrereqWF.geometricSmallPrimes P D ε) ⋯ g hgm hg

@[simp]

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.smallDensityBoundingSieve_nu (P : Finset ℕ) (D ε : ℝ) (g : ArithmeticFunction ℝ) (hgm : g.IsMultiplicative) (hg : ∀ p ∈ geometricSmallPrimes P D ε, 0 ≤ g p ∧ g p < 1) : (smallDensityBoundingSieve P D ε g hgm hg).nu = g

@[simp]

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.smallDensityBoundingSieve_primeFactors (P : Finset ℕ) (D ε : ℝ) (g : ArithmeticFunction ℝ) (hgm : g.IsMultiplicative) (hg : ∀ p ∈ geometricSmallPrimes P D ε, 0 ≤ g p ∧ g p < 1) : (smallDensityBoundingSieve P D ε g hgm hg).prodPrimes.primeFactors = nonzeroDensityPrimes (geometricSmallPrimes P D ε) ⇑g

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.smallDensityBoundingSieve_cutoffs (P : Finset ℕ) (D ε : ℝ) (g : ArithmeticFunction ℝ) (hgm : g.IsMultiplicative) (hg : ∀ p ∈ geometricSmallPrimes P D ε, 0 ≤ g p ∧ g p < 1) (hD : 2 ≤ D) (hε : 0 < ε) (hε1 : ε ≤ 1) : 2 ≤ ⌈D ^ ε ^ 2⌉₊ ∧ ⌈D ^ ε ^ 2⌉₊ ≤ ⌈D ^ ε⌉₊ ∧ ∀ p ∈ (smallDensityBoundingSieve P D ε g hgm hg).prodPrimes.primeFactors, p < ⌈D ^ ε⌉₊ ∧ p < ⌈D ^ ε ^ 2⌉₊

These are the exact cutoff and level hypotheses of the finite producers.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.smallDensityBoundingSieve_rounded_carrier (P : Finset ℕ) (D ε : ℝ) (g : ArithmeticFunction ℝ) (hgm : g.IsMultiplicative) (hg : ∀ p ∈ geometricSmallPrimes P D ε, 0 ≤ g p ∧ g p < 1) (hD : 2 ≤ D) (hε : 0 < ε) : {p ∈ (smallDensityBoundingSieve P D ε g hgm hg).prodPrimes.primeFactors | p < ⌈↑⌈D ^ ε⌉₊ ^ (1 / roundedSieveCoordinate (D ^ ε) (D ^ ε ^ 2))⌉₊} = nonzeroDensityPrimes (geometricSmallPrimes P D ε) ⇑g

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.smallDensityBoundingSieve_mainSums (P : Finset ℕ) (D ε : ℝ) (g : ArithmeticFunction ℝ) (hgm : g.IsMultiplicative) (hg : ∀ p ∈ geometricSmallPrimes P D ε, 0 ≤ g p ∧ g p < 1) : have B := geometricSmallPrimes P D ε; have S := smallDensityBoundingSieve P D ε g hgm hg; BoundingSieve.mainSum ⇑(lowerWeight S.prodPrimes ↑⌈D ^ ε⌉₊) = ∑ d ∈ (B.prod id).divisors, (lowerSmallWeight P D ε) d * g d ∧ BoundingSieve.mainSum ⇑(upperWeight S.prodPrimes ↑⌈D ^ ε⌉₊) = ∑ d ∈ (B.prod id).divisors, (upperSmallWeight P D ε) d * g d

Both main sums are the densities of the original named small weights, not of a substituted family. This identity imposes no sign restriction on D or ε; the support is the actual finite set in their definitions.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.smallDensityBoundingSieve_mainSums_eq_fullDefects (P : Finset ℕ) (D ε : ℝ) (g : ArithmeticFunction ℝ) (hgm : g.IsMultiplicative) (hg : ∀ p ∈ geometricSmallPrimes P D ε, 0 ≤ g p ∧ g p < 1) (hD : 2 ≤ D) (hε : 0 < ε) (hε1 : ε ≤ 1) : have B := geometricSmallPrimes P D ε; have S := smallDensityBoundingSieve P D ε g hgm hg; BoundingSieve.mainSum ⇑(lowerWeight S.prodPrimes ↑⌈D ^ ε⌉₊) = ∏ p ∈ B, (1 - g p) - lowerDensityDefect (D ^ ε) (⇑g) (B.sort fun (x1 x2 : ℕ) => x1 ≤ x2) ∧ BoundingSieve.mainSum ⇑(upperWeight S.prodPrimes ↑⌈D ^ ε⌉₊) = ∏ p ∈ B, (1 - g p) + upperDensityDefect (D ^ ε) (⇑g) (B.sort fun (x1 x2 : ℕ) => x1 ≤ x2)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.smallDensityBoundingSieve_localProduct (P : Finset ℕ) (D ε : ℝ) (g : ArithmeticFunction ℝ) (hgm : g.IsMultiplicative) (hg : ∀ p ∈ geometricSmallPrimes P D ε, 0 ≤ g p ∧ g p < 1) {K : ℝ} (hK : 0 ≤ K) (hdim : DimensionOneProductBound P (⇑g) K) : have S := smallDensityBoundingSieve P D ε g hgm hg; ∀ (w z : ℝ), 2 ≤ w → w ≤ z → ∏ p ∈ S.prodPrimes.primeFactors with w ≤ ↑p ∧ ↑p < z, (1 - S.nu p)⁻¹ ≤ Real.log z / Real.log w * (1 + K / Real.log w)

The exact expanded producer product hypothesis, with the same K and the non-strict diagonal case included. No conditions on g above D^(ε²) are added by restricting the carrier.