MRTWorkingLength.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Cap the original short length before choosing its prime bands. The uncapped branch is kept exactly; on the capped branch the omitted final block is negligible compared with W^(-1/4).

def OAI.TwoPointCorrelations.mrtWorkingCap line 14
def OAI.TwoPointCorrelations.mrtWorkingLength line 17
lemma OAI.TwoPointCorrelations.mrt_working_cap_upper line 20
theorem OAI.TwoPointCorrelations.mrt_working_cap_power line 25
Source documentation
The fixed cap eventually exceeds every prescribed power of W.
```
theorem mrt_working_cap_power (a : ℕ) :
    ∀ᶠ W : ℝ in atTop, W ^ a ≤ (mrtWorkingCap W : ℝ) := by
…
```
Mentions: OAI.TwoPointCorrelations.mrtWorkingCap
lemma OAI.TwoPointCorrelations.mrt_working_length_upper line 58
lemma OAI.TwoPointCorrelations.mrt_working_length_exp_upper line 68
lemma OAI.TwoPointCorrelations.mrt_working_length_power line 76
lemma OAI.TwoPointCorrelations.mrt_working_tail_exp line 82
lemma OAI.TwoPointCorrelations.mrt_working_length_remainder line 92
Source documentation
Either no subdivision is performed, or the final incomplete block has relative length at most W^(-1/4).
```
lemma mrt_working_length_remainder {H : ℕ} {W : ℝ} (hW : 0 < W) :
    mrtWorkingLength H W = H ∨
      (mrtWorkingLength H W : ℝ) / H ≤ W ^ (-(1 / 4 : ℝ)) := by
…
```
Mentions: OAI.TwoPointCorrelations.mrtWorkingLength
lemma OAI.TwoPointCorrelations.mrt_working_length_loglog line 112
theorem OAI.TwoPointCorrelations.mrt_working_cap_log line 123

theorem OAI.TwoPointCorrelations.mrt_working_original_power line 142

Source documentation

The bound W ≤ log(H)^5 forces H above any fixed power of W.

theorem mrt_working_original_power (a : ℕ) :
    ∀ᶠ W : ℝ in atTop, ∀ H : ℝ, 0 < H → 1 ≤ Real.log H →
      W ≤ (Real.log H) ^ (5 : ℕ) → W ^ a ≤ H := by
…