MRTFinalBand.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The actual finite band family ending below exp(sqrt(log N)). Its final lower endpoint is large enough for the optimized sample estimate.

lemma OAI.TwoPointCorrelations.mrt_eventually_final_band_target line 13

theorem OAI.TwoPointCorrelations.mrt_final_band_geometry line 33

Source documentation

P and Q may vary with L. The disjunction handles the possible one-band family without assuming a large second band exists.

theorem mrt_final_band_geometry :
    ∀ᶠ L : ℝ in atTop, ∀ P Q : ℝ,
    1 ≤ Real.log P → 1 ≤ Real.log Q → Real.log Q ≤ Real.sqrt L →
    (200*Real.log L+1 ≤ Real.log P ∨
      Real.log (mrtBandUpper Q 2) ≤ Real.sqrt L) →
    ∃ J : ℕ, 1 ≤ J ∧
      200*Real.log L+1 ≤ Real.log (mrtBandLower P Q J) ∧
      Real.sqrt L < Real.log (mrtBandUpper Q (J+1)) ∧
      ∀ j ∈ Icc 1 J, Real.log (mrtBandUpper Q j) ≤ Real.sqrt L := by
…

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

theorem OAI.TwoPointCorrelations.mrt_final_band_geometry_fixed line 48

Source documentation

For fixed initial bands, the second-band alternative eventually holds. Thus no growing initial lower endpoint is needed in this case.

theorem mrt_final_band_geometry_fixed (P Q : ℝ)
    (hP : 1 ≤ Real.log P) (hQ : 1 ≤ Real.log Q) :
    ∀ᶠ L : ℝ in atTop, ∃ J : ℕ, 1 ≤ J ∧
      200*Real.log L+1 ≤ Real.log (mrtBandLower P Q J) ∧
      Real.sqrt L < Real.log (mrtBandUpper Q (J+1)) ∧
      ∀ j ∈ Icc 1 J, Real.log (mrtBandUpper Q j) ≤ Real.sqrt L := by
…

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