MRTShortTrivialCases.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Uniform absorption of the bounded outer scales and small values of the common arc parameter in the exact published short-interval error.

lemma OAI.TwoPointCorrelations.mrt_allowed_short_log line 11
lemma OAI.TwoPointCorrelations.mrt_large_parameter_logs line 18
lemma OAI.TwoPointCorrelations.mrt_short_error_nonneg line 33

lemma OAI.TwoPointCorrelations.mrt_small_arc_parameter line 44

Source documentation

A bounded arc parameter forces either a bounded short length or a bounded exponential-distance parameter.

lemma mrt_small_arc_parameter {X H : ℕ} {B M : ℝ}
    (hB : 2 ≤ B) (hH : 10 ≤ H) (hHX : H ≤ X)
    (hsmall : majorArcParameter (Real.log (X:ℝ)) H M ≤ B) :
    (H:ℝ) ≤ Real.exp (B^(125:ℕ)) ∨ Real.exp (M/3) ≤ B := by
…

Mentions: OAI.TwoPointCorrelations.majorArcParameter

lemma OAI.TwoPointCorrelations.mrt_small_exponential_parameter line 74
theorem OAI.TwoPointCorrelations.mrt_short_trivial_absorption line 89
Source documentation
No lower-distance assumption is needed in any bounded-scale case. The constant is independent of the original function and frequency.
```
theorem mrt_short_trivial_absorption (B₀ : ℝ) (X₀ : ℕ) :
    ∃ C : ℝ, 0<C ∧ ∀ X H : ℕ, 10≤H → H≤X → ∀ M : ℝ,
      (majorArcParameter (Real.log (X:ℝ)) H M ≤ B₀ ∨ X≤X₀) →
      1 ≤ C*(Real.exp (-M/20)+mrtShortError X H) := by
…
```
Mentions: OAI.TwoPointCorrelations.majorArcParameter, OAI.TwoPointCorrelations.mrtShortError
theorem OAI.TwoPointCorrelations.mrt_short_trivial_cases line 132