PrimeSubsetSieve.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Summing the positive subset expansion inside the additive large sieve

theorem OAI.Ostmann.prime_subset_product_dvd_iff line 10
theorem OAI.Ostmann.prime_subset_product_injective line 22

theorem OAI.Ostmann.prime_subset_sieve_bound line 33

Source documentation

The complete double sum is bounded by the classical additive large sieve. No centered-coordinate energy estimate is postulated in this step.

theorem prime_subset_sieve_bound (ls : PublishedAdditiveLargeSieve)
    {n M Q : ℕ} (p : Fin n → ℕ) [∀ i, Fact (p i).Prime]
    (hc : Pairwise (fun i j => (p i).Coprime (p j)))
    (S : ∀ i, Finset (ZMod (p i))) (G : Finset (Finset (Fin n)))
    (hQ : 1 ≤ Q) (hM : 1 ≤ M) (A : Finset (Fin M)) (hA : A.Nonempty) (J : ℤ)
    (hprod : ∀ R ∈ G, (∏ i ∈ R, p i) ≤ Q)
    (ha : ∀ R ∈ G, ∀ x ∈ A, ∀ i ∈ R, ((J + (x.val : ℤ) : ℤ) : ZMod (p i)) ∈ S i) :
    (∑ R ∈ G, ∑ T ∈ R.powerset, subsetSieveCoefficient p S R T *
      centeredSubsetEnergy p S T A (fun x i => ((J + (x.val : ℤ) : ℤ) : ZMod (p i)))) ≤
      ((M : ℝ) + (Q : ℝ) ^ 2) / A.card := by
…

Mentions: OAI.Ostmann.PublishedAdditiveLargeSieve, OAI.Ostmann.subsetSieveCoefficient, OAI.Ostmann.centeredSubsetEnergy