A genuine density sieve on the zero-deleted small-prime carrier

The counting data are empty: this object is used only for its actual BoundingSieve.nu, prime carrier, and mainSum. Its density function is the original multiplicative function, not a new density chosen to fit a conclusion. Deleting its zero primes preserves both entire signed Rosser densities and the Euler product, including when the surviving carrier is empty.

No unadmitted producer module is imported here.

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.densityBoundingSieve (B : Finset ℕ) (hB : ∀ p ∈ B, Nat.Prime p) (g : ArithmeticFunction ℝ) (hgm : g.IsMultiplicative) (hg : ∀ p ∈ B, 0 ≤ g p ∧ g p < 1) : BoundingSieve

The analytic sieve with the original density and exactly its nonzero primes in B. The empty counting support imposes no extra hypothesis on g.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.densityBoundingSieve B hB g hgm hg = { support := ∅, prodPrimes := (MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.nonzeroDensityPrimes B ⇑g).prod id, prodPrimes_squarefree := ⋯, weights := fun (x : ℕ) => 0, weights_nonneg := MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.densityBoundingSieve._proof_2, totalMass := 0, nu := g, nu_mult := hgm, nu_pos_of_prime := ⋯, nu_lt_one_of_prime := ⋯ }

@[simp]

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.densityBoundingSieve_nu (B : Finset ℕ) (hB : ∀ p ∈ B, Nat.Prime p) (g : ArithmeticFunction ℝ) (hgm : g.IsMultiplicative) (hg : ∀ p ∈ B, 0 ≤ g p ∧ g p < 1) : (densityBoundingSieve B hB g hgm hg).nu = g

@[simp]

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.densityBoundingSieve_primeFactors (B : Finset ℕ) (hB : ∀ p ∈ B, Nat.Prime p) (g : ArithmeticFunction ℝ) (hgm : g.IsMultiplicative) (hg : ∀ p ∈ B, 0 ≤ g p ∧ g p < 1) : (densityBoundingSieve B hB g hgm hg).prodPrimes.primeFactors = nonzeroDensityPrimes B ⇑g

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.densityBoundingSieve_mem_primeFactors (B : Finset ℕ) (hB : ∀ p ∈ B, Nat.Prime p) (g : ArithmeticFunction ℝ) (hgm : g.IsMultiplicative) (hg : ∀ p ∈ B, 0 ≤ g p ∧ g p < 1) (p : ℕ) : p ∈ (densityBoundingSieve B hB g hgm hg).prodPrimes.primeFactors ↔ p ∈ B ∧ g p ≠ 0

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.densityBoundingSieve_prime_lt_ceil (B : Finset ℕ) (hB : ∀ p ∈ B, Nat.Prime p) (g : ArithmeticFunction ℝ) (hgm : g.IsMultiplicative) (hg : ∀ p ∈ B, 0 ≤ g p ∧ g p < 1) {u : ℝ} (hcut : ∀ p ∈ B, ↑p < u) (p : ℕ) : p ∈ (densityBoundingSieve B hB g hgm hg).prodPrimes.primeFactors → p < ⌈u⌉₊

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.densityBoundingSieve_rounded_carrier (B : Finset ℕ) (hB : ∀ p ∈ B, Nat.Prime p) (g : ArithmeticFunction ℝ) (hgm : g.IsMultiplicative) (hg : ∀ p ∈ B, 0 ≤ g p ∧ g p < 1) {L u : ℝ} (hL : 1 < L) (hu : 1 < u) (hcut : ∀ p ∈ B, ↑p < u) : {p ∈ (densityBoundingSieve B hB g hgm hg).prodPrimes.primeFactors | p < ⌈↑⌈L⌉₊ ^ (1 / roundedSieveCoordinate L u)⌉₊} = nonzeroDensityPrimes B ⇑g

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.densityBoundingSieve_euler (B : Finset ℕ) (hB : ∀ p ∈ B, Nat.Prime p) (g : ArithmeticFunction ℝ) (hgm : g.IsMultiplicative) (hg : ∀ p ∈ B, 0 ≤ g p ∧ g p < 1) : ∏ p ∈ (densityBoundingSieve B hB g hgm hg).prodPrimes.primeFactors, (1 - (densityBoundingSieve B hB g hgm hg).nu p) = ∏ p ∈ B, (1 - g p)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.densityBoundingSieve_mainSums (B : Finset ℕ) (hB : ∀ p ∈ B, Nat.Prime p) (g : ArithmeticFunction ℝ) (hgm : g.IsMultiplicative) (hg : ∀ p ∈ B, 0 ≤ g p ∧ g p < 1) (L : ℝ) : have S := densityBoundingSieve B hB g hgm hg; BoundingSieve.mainSum ⇑(lowerWeight S.prodPrimes ↑⌈L⌉₊) = ∑ d ∈ (B.prod id).divisors, (lowerWeight (B.prod id) L) d * g d ∧ BoundingSieve.mainSum ⇑(upperWeight S.prodPrimes ↑⌈L⌉₊) = ∑ d ∈ (B.prod id).divisors, (upperWeight (B.prod id) L) d * g d

The level and the carrier are both changed, but the entire signed density of each of the original weights is preserved exactly.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.densityBoundingSieve_mainSums_eq_setDensities (B : Finset ℕ) (hB : ∀ p ∈ B, Nat.Prime p) (g : ArithmeticFunction ℝ) (hgm : g.IsMultiplicative) (hg : ∀ p ∈ B, 0 ≤ g p ∧ g p < 1) (L : ℝ) : have S := densityBoundingSieve B hB g hgm hg; BoundingSieve.mainSum ⇑(lowerWeight S.prodPrimes ↑⌈L⌉₊) = lowerSetDensity L (⇑g) B ∧ BoundingSieve.mainSum ⇑(upperWeight S.prodPrimes ↑⌈L⌉₊) = upperSetDensity L (⇑g) B

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.densityBoundingSieve_mainSums_eq_fullDefects (B : Finset ℕ) (hB : ∀ p ∈ B, Nat.Prime p) (g : ArithmeticFunction ℝ) (hgm : g.IsMultiplicative) (hg : ∀ p ∈ B, 0 ≤ g p ∧ g p < 1) {L : ℝ} (hL : 1 < L) (hcut : ∀ p ∈ B, ↑p < L) : have S := densityBoundingSieve B hB g hgm hg; BoundingSieve.mainSum ⇑(lowerWeight S.prodPrimes ↑⌈L⌉₊) = ∏ p ∈ B, (1 - g p) - lowerDensityDefect L (⇑g) (B.sort fun (x1 x2 : ℕ) => x1 ≤ x2) ∧ BoundingSieve.mainSum ⇑(upperWeight S.prodPrimes ↑⌈L⌉₊) = ∏ p ∈ B, (1 - g p) + upperDensityDefect L (⇑g) (B.sort fun (x1 x2 : ℕ) => x1 ≤ x2)

The lower sign remains minus; the upper sign remains plus. These are the whole original defects, not only a truncation or high-minimum part.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.densityBoundingSieve_dimensionOne (B : Finset ℕ) (hB : ∀ p ∈ B, Nat.Prime p) (g : ArithmeticFunction ℝ) (hgm : g.IsMultiplicative) (hg : ∀ p ∈ B, 0 ≤ g p ∧ g p < 1) {K : ℝ} (hdim : DimensionOneProductBound B (⇑g) K) : DimensionOneProductBound (densityBoundingSieve B hB g hgm hg).prodPrimes.primeFactors (⇑(densityBoundingSieve B hB g hgm hg).nu) K

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.densityBoundingSieve_localProduct (B : Finset ℕ) (hB : ∀ p ∈ B, Nat.Prime p) (g : ArithmeticFunction ℝ) (hgm : g.IsMultiplicative) (hg : ∀ p ∈ B, 0 ≤ g p ∧ g p < 1) {K : ℝ} (hK : 0 ≤ K) (hdim : DimensionOneProductBound B (⇑g) K) : have S := densityBoundingSieve B hB 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 producer's product formula has w ≤ z, unlike the local strict interval convention. The extra diagonal case requires only K ≥ 0.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.densityBoundingSieve_empty_carrier (B : Finset ℕ) (hB : ∀ p ∈ B, Nat.Prime p) (g : ArithmeticFunction ℝ) (hgm : g.IsMultiplicative) (hg : ∀ p ∈ B, 0 ≤ g p ∧ g p < 1) (hz : ∀ p ∈ B, g p = 0) : (densityBoundingSieve B hB g hgm hg).prodPrimes = 1