MRTArcQuotientScale.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The correction divisor and the gcd divisor together cost at most W^6. These bounds retain the actual floor quotients after subdivision.

lemma OAI.TwoPointCorrelations.mrt_arc_combined_divisor line 13
lemma OAI.TwoPointCorrelations.mrt_arc_quotient_window_lower line 22
lemma OAI.TwoPointCorrelations.mrt_arc_quotient_window_power line 39
lemma OAI.TwoPointCorrelations.mrt_arc_quotient_window_log line 52
lemma OAI.TwoPointCorrelations.mrt_arc_quotient_prime_ratio line 68

theorem OAI.TwoPointCorrelations.mrt_arc_quotient_outer_logs line 84

Source documentation

All corrected and gcd-divided outer cutoffs have comparable logarithms. The exponent 1/170 leaves room for the combined W^6 denominator.

theorem mrt_arc_quotient_outer_logs :
    ∀ᶠ X : ℕ in atTop, 2 ≤ Real.log (X : ℝ) ∧
      ∀ W : ℝ, 1 ≤ W → W ≤ (Real.log (X : ℝ)) ^ (1 / 170 : ℝ) →
      ∀ c : ℕ, 0 < c → (c : ℝ) ≤ W ^ (6 : ℕ) →
        Real.log (X : ℝ) / 2 ≤ Real.log (X / c + 1 : ℕ) ∧
        Real.log (X / c + 1 : ℕ) ≤ 2 * Real.log (X : ℝ) := by
…

lemma OAI.TwoPointCorrelations.mrt_arc_long_prefix_quotient_lower line 111
Source documentation
The longer prefix cutoff used after partial summation loses W^4 before the two divisor extractions.
```
lemma mrt_arc_long_prefix_quotient_lower {W H : ℝ} {h c : ℕ}
    (hW : 0 < W) (hc : 0 < c) (hcW : (c:ℝ) ≤ W^6)
    (hh : H/W^4 ≤ (h:ℝ)) :
    H/W^10 ≤ (h/c+1:ℕ) := by
…
```
lemma OAI.TwoPointCorrelations.mrt_arc_long_prefix_quotient_power line 127
lemma OAI.TwoPointCorrelations.mrt_arc_long_prefix_quotient_log line 140
lemma OAI.TwoPointCorrelations.mrt_arc_long_prefix_prime_ratio line 156