RoughFourierSieve.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The manuscript rough-integer Fourier estimates, deduced from the published bounded Mertens input and the proved finite sieve.

theorem OAI.TwoPointCorrelations.PrimeReciprocalInput.rough_fourier line 17

Source documentation

Manuscript (q:rough-fourier), uniformly in the interval length and in every subset of the integers having no prime factor below the cutoff.

theorem PrimeReciprocalInput.rough_fourier (hM : PrimeReciprocalInput) :
    ∃ U V : ℝ, 0 < U ∧ 0 < V ∧ ∀ᶠ L : ℝ in atTop,
      ∀ (D h : ℕ), (1 / 2 : ℝ) * Real.exp (L ^ (199 / 200 : ℝ)) ≤ D → 0 < h →
      ∀ Z : Finset ℕ,
      (∀ z ∈ Z, D ≤ z ∧ z < D + D ∧
        avoidsPrimeSet (sievePrimesUpTo (Real.exp (L ^ (99 / 100 : ℝ)))) z) →
      (∀ θ, ‖roughFourierPolynomial Z h θ‖ ≤ U * L ^ (-99 / 100 : ℝ)) ∧
      (∫ θ, ‖roughFourierPolynomial Z h θ‖ ^ 4 ∂AddCircle.haarAddCircle) ≤
        V / (D : ℝ) * L ^ (-99 / 25 : ℝ) := by
…

Mentions: OAI.TwoPointCorrelations.PrimeReciprocalInput, OAI.TwoPointCorrelations.avoidsPrimeSet, OAI.TwoPointCorrelations.sievePrimesUpTo, OAI.TwoPointCorrelations.roughFourierPolynomial