noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.suzukiPrimeMassBelow (S : BoundingSieve) (z : ℝ) : ℝ

The finite supported-prime mass below z.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.suzukiPrimeMassBelow S z = ∑ p ∈ S.prodPrimes.primeFactors with ↑p < z, S.nu p

theorem MathlibNt.SieveTheory.SwitchingPrinciple.lemmaFourteenOne_localProduct_mass {S : BoundingSieve} {K z : ℝ} (hlocal : HasDimensionOneLocalProductBound S K) (hz : 2 ≤ z) : suzukiPrimeMassBelow S z ≤ Real.log (Real.log z / Real.log 2) + Real.log (1 + K / Real.log 2)

Lemma 14.1's total-mass estimate, obtained only from the dimension-one local Euler-product bound.