The original small weights and the admitted finite Suzuki producers

Strict real-level tests become tests at the natural ceiling. Deleting zero-density primes preserves the entire signed densities and the Euler product. The lower and upper defects are exactly the actual Suzuki sums at exhaustive even and odd depths, respectively.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerAdmissibleSet_iff_producer (L : ℝ) (s : Finset ℕ) : LowerAdmissibleSet L s ↔ LinearSieve.LowerRosserAdmissibleSet ⌈L⌉₊ s

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperAdmissibleSet_iff_producer (L : ℝ) (s : Finset ℕ) : UpperAdmissibleSet L s ↔ LinearSieve.UpperRosserAdmissibleSet ⌈L⌉₊ s

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.setWeight_eq_producer (L : ℝ) (s : Finset ℕ) : setWeight L s = LinearSieve.lowerRosserSetWeight ⌈L⌉₊ s

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSetWeight_eq_producer (L : ℝ) (s : Finset ℕ) : upperSetWeight L s = LinearSieve.upperRosserSetWeight ⌈L⌉₊ s

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerSetDensity_eq_producer (L : ℝ) (g : ℕ → ℝ) (B : Finset ℕ) : lowerSetDensity L g B = LinearSieve.lowerRosserSetDensitySum g ⌈L⌉₊ B

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSetDensity_eq_producer (L : ℝ) (g : ℕ → ℝ) (B : Finset ℕ) : upperSetDensity L g B = LinearSieve.upperRosserSetDensitySum g ⌈L⌉₊ B

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.densityBoundingSieve_actual_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 (LinearSieve.lowerRosserWeight S.prodPrimes ⌈L⌉₊) = lowerSetDensity L (⇑g) B ∧ BoundingSieve.mainSum (LinearSieve.upperRosserWeight S.prodPrimes ⌈L⌉₊) = upperSetDensity L (⇑g) B

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.densityBoundingSieve_supportedBelow (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) : SwitchingPrinciple.suzukiSupportedBelow (densityBoundingSieve B hB g hgm hg) ⌈u⌉₊ = nonzeroDensityPrimes B ⇑g

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.densityBoundingSieve_hasDimensionOneLocalProductBound (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) : SwitchingPrinciple.HasDimensionOneLocalProductBound (densityBoundingSieve B hB g hgm hg) K

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.densityBoundingSieve_suzukiVProduct (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) : SwitchingPrinciple.suzukiVProduct (densityBoundingSieve B hB g hgm hg) ↑⌈u⌉₊ = ∏ p ∈ B, (1 - g p)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.densityBoundingSieve_actual_densities (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) (huL : u ≤ L) (hcut : ∀ p ∈ B, ↑p < u) : have S := densityBoundingSieve B hB g hgm hg; have T := nonzeroDensityPrimes B ⇑g; lowerSetDensity L (⇑g) B = ∏ p ∈ B, (1 - g p) - suzukiActualT S (2 * (T.card + 1)) ⌈L⌉₊ ⌈u⌉₊ ∧ upperSetDensity L (⇑g) B = ∏ p ∈ B, (1 - g p) + suzukiActualT S (2 * T.card + 1) ⌈L⌉₊ ⌈u⌉₊

The lower depth is even and its sum is subtracted; the upper depth is odd and its sum is added. Both exhaust the zero-deleted finite carrier.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.densityDefects_eq_suzukiActualT (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) (huL : u ≤ L) (hcut : ∀ p ∈ B, ↑p < u) : have S := densityBoundingSieve B hB g hgm hg; have T := nonzeroDensityPrimes B ⇑g; lowerDensityDefect L (⇑g) (B.sort fun (x1 x2 : ℕ) => x1 ≤ x2) = suzukiActualT S (2 * (T.card + 1)) ⌈L⌉₊ ⌈u⌉₊ ∧ upperDensityDefect L (⇑g) (B.sort fun (x1 x2 : ℕ) => x1 ≤ x2) = suzukiActualT S (2 * T.card + 1) ⌈L⌉₊ ⌈u⌉₊

Exact identification of the whole original boundary defects, not just their high-minimum-prime contributions.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.smallDensityBoundingSieve_hasDimensionOneLocalProductBound (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) : SwitchingPrinciple.HasDimensionOneLocalProductBound (smallDensityBoundingSieve P D ε g hgm hg) K

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.smallDensityDefects_eq_suzukiActualT (P : Finset ℕ) {D ε : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) (hε1 : ε ≤ 1) (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; have T := nonzeroDensityPrimes B ⇑g; lowerDensityDefect (D ^ ε) (⇑g) (B.sort fun (x1 x2 : ℕ) => x1 ≤ x2) = suzukiActualT S (2 * (T.card + 1)) ⌈D ^ ε⌉₊ ⌈D ^ ε ^ 2⌉₊ ∧ upperDensityDefect (D ^ ε) (⇑g) (B.sort fun (x1 x2 : ℕ) => x1 ≤ x2) = suzukiActualT S (2 * T.card + 1) ⌈D ^ ε⌉₊ ⌈D ^ ε ^ 2⌉₊