MRTWeakVKScale.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Quantitative height bookkeeping for the original character range. Every fixed tail exponent greater than 2/3 absorbs the two logarithmic factors in the weak VK derivative estimate.

lemma OAI.TwoPointCorrelations.mrt_VK_height_upper line 15
lemma OAI.TwoPointCorrelations.mrt_VK_weight_upper line 26
lemma OAI.TwoPointCorrelations.mrt_VK_log_square_decay line 43

theorem OAI.TwoPointCorrelations.mrt_VK_power_tail_parameters line 67

Source documentation

Both explicit hypotheses of the finite prime-tail estimate hold in the original modulus range and at every height up to X.

theorem mrt_VK_power_tail_parameters {a : ℝ} (ha : (2 / 3 : ℝ) < a) (_ha1 : a ≤ 1) :
    ∀ᶠ X : ℕ in atTop, ∀ (q : ℕ) [NeZero q],
      (q : ℝ) ≤ (Real.log (X : ℝ)) ^ (1 / 125 : ℝ) →
      ∀ t : ℝ, |t| ≤ 6 * X → 1 ≤ mrtVKLog (2 * t) →
        (1 / Real.log (mrtPrimePowerCutoff a X : ℝ) ≤ mrtVKRadius (2 * t) / 16) ∧
        ((mrtVKWeight q (2 * t)) ^ 2 * (mrtVKLog (2 * t)) ^ (2 / 3 : ℝ) ≤
          Real.log (mrtPrimePowerCutoff a X : ℝ)) := by
…

Mentions: OAI.TwoPointCorrelations.mrtVKLog, OAI.TwoPointCorrelations.mrtPrimePowerCutoff, OAI.TwoPointCorrelations.mrtVKRadius, OAI.TwoPointCorrelations.mrtVKWeight