MellinPrimeSieve.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The proved sieve applied to nonnegative Mellin square weights

lemma OAI.JointDickman.sieve_level_card_le line 13
def OAI.JointDickman.primeDivisorEvents line 23
lemma OAI.JointDickman.primeDivisorEvents_prime line 26

theorem OAI.JointDickman.prime_weighted_sieve line 38

Source documentation

Positive weights on primes larger than the sieve level. The error is the literal sum of residue-class discrepancies of the given weight.

theorem prime_weighted_sieve : ∃ C : ℝ, 0 < C ∧
    ∀ (K Z : ℕ) (P Q : Finset ℕ) (w : ℕ → ℝ) (M R : ℝ),
      2 ≤ Z → 0 ≤ M → 0 ≤ R →
      (∀ p ∈ P, p.Prime ∧ p ≤ Z) →
      Q ⊆ Icc 1 K → (∀ q ∈ Q, q.Prime ∧ Z < q) →
      (∀ n ∈ Icc 1 K, 0 ≤ w n) →
      (∀ D ∈ P.powerset.filter (fun D => (∏ p ∈ D, p) ≤ Z),
        |sieveRemainder (fun n : Icc 1 K => primeDivisorEvents P n)
          (fun n => w n) M (fun p => 1/(p : ℝ)) D| ≤ R) →
      (∑ q ∈ Q, w q) ≤ C*M*(∏ p ∈ P, (1-1/(p : ℝ))) + (Z+1:ℕ)*R := by
…

Mentions: OAI.JointDickman.sieveRemainder, OAI.JointDickman.primeDivisorEvents