noncomputable def MathlibNt.SieveTheory.suzukiSupportedBelowList (S : BoundingSieve) (z : ℕ) : List ℕ

The canonical increasing list of supported primes below z.

Equations

• MathlibNt.SieveTheory.suzukiSupportedBelowList S z = (MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S z).sort fun (x1 x2 : ℕ) => x1 ≤ x2

@[simp]

theorem MathlibNt.SieveTheory.suzukiSupportedBelowList_toFinset (S : BoundingSieve) (z : ℕ) : (suzukiSupportedBelowList S z).toFinset = SwitchingPrinciple.suzukiSupportedBelow S z

theorem MathlibNt.SieveTheory.lowerRosserBoundaryMass_eq_sum_fixedPairDepth0Density (nu : ℕ → ℝ) {D q : ℕ} {P : Finset ℕ} (hqP : q ∉ P) (hqprime : Nat.Prime q) (hqmin : ∀ p ∈ P, q ≤ p) : LinearSieve.lowerRosserBoundaryMass nu D q P = ∑ k ∈ Finset.range (P.card + 1), LinearSieve.lowerRosserBoundaryChainsFixedPairDepth0Density nu D q P k

Every finite boundary powerset mass is the sum of all its exact even source layers. The range P.card + 1 is a structural support bound, not a fixed-depth replacement.

theorem MathlibNt.SieveTheory.lowerRosserBoundaryAccum_supportedBelow_eq_primeSum (S : BoundingSieve) (D z : ℕ) : LinearSieve.lowerRosserBoundaryAccum (⇑S.nu) D ∅ (suzukiSupportedBelowList S z) = ∑ q ∈ SwitchingPrinciple.suzukiSupportedBelow S z, S.nu q * sourceDiscreteEuler S q * LinearSieve.lowerRosserBoundaryMass (⇑S.nu) D q ({r ∈ SwitchingPrinciple.suzukiSupportedBelow S z | q < r})

Exact expansion of the production accumulator over its canonical supported prime list. The prefix Euler product is the source terminal factor.

noncomputable def MathlibNt.SieveTheory.lowerSuzukiUnnormalizedLayer (S : BoundingSieve) (D z k : ℕ) : ℝ

The unnormalized exact pair-depth layer. Unlike lowerSuzukiNormalizedLayer, its terminal factor is Suzuki's finite Euler product below q, exactly as in the production accumulator.

Equations

• MathlibNt.SieveTheory.lowerSuzukiUnnormalizedLayer S D z k = ∑ q ∈ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S z, S.nu q * MathlibNt.SieveTheory.sourceDiscreteEuler S q * MathlibNt.SieveTheory.lowerSuzukiDiscreteKernel S D z k q

theorem MathlibNt.SieveTheory.ceilDiv_ceilDiv_eq {D a b : ℕ} (ha : 0 < a) (hb : 0 < b) : D ⌈/⌉ a ⌈/⌉ b = D ⌈/⌉ (a * b)

Successive ceiling divisions by positive divisors equal division by their product.

theorem MathlibNt.SieveTheory.lowerRosserEvenBoundaryLayerMass_eq_unnormalizedLayer (S : BoundingSieve) (D z k : ℕ) (hzD : z ≤ D) : lowerRosserEvenBoundaryLayerMass S k D z = lowerSuzukiUnnormalizedLayer S D z k

Exact all-depth layer bridge: pair depth k is Suzuki source depth 2*(k+1), with no fixed-depth truncation.