MRTCommonFinalBand.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

One final original band works for both dyadic polynomials at N and 2N. The lower-endpoint margin absorbs the change in log-log scale, while the upper endpoint remains below the smaller square-root cutoff.

lemma OAI.TwoPointCorrelations.mrt_eventually_common_band_target line 13
lemma OAI.TwoPointCorrelations.mrt_dyadic_log_comparison line 31
lemma OAI.TwoPointCorrelations.mrt_dyadic_log_error line 52
lemma OAI.TwoPointCorrelations.mrt_common_density_power line 67
lemma OAI.TwoPointCorrelations.mrt_common_density_cutoff line 72

theorem OAI.TwoPointCorrelations.mrt_log_error_published_rate line 80

Source documentation

The extra-band logarithmic error is smaller than the squared published 1/700 scale.

theorem mrt_log_error_published_rate :
    ∀ᶠ L : ℝ in atTop,
      Real.log L/L^(1/100:ℝ) ≤ L^(-1/350:ℝ) ∧
      Real.sqrt (Real.log L/L^(1/100:ℝ)) ≤ L^(-1/700:ℝ) := by
…

theorem OAI.TwoPointCorrelations.mrt_common_final_band_geometry line 101

Source documentation

The same J satisfies the actual final-band bounds at both dyadic cutoffs, not merely separate existential choices for the two cutoffs.

theorem mrt_common_final_band_geometry :
    ∀ᶠ N : ℕ in atTop, ∀ P Q : ℝ,
      1 ≤ Real.log P → 1 ≤ Real.log Q → Real.log Q ≤ Real.sqrt (Real.log N) →
      (400*Real.log (Real.log N)+1 ≤ Real.log P ∨
        Real.log (mrtBandUpper Q 2) ≤ Real.sqrt (Real.log N)) →
      ∃ J : ℕ, 1 ≤ J ∧
        Real.sqrt (Real.log N) < Real.log (mrtBandUpper Q (J+1)) ∧
        ∀ k ∈ ({N,2*N} : Finset ℕ),
          200*Real.log (Real.log k)+1 ≤ Real.log (mrtBandLower P Q J) ∧
          ∀ i ∈ Icc 1 J, mrtBandUpper Q i ≤ Real.exp (Real.sqrt (Real.log k)) := by
…

Mentions: OAI.TwoPointCorrelations.mrtBandUpper, OAI.TwoPointCorrelations.mrtBandLower

theorem OAI.TwoPointCorrelations.mrt_common_final_band_fixed line 134

Source documentation

For fixed initial P,Q the second-band alternative always holds once N is large, yielding a common final band without extra hypotheses.

theorem mrt_common_final_band_fixed (P Q : ℝ)
    (hP : 1 ≤ Real.log P) (hQ : 1 ≤ Real.log Q) :
    ∀ᶠ N : ℕ in atTop, ∃ J : ℕ, 1 ≤ J ∧
      Real.sqrt (Real.log N) < Real.log (mrtBandUpper Q (J+1)) ∧
      ∀ k ∈ ({N,2*N} : Finset ℕ),
        200*Real.log (Real.log k)+1 ≤ Real.log (mrtBandLower P Q J) ∧
        ∀ i ∈ Icc 1 J, mrtBandUpper Q i ≤ Real.exp (Real.sqrt (Real.log k)) := by
…

Mentions: OAI.TwoPointCorrelations.mrtBandUpper, OAI.TwoPointCorrelations.mrtBandLower