MRTWorkingDensity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform finite-interval density for the actual working prime bands. The outer and working-parameter thresholds are independent.

theorem OAI.TwoPointCorrelations.mrt_actual_band_interval_density line 16

Source documentation

The explicit natural-indexed bands have the same density estimate on every translated interval of length at least the original outer cutoff.

theorem mrt_actual_band_interval_density :
    ∃ C : ℝ, 0 < C ∧ ∀ᶠ X : ℕ in atTop,
      ∀ (P Q : ℝ) (J : ℕ), 2 ≤ P → P ≤ Q → 1 ≤ Real.log Q →
      (∀ j ∈ Icc 1 J, mrtBandUpper Q j ≤
        Real.exp (Real.sqrt (Real.log (X:ℝ))/2)) →
      ∀ (A N : ℕ) [NeZero N], X ≤ N →
      (uniformFiniteLaw (Fin N)).probability
        (fun n => ¬mrtTypical (Icc 1 J)
          (fun j => 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

theorem OAI.TwoPointCorrelations.mrt_working_interval_density line 62

Source documentation

For the actual working first band the missing density has exactly the working error rate, uniformly in translation and all longer intervals.

theorem mrt_working_interval_density :
    ∃ C : ℝ, 0 < C ∧ ∃ W₀ : ℝ, ∃ X₀ : ℕ,
      ∀ W : ℝ, W₀ ≤ W → ∀ H : ℕ, 0 < H →
      1 ≤ Real.log (H:ℝ) → W ≤ Real.log (H:ℝ)^5 →
      ∀ X : ℕ, X₀ ≤ X → ∀ J : ℕ,
      let P := W^(500000:ℕ)
…