MRTMaximalBand.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A maximal actual MRT band below a prescribed logarithmic cutoff. The cubic next-band comparison supplies a large final lower endpoint.

lemma OAI.TwoPointCorrelations.mrt_band_upper_log_mono line 13
theorem OAI.TwoPointCorrelations.mrt_maximal_band_exists line 25
lemma OAI.TwoPointCorrelations.mrt_next_band_log_le_lower_cube line 53
Source documentation
Cubing the last lower endpoint dominates the next upper endpoint; the small exceptional index is handled by direct integer arithmetic.
```
lemma mrt_next_band_log_le_lower_cube {P Q : ℝ}
    (hP : 1 ≤ Real.log P) (hQ : 1 ≤ Real.log Q) {j : ℕ} (hj : 2 ≤ j) :
    Real.log (mrtBandUpper Q (j+1)) ≤ Real.log (mrtBandLower P Q j)^3 := by
…
```
Mentions: OAI.TwoPointCorrelations.mrtBandUpper, OAI.TwoPointCorrelations.mrtBandLower

theorem OAI.TwoPointCorrelations.mrt_maximal_band_lower line 80

Source documentation

The first-band alternative covers J=1. Otherwise maximality and the cubic comparison force the final lower endpoint above the desired target.

theorem mrt_maximal_band_lower {P Q B K : ℝ}
    (hP : 1 ≤ Real.log P) (hQ : 1 ≤ Real.log Q)
    (hB : Real.log Q ≤ B) (hK : K^3 ≤ B)
    (hfirst : K ≤ Real.log P ∨ Real.log (mrtBandUpper Q 2) ≤ B) :
    ∃ J : ℕ, 1 ≤ J ∧ K ≤ Real.log (mrtBandLower P Q J) ∧
      B < Real.log (mrtBandUpper Q (J+1)) ∧
      ∀ j ∈ Icc 1 J, Real.log (mrtBandUpper Q j) ≤ B := by
…

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