MRTTypicalDensity.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The dense typical set in MRT Lemma 2.2, with a uniform translated finite-interval formulation. No fundamental-lemma-of-sieve input remains: the finite Bonferroni estimate and the proved Mertens bound suffice here.

lemma OAI.TwoPointCorrelations.mrt_band_count_le_scale line 15
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTTypicalDensity.lean:15 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_band_small_error line 31
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTTypicalDensity.lean:31 (same declaration text).

theorem OAI.TwoPointCorrelations.mrt_typical_density line 54

Source documentation

Every family of the explicit MRT bands below the allowed upper cutoff has missing density O(log P / log Q), uniformly in translation. The family need not be chosen maximal.

Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTTypicalDensity.lean:54 (same declaration text).

theorem mrt_typical_density : ∃ C : ℝ, 0 < C ∧
    ∀ᶠ L : ℝ in atTop, ∀ (P Q : ℝ) (J : ℕ),
      2 ≤ P → P ≤ Q → 1 ≤ Real.log Q →
      (∀ j ∈ Icc 1 J, mrtBandUpper Q j ≤ Real.exp (L ^ (99 / 100 : ℝ))) →
      ∀ (A N : ℕ) [NeZero N],
      (1 / 2 : ℝ) * Real.exp (L ^ (199 / 200 : ℝ)) ≤ N →
      (uniformFiniteLaw (Fin N)).probability
        (fun n => ¬mrtTypical univ
          (fun j : {j : ℕ // j ∈ (Icc 1 J : Finset ℕ)} =>
            mrtPrimeBand (mrtBandLower P Q j) (mrtBandUpper Q j)) (A + n.val)) ≤
        C * Real.log P / Real.log Q := by
…

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