OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCorrectionWindowScale.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Dividing by the small correction factors preserves the logarithmic short-window and outer-scale rates. All floor quotients remain literal.

  1. lemma OAI.TwoPointCorrelations.mrt_correction_window_log_lower line 13
  2. lemma OAI.TwoPointCorrelations.mrt_loglog_ratio_of_comparable line 29
  3. theorem OAI.TwoPointCorrelations.mrt_correction_window_log_rate line 49
  4. theorem OAI.TwoPointCorrelations.mrt_correction_outer_log_scale line 73

    Source documentation

    The published modulus-size bound keeps each corrected outer cutoff within a fixed logarithmic factor of the original cutoff.

    theorem mrt_correction_outer_log_scale :
    ∀ᶠ X : ℕ in atTop, 2 ≤ Real.log (X : ℝ) ∧
      ∀ W : ℝ, 1 ≤ W → W ≤ (Real.log (X : ℝ)) ^ (1 / 125 : ℝ) →
      ∀ d : ℕ, 0 < d → (d : ℝ) ≤ W ^ (5 : ℕ) →
        Real.log (X : ℝ) / 2 ≤ Real.log (X / d + 1 : ℕ) ∧
        Real.log (X / d + 1 : ℕ) ≤ 2 * Real.log (X : ℝ) := by
…