MRTScale.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Numerical scale estimates for the published MRT short-sum error.

lemma OAI.TwoPointCorrelations.eventually_four_log_le_small_power line 12

theorem OAI.TwoPointCorrelations.eventually_mrtShortError_scale line 24

Source documentation

The two published error terms have the required power saving under the precise logarithmic consequences of the manuscript scale choices.

theorem eventually_mrtShortError_scale :
    ∀ᶠ L : ℝ in atTop, ∀ X D : ℕ,
      (1 / 2 : ℝ) * L ^ (199 / 200 : ℝ) ≤ Real.log D →
      Real.log D ≤ 2 * L → L ^ (560 : ℝ) ≤ Real.log X →
      mrtShortError X D ≤ 2 * L ^ (-4 / 5 : ℝ) := by
…

Mentions: OAI.TwoPointCorrelations.mrtShortError

theorem OAI.TwoPointCorrelations.eventually_mrtShortError_cutoffs line 61

Source documentation

The original exponential cutoff hypotheses imply all logarithmic conditions above, with no integer-floor or endpoint loss.

theorem eventually_mrtShortError_cutoffs :
    ∀ᶠ L : ℝ in atTop, ∀ X D : ℕ,
      (1 / 2 : ℝ) * Real.exp (L ^ (199 / 200 : ℝ)) ≤ D →
      (D : ℝ) ≤ Real.exp (2 * L) →
      Real.exp ((1 / 2 : ℝ) * L ^ (1000 : ℝ)) ≤ X →
      mrtShortError X D ≤ 2 * L ^ (-4 / 5 : ℝ) := by
…

Mentions: OAI.TwoPointCorrelations.mrtShortError

theorem OAI.TwoPointCorrelations.MRTLiouvilleShortInput.progression_window_scale line 101

Source documentation

The published short-interval theorem now bounds the actual progression polynomials on the manuscript scales. The bound is uniform over the circle.

theorem MRTLiouvilleShortInput.progression_window_scale (hMRT : MRTLiouvilleShortInput) :
    ∃ C : ℝ, 0 < C ∧ ∀ᶠ L : ℝ in atTop, ∀ (Y D l : ℕ),
      1 ≤ Y → 10 ≤ D → D ≤ Y + 1 →
      (1 / 2 : ℝ) * Real.exp (L ^ (199 / 200 : ℝ)) ≤ D →
      (D : ℝ) ≤ Real.exp (2 * L) →
      Real.exp ((1 / 2 : ℝ) * L ^ (1000 : ℝ)) ≤ (Y + 1 : ℕ) →
      ∀ [NeZero l] (a : ZMod l) (θ : AddCircle (1 : ℝ)),
        (∑ v ∈ Finset.range Y,
          ‖forwardWindowPolynomial (progressionSequence liouville l a) D (v + 1) θ‖) ≤
            C * Y * D * L ^ (-4 / 5 : ℝ) := by
…

Mentions: OAI.TwoPointCorrelations.MRTLiouvilleShortInput, OAI.TwoPointCorrelations.forwardWindowPolynomial, OAI.TwoPointCorrelations.progressionSequence