OAI/NumberTheory/Ostmann/Supply/SubsetEnergyAmplification.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.subset_energy_amplification line 10
2. theorem OAI.Ostmann.prime_subset_energy_budget line 44

   Source documentation

   Once the concrete extension weights are supplied, the actual centered subset energies inherit the classical additive-sieve budget.

   theorem prime_subset_energy_budget (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))) (hS : ∀ i, (S i).Nonempty)
       (F 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)
       (α : ℝ) (hweight : ∀ T ∈ F, α ≤ ∑ R ∈ G,
         if T ⊆ R then subsetSieveCoefficient p S R T else 0) :
       α * (∑ T ∈ F, centeredSubsetEnergy p S T A
         (fun x i => ((J + (x.val : ℤ) : ℤ) : ZMod (p i)))) ≤
   …

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