Deleting zero-density primes without changing the actual density

The coefficients are unchanged on every surviving subset. Subsets containing a deleted prime have zero density, irrespective of their Rosser admissibility. In particular both entire defects, not merely their high-minimum parts, survive this reduction exactly.

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.nonzeroDensityPrimes (B : Finset ℕ) (g : ℕ → ℝ) : Finset ℕ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.nonzeroDensityPrimes B g = {p ∈ B | g p ≠ 0}

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.nonzeroDensityPrimes_subset (B : Finset ℕ) (g : ℕ → ℝ) : nonzeroDensityPrimes B g ⊆ B

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.nonzeroDensityPrimes_pos {B : Finset ℕ} {g : ℕ → ℝ} (hg : ∀ p ∈ B, 0 ≤ g p ∧ g p < 1) (p : ℕ) : p ∈ nonzeroDensityPrimes B g → 0 < g p ∧ g p < 1

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.density_product_zero_of_not_subset {B s : Finset ℕ} {g : ℕ → ℝ} (hs : s ⊆ B) (hn : ¬s ⊆ nonzeroDensityPrimes B g) : ∏ p ∈ s, g p = 0

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.subsetDensity_delete_zero (c : Finset ℕ → ℝ) (B : Finset ℕ) (g : ℕ → ℝ) : ∑ s ∈ (nonzeroDensityPrimes B g).powerset, c s * ∏ p ∈ s, g p = ∑ s ∈ B.powerset, c s * ∏ p ∈ s, g p

Valid for the actual signed coefficient, with no bound or sign assumption.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerSetDensity_delete_zero (L : ℝ) (B : Finset ℕ) (g : ℕ → ℝ) : lowerSetDensity L g (nonzeroDensityPrimes B g) = lowerSetDensity L g B

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSetDensity_delete_zero (L : ℝ) (B : Finset ℕ) (g : ℕ → ℝ) : upperSetDensity L g (nonzeroDensityPrimes B g) = upperSetDensity L g B

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.eulerProduct_delete_zero (B : Finset ℕ) (g : ℕ → ℝ) : ∏ p ∈ nonzeroDensityPrimes B g, (1 - g p) = ∏ p ∈ B, (1 - g p)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.dimensionOneProductBound_delete_zero {P : Finset ℕ} {g : ℕ → ℝ} {K : ℝ} (h : DimensionOneProductBound P g K) : DimensionOneProductBound (nonzeroDensityPrimes P g) g K

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.dimensionOneProductBound_truncate {P : Finset ℕ} {g : ℕ → ℝ} {K : ℝ} (h : DimensionOneProductBound P g K) (hK : 0 ≤ K) (u : ℝ) : DimensionOneProductBound ({p ∈ P | Nat.Prime p ∧ ↑p < u}) g K

Truncation at the actual cutoff uses the product hypothesis at min z u. No density assumption on primes above u is needed.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.densityDefects_delete_zero (B : Finset ℕ) {L : ℝ} (g : ℕ → ℝ) (hL : 1 < L) (hB : ∀ p ∈ B, Nat.Prime p) (hcut : ∀ p ∈ B, ↑p < L) : lowerDensityDefect L g ((nonzeroDensityPrimes B g).sort fun (x1 x2 : ℕ) => x1 ≤ x2) = lowerDensityDefect L g (B.sort fun (x1 x2 : ℕ) => x1 ≤ x2) ∧ upperDensityDefect L g ((nonzeroDensityPrimes B g).sort fun (x1 x2 : ℕ) => x1 ≤ x2) = upperDensityDefect L g (B.sort fun (x1 x2 : ℕ) => x1 ≤ x2)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.weightDensities_delete_zero (B : Finset ℕ) (L : ℝ) (hB : ∀ p ∈ B, Nat.Prime p) {g : ArithmeticFunction ℝ} (hg : g.IsMultiplicative) : ∑ d ∈ ((nonzeroDensityPrimes B ⇑g).prod id).divisors, (lowerWeight ((nonzeroDensityPrimes B ⇑g).prod id) L) d * g d = ∑ d ∈ (B.prod id).divisors, (lowerWeight (B.prod id) L) d * g d ∧ ∑ d ∈ ((nonzeroDensityPrimes B ⇑g).prod id).divisors, (upperWeight ((nonzeroDensityPrimes B ⇑g).prod id) L) d * g d = ∑ d ∈ (B.prod id).divisors, (upperWeight (B.prod id) L) d * g d

Exact density of the original divisor weights after deleting zero primes.