MRTPrimeMoments.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

High even moments of a prime Dirichlet polynomial. Expanding the power produces ordered prime tuples; unique factorization bounds each coefficient fiber by the factorial, and the ordinary mean-square theorem then applies to a polynomial of length N ^ r.

def OAI.TwoPointCorrelations.mrtPrimePowerCoefficient line 15
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTPrimeMoments.lean:15 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_prime_tuple_range line 20
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTPrimeMoments.lean:20 (same declaration text).
theorem OAI.TwoPointCorrelations.mrt_prime_power_coefficient_mass line 30
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTPrimeMoments.lean:30 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_prime_tuple_phase line 53
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTPrimeMoments.lean:53 (same declaration text).
theorem OAI.TwoPointCorrelations.mrt_prime_polynomial_power line 66
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTPrimeMoments.lean:66 (same declaration text).

theorem OAI.TwoPointCorrelations.mrt_prime_polynomial_moment line 103

Source documentation

The prime-polynomial high-moment bound with an absolute constant. Repeated prime factors are included; their only cost is r!.

Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTPrimeMoments.lean:103 (same declaration text).

theorem mrt_prime_polynomial_moment (P : Finset ℕ) (a : ℕ → ℂ)
    (N r : ℕ) (hP : ∀ p ∈ P, p.Prime) (hN : ∀ p ∈ P, p ≤ N)
    {T : ℝ} (hT : 0 < T) :
    (∫ t in -T..T, ‖mrtExponentialPolynomial P a (fun p => -Real.log (p : ℝ)) t‖ ^
      (2 * r)) ≤
      8 * Real.exp 1 * (T + (N ^ r : ℕ)) *
        (r.factorial : ℝ) * (∑ p ∈ P, ‖a p‖ ^ 2) ^ r := by
…

Mentions: OAI.TwoPointCorrelations.mrtExponentialPolynomial