OAI/NumberTheory/TwoPoint/ShortIntervals/MRTExtraBandGeometry.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The additional large-prime interval used after the last ordinary band. A factor two in its lower logarithm absorbs bin rounding.

  1. def OAI.TwoPointCorrelations.mrtExtraPrimeLower line 13
  2. def OAI.TwoPointCorrelations.mrtExtraPrimeUpper line 16
  3. def OAI.TwoPointCorrelations.mrtExtraPrimeResolution line 19
  4. theorem OAI.TwoPointCorrelations.mrt_extra_band_geometry line 21
  5. theorem OAI.TwoPointCorrelations.mrt_extra_band_disjoint line 93

    Source documentation

    The additional interval is disjoint from every original prime set under the proved maximal-band upper cutoff.

    theorem mrt_extra_band_disjoint :
    ∀ᶠ L : ℝ in atTop, ∀ S : Finset ℕ,
      (∀ p ∈ S, (p:ℝ) ≤ Real.exp (Real.sqrt L)) →
      Disjoint S (mrtPrimeBand (mrtExtraPrimeLower L) (mrtExtraPrimeUpper L)) := by
…

    Mentions: OAI.TwoPointCorrelations.mrtPrimeBand, OAI.TwoPointCorrelations.mrtExtraPrimeLower, OAI.TwoPointCorrelations.mrtExtraPrimeUpper