OAI/NumberTheory/Ostmann/Quadratic/QuadraticAmplificationCoefficients.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.primeSubsetCoefficient line 12
2. theorem OAI.Ostmann.primeSubsetCoefficient_norm_le line 16
3. theorem OAI.Ostmann.primeSubsetCoefficient_energy_le line 30
4. theorem OAI.Ostmann.amplification_numeric_budget line 53
5. theorem OAI.Ostmann.quadratic_amplification_energy line 73

   Source documentation

   This is the k! / J^k energy bound in the manuscript, for an actual coefficient function supported on products of distinct primes.

   theorem quadratic_amplification_energy (P : Finset ℕ) (k N : ℕ) (e : ℕ → ℂ)
       (hP : ∀ p ∈ P, p.Prime) (he : ∀ p ∈ P, ‖e p‖ ≤ 1) (hcard : 0 < P.card) :
       quadraticSieveEnergy N (primeSubsetCoefficient P k
         (((k.factorial : ℝ) / (P.card : ℝ) ^ k : ℝ) : ℂ) e) ≤
           (k.factorial : ℝ) / (P.card : ℝ) ^ k := by
   …

   Mentions: OAI.Ostmann.quadraticSieveEnergy, OAI.Ostmann.primeSubsetCoefficient