OAI/NumberTheory/TwoPoint/ShortIntervals/MRTGeneralPrimeMean.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TwoPointCorrelations.mrt_prime_square_broad_coefficient_mass line 13

   Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTGeneralPrimeMean.lean:13 (same declaration text).

2. theorem OAI.TwoPointCorrelations.mrt_prime_square_broad_mean line 51

   Source documentation

   A prime-extraction error of size twice the square-divisor count has an absolute mean-square cost on the complete coarse window.

   Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTGeneralPrimeMean.lean:51 (same declaration text).

   theorem mrt_prime_square_broad_mean (P : Finset ℕ)
       (hP : ∀ p ∈ P, p.Prime) (b : ℕ → ℂ) {N : ℕ} (hN : 0 < N)
       (hb : ∀ n ∈ Ioc N (4 * N), ‖b n‖ ≤ 2 * mrtPrimeSquareCount P n)
       {T : ℝ} (hT : 0 < T) :
       (∫ t in -T..T, ‖mrtExponentialPolynomial (Ioc N (4 * N))
         (fun n => b n / (n : ℂ)) (fun n => -Real.log (n : ℝ)) t‖ ^ 2) ≤
         512 * Real.exp 1 * (T / (N : ℝ) + 1) *
           ((∑ p ∈ P, 1 / (p : ℝ) ^ 2) + (∑ p ∈ P, 1 / (p : ℝ) ^ 2) ^ 2) := by
   …

   Mentions: OAI.TwoPointCorrelations.mrtPrimeSquareCount, OAI.TwoPointCorrelations.mrtExponentialPolynomial