OAI/NumberTheory/TwoPoint/ShortIntervals/MRTRieszTails.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Integrability and the far tails of the shifted quadratic Riesz integral.

  1. lemma OAI.TwoPointCorrelations.mrt_zeta_riesz_integrable line 13
  2. lemma OAI.TwoPointCorrelations.mrt_vertical_power_tails line 51
  3. lemma OAI.TwoPointCorrelations.mrt_shifted_log_height line 83
  4. theorem OAI.TwoPointCorrelations.MRTWeakHurwitzGrowthInput.riesz_far_tail line 102

    Source documentation

    The constant has deliberately ample room; the essential saving is T^-3/2, which can be charged to the pole term even for arbitrarily large cutoffs x.

    theorem MRTWeakHurwitzGrowthInput.riesz_far_tail (h : MRTWeakHurwitzGrowthInput) :
    ∃ C T₀ : ℝ, 0 < C ∧ 0 < T₀ ∧ ∀ x b T u : ℝ,
      0 < x → 1 < b → T₀ ≤ T → |u| ≤ T / 2 →
        ‖VerticalIntegral (mrtZetaRieszIntegrand x u) b -
          VIntegral (mrtZetaRieszIntegrand x u) b (-T) T‖ ≤
            C * x ^ b * T ^ (-(3 / 2 : ℝ)) := by
…

    Mentions: OAI.TwoPointCorrelations.MRTWeakHurwitzGrowthInput, OAI.TwoPointCorrelations.mrtZetaRieszIntegrand