MRTTypicalSieveScale.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform finite-interval error in the sieve for MRT's prime bands. The prime mass uses the proved Mertens theorem; the remaining errors are the explicit Bonferroni and CRT boundary errors.

lemma OAI.TwoPointCorrelations.mrt_exponential_sieve_tail line 15
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalSieveScale.lean:15 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_prime_band_card_le line 33
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalSieveScale.lean:33 (same declaration text).

theorem OAI.TwoPointCorrelations.mrt_eventually_missing_band line 42

Source documentation

A single prime band has its Mertens main term, uniformly in the interval's starting point, plus an error smaller than 2 L^-100.

Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalSieveScale.lean:42 (same declaration text).

theorem mrt_eventually_missing_band : ∃ C : ℝ, 0 < C ∧
    ∀ᶠ L : ℝ in atTop, ∀ P Q : ℝ, 2 ≤ P → P ≤ Q →
      Q ≤ Real.exp (L ^ (99 / 100 : ℝ)) →
      ∀ (A N : ℕ) [NeZero N],
      (1 / 2 : ℝ) * Real.exp (L ^ (199 / 200 : ℝ)) ≤ N →
      (uniformFiniteLaw (Fin N)).probability
        (fun j => mrtPrimeAvoids (mrtPrimeBand P Q) (A + j.val)) ≤
        C * Real.log P / Real.log Q + 2 * L ^ (-100 : ℝ) := by
…

Mentions: OAI.TwoPointCorrelations.uniformFiniteLaw, OAI.TwoPointCorrelations.mrtPrimeAvoids, OAI.TwoPointCorrelations.mrtPrimeBand

theorem OAI.TwoPointCorrelations.mrt_eventually_atypical_family line 91

Source documentation

The uniform band errors add over the actual family of bands; the main term is the sum of their logarithmic endpoint ratios.

Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalSieveScale.lean:91 (same declaration text).

theorem mrt_eventually_atypical_family : ∃ C : ℝ, 0 < C ∧
    ∀ᶠ L : ℝ in atTop, ∀ (ι : Type*) [Fintype ι] (P Q : ι → ℝ),
      (∀ i, 2 ≤ P i) → (∀ i, P i ≤ Q i) →
      (∀ i, Q i ≤ Real.exp (L ^ (99 / 100 : ℝ))) →
      ∀ (A N : ℕ) [NeZero N],
      (1 / 2 : ℝ) * Real.exp (L ^ (199 / 200 : ℝ)) ≤ N →
      (uniformFiniteLaw (Fin N)).probability
        (fun j => ¬mrtTypical univ (fun i => mrtPrimeBand (P i) (Q i)) (A + j.val)) ≤
        C * ∑ i, Real.log (P i) / Real.log (Q i) +
          2 * Fintype.card ι * L ^ (-100 : ℝ) := by
…

Mentions: OAI.TwoPointCorrelations.uniformFiniteLaw, OAI.TwoPointCorrelations.mrtTypical, OAI.TwoPointCorrelations.mrtPrimeBand