OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCorrectionArcScale.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The divisor correction preserves the numerical budgets used in the major-arc reduction. In particular, dilation of the additive frequency costs only a factor two in the perturbation budget.

  1. lemma OAI.TwoPointCorrelations.mrt_correction_divisor_le_window line 13
  2. lemma OAI.TwoPointCorrelations.mrt_correction_quotient_volume line 26
  3. lemma OAI.TwoPointCorrelations.mrt_correction_phase_budget line 42
  4. lemma OAI.TwoPointCorrelations.mrt_correction_log_power_saving line 66
  5. theorem OAI.TwoPointCorrelations.mrt_correction_outer_saving line 85

    Source documentation

    The outer logarithmic error in the typical mean is smaller than the required correction scale, uniformly over all small correction divisors.

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