OAI/NumberTheory/TwoPoint/Bounds/RoughSieveCounts.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Passing from actual uniform samples to subset and additive-energy counts. Every additive quadruple is injected into its first three entries.

  1. lemma OAI.TwoPointCorrelations.uniformFiniteLaw_probability line 14
  2. def OAI.TwoPointCorrelations.roughIntervalSamples line 21
  3. def OAI.TwoPointCorrelations.roughCubeSamples line 24
  4. lemma OAI.TwoPointCorrelations.roughIntervalSamples_probability line 29
  5. lemma OAI.TwoPointCorrelations.roughCubeSamples_probability line 37
  6. theorem OAI.TwoPointCorrelations.rough_subset_card_le line 48
  7. def OAI.TwoPointCorrelations.additiveQuadruples line 70
  8. lemma OAI.TwoPointCorrelations.mem_additiveQuadruples line 74
  9. theorem OAI.TwoPointCorrelations.rough_additiveQuadruples_card_le line 80
  10. theorem OAI.TwoPointCorrelations.roughFourier_bounds_of_sieve line 131

    Source documentation

    The actual rough interval and three-variable sieve probabilities imply both manuscript Fourier bounds, uniformly over every subset of rough integers.

    theorem roughFourier_bounds_of_sieve (P Z : Finset ℕ) (D h : ℕ) [NeZero D]
    (hh : 0 < h) (L U V : ℝ)
    (hZ : ∀ z ∈ Z, D ≤ z ∧ z < D + D ∧ avoidsPrimeSet P z)
    (h₁ : (uniformFiniteLaw (Fin D)).probability
      (fun j => avoidsPrimeSet P (D + j.val)) ≤ U * L ^ (-99 / 100 : ℝ))
    (h₄ : (uniformFiniteLaw (Fin D × Fin D × Fin D)).probability
      (fun j => fourFormsAvoidPrimeSet P
        (D + j.1.val, D + j.2.1.val, D + j.2.2.val)) ≤ V * L ^ (-99 / 25 : ℝ)) :
    (∀ θ, ‖roughFourierPolynomial Z h θ‖ ≤ U * L ^ (-99 / 100 : ℝ)) ∧
      (∫ θ, ‖roughFourierPolynomial Z h θ‖ ^ 4 ∂AddCircle.haarAddCircle) ≤
        V / (D : ℝ) * L ^ (-99 / 25 : ℝ) := by
…

    Mentions: OAI.TwoPointCorrelations.avoidsPrimeSet, OAI.TwoPointCorrelations.uniformFiniteLaw, OAI.TwoPointCorrelations.fourFormsAvoidPrimeSet, OAI.TwoPointCorrelations.roughFourierPolynomial