noncomputable def MathlibNt.SieveTheory.suzukiElementaryMass (S : BoundingSieve) (n z : ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.suzukiElementaryMass S n z = ∑ t ∈ Finset.powersetCard n (MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S z), ∏ p ∈ t, S.nu p

theorem MathlibNt.SieveTheory.suzukiSourceV_le_elementaryMass (S : BoundingSieve) (n D z : ℕ) : suzukiSourceV S n D z ≤ suzukiElementaryMass S n z

The literal source recursion is bounded by the elementary symmetric mass on all supported primes below z; source cutoffs are only discarded by nonnegativity.