RoughLiouvilleShifts.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The complete quantitative rough-shift analytic estimate, conditional only on the stated published Mertens and MRT inputs.

theorem OAI.TwoPointCorrelations.rough_liouville_shifts line 16

Source documentation

Manuscript (q:rough-shifts), including arbitrary (possibly nonunit) progression classes. The finite rough set is unrestricted within its interval.

theorem rough_liouville_shifts (hM : PrimeReciprocalInput)
    (hMRT : MRTLiouvilleShortInput) (h : ℕ) (hh : 0 < h) :
    ∃ C : ℝ, 0 < C ∧ ∀ᶠ L : ℝ in atTop, ∀ Y D l : ℕ,
      (1 / 2 : ℝ) * Real.exp (L ^ (199 / 200 : ℝ)) ≤ D →
      (D : ℝ) ≤ Real.exp (2 * L) →
      Real.exp ((1 / 2 : ℝ) * L ^ (1000 : ℝ)) ≤ Y →
      ∀ [NeZero l] (a : ZMod l) (Z : Finset ℕ),
      (∀ z ∈ Z, D ≤ z ∧ z < D + D ∧
        avoidsPrimeSet (sievePrimesUpTo (Real.exp (L ^ (99 / 100 : ℝ)))) z) →
      ‖roughShiftAverage (progressionSequence liouville l a) liouville Z h Y‖ ≤
        C * L ^ (-21 / 20 : ℝ) := by
…

Mentions: OAI.TwoPointCorrelations.PrimeReciprocalInput, OAI.TwoPointCorrelations.MRTLiouvilleShortInput, OAI.TwoPointCorrelations.avoidsPrimeSet, OAI.TwoPointCorrelations.sievePrimesUpTo, OAI.TwoPointCorrelations.roughShiftAverage, OAI.TwoPointCorrelations.progressionSequence