WeightedUpperSieve.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Reducing weights in the published upper sieve

Independent random forbidding derives the Euler factors for arbitrary retained weights in [0,1]. The original remainder is unchanged, and the constant stays uniform over all the retained weights.

theorem OAI.JointDickman.ford_weighted_upper_sieve line 17

theorem OAI.JointDickman.weighted_upper_sieve_from_published line 74

Source documentation

The ready-to-apply bound: only Ford and Mertens remain published inputs; no abstract sieve dimension hypothesis remains.

theorem weighted_upper_sieve_from_published
    (hFord : PublishedInputs.FordUpperSieveInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput)
    {k : ℝ} (hk : 0 < k) :
    ∃ C : ℝ, 0 < C ∧ ∀ (X : Type) [Fintype X]
      (P : Finset ℕ) (E : X → Finset ℕ) (w : X → ℝ) (M z : ℝ)
      (g θ : ℕ → ℝ), 2 ≤ z → 0 ≤ M → (∀ x, 0 ≤ w x) →
      (∀ p ∈ P, p.Prime ∧ (p : ℝ) ≤ z) → (∀ x, E x ⊆ P) →
      (∀ p ∈ P, 0 ≤ g p ∧ g p ≤ 1 / 2 ∧ g p ≤ k / (p : ℝ)) →
      (∀ p ∈ P, 0 ≤ θ p ∧ θ p ≤ 1) →
      (∑ x, w x * ∏ p ∈ E x, θ p) ≤
        C * M * (∏ p ∈ P, (1 - g p + g p * θ p)) +
…

Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput