Documentation

MathlibNt.SieveTheory.LinearSieve.Suzuki.SuzukiLemma141LocalProductMass

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

The finite supported-prime mass below z.

Equations
Instances For
    Inspect dependencies

    MathlibNt.SieveTheory.SwitchingPrinciple.suzukiPrimeMassBelow · compiled type and proof/definition references.

    source
    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.

    Inspect dependencies

    MathlibNt.SieveTheory.SwitchingPrinciple.lemmaFourteenOne_localProduct_mass · compiled type and proof/definition references.