GoodSieveMultipliers.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Simultaneously squarefree, coprime and low-weight sieve multipliers

def OAI.Ostmann.goodSieveMultipliers line 10

theorem OAI.Ostmann.goodSieveMultipliers_card_lower line 17

Source documentation

An explicit positive proportion. The hypotheses will be furnished by prime reciprocal and logarithmic-imbalance estimates in the application.

theorem goodSieveMultipliers_card_lower (U : ℕ) (T P : Finset ℕ) (w : ℕ → ℝ)
    (hw : ∀ p ∈ P, 0 ≤ w p) (B : ℝ) (hB : 0 < B)
    (hT : (∑ p ∈ T, (p : ℝ)⁻¹) ≤ 1 / 16)
    (hP : (∑ p ∈ P, w p / p) ≤ B / 16) :
    (U : ℝ) / 8 ≤ (goodSieveMultipliers U T P w B).card := by
…

Mentions: OAI.Ostmann.goodSieveMultipliers