OAI/NumberTheory/Ostmann/Preliminaries/AdditiveSieveProbability.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The additive large sieve for a uniform measure on an actual interval subset

  1. def OAI.Ostmann.intervalSetExponentialSum line 11
  2. def OAI.Ostmann.intervalSetReducedEnergy line 15
  3. theorem OAI.Ostmann.intervalSetReducedEnergy_nonneg line 20
  4. theorem OAI.Ostmann.additiveSieve_probability_bound line 25

    Source documentation

    No density or distribution assumption on the interval subset is needed.

    theorem additiveSieve_probability_bound (ls : PublishedAdditiveLargeSieve)
    {M Q : ℕ} (hM : 1 ≤ M) (hQ : 1 ≤ Q) (A : Finset (Fin M))
    (hA : A.Nonempty) (J : ℤ) :
    (∑ q ∈ Finset.Icc 1 Q, intervalSetReducedEnergy A J q) ≤
      ((M : ℝ) + (Q : ℝ) ^ 2) / A.card := by
…

    Mentions: OAI.Ostmann.PublishedAdditiveLargeSieve, OAI.Ostmann.intervalSetReducedEnergy

  5. theorem OAI.Ostmann.sieveAdditivePhase_eq_stdAddChar line 50