SieveRemainders.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Elementary bounds for the total sieve remainder

A crude fixed power of the level suffices: the manuscript allows a fixed sieve cutoff sufficiently small compared with the counting scale.

theorem OAI.JointDickman.prime_card_power_le_product_power line 17
Source documentation
Fixed exponential weights in the number of prime factors admit a fixed polynomial bound in the product.
```
theorem prime_card_power_le_product_power (D : Finset ℕ)
    (hD : ∀ p ∈ D, p.Prime) (k : ℕ) :
    k ^ D.card ≤ (∏ p ∈ D, p) ^ k := by
…
```

theorem OAI.JointDickman.sieve_level_power_sum line 28

Source documentation

Distinct subsets give distinct squarefree products; summing their fixed-factor-count weights below N costs at most N^(k+1)+N^k.

theorem sieve_level_power_sum (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
    (k N : ℕ) :
    (∑ D ∈ P.powerset.filter (fun D => (∏ p ∈ D, p) ≤ N), k ^ D.card) ≤
      (N + 1) * N ^ k := by
…

theorem OAI.JointDickman.sieve_level_root_sum line 58

Source documentation

The same level bound with arbitrary local root counts bounded by k.

theorem sieve_level_root_sum (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
    (r : ℕ → ℕ) (k N : ℕ) (hr : ∀ p ∈ P, r p ≤ k) :
    (∑ D ∈ P.powerset.filter (fun D => (∏ p ∈ D, p) ≤ N), ∏ p ∈ D, r p) ≤
      (N + 1) * N ^ k := by
…