WeightedMultiplierSupply.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The weighted positive-density supply used in the sieve amplification

theorem OAI.Ostmann.goodSieveMultipliers_coprime line 10
theorem OAI.Ostmann.weighted_multiplier_supply line 20

theorem OAI.Ostmann.weighted_multiplier_supply_inv line 55

Source documentation

The same supply is available for the reciprocal imbalance factors.

theorem weighted_multiplier_supply_inv (U : ℕ) (T P : Finset ℕ) (κ : ℕ → ℝ)
    (hκ : ∀ p ∈ P, 0 < κ p) (hTprime : ∀ p ∈ T, Nat.Prime p)
    (B : ℝ) (hB : 0 < B)
    (hT : (∑ p ∈ T, (p : ℝ)⁻¹) ≤ 1 / 16)
    (hP : (∑ p ∈ P, |Real.log (κ p)| / p) ≤ B / 16) :
    (U : ℝ) / 8 * Real.exp (-B) ≤
      ∑ u ∈ (positiveMultipliers U).filter
        (fun u => Squarefree u ∧ u.Coprime (∏ p ∈ T, p)),
          multiplierRatioProduct P (fun p => (κ p)⁻¹) u := by
…

Mentions: OAI.Ostmann.positiveMultipliers, OAI.Ostmann.multiplierRatioProduct