HalaszSparseSmallPrimes.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The small-prime range of the published sparse estimate follows from Chebyshev and finite weighted Gram duality. Only larger log Y requires the oscillatory prime estimate.

lemma OAI.TwoPointCorrelations.halasz_dyadic_prime_log_mass line 14
theorem OAI.TwoPointCorrelations.halasz_sparse_prime_card_bound line 27
lemma OAI.TwoPointCorrelations.halasz_sparse_small_scale line 59

theorem OAI.TwoPointCorrelations.halasz_sparse_small_primes line 75

Source documentation

This is the exact sparse-input inequality in the small log Y range.

theorem halasz_sparse_small_primes {L Y : ℝ} (hL : 1 ≤ L) (hY : 2 ≤ Y)
    (hscale : Real.log Y ≤ 2*L^(3/4:ℝ)*Real.log L)
    (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime ∧ Y ≤ (p:ℝ) ∧ (p:ℝ) ≤ 2*Y)
    (a : ℕ → ℂ) (S : Finset ℝ)
    (hsep : ∀ t ∈ S, ∀ s ∈ S, t≠s → 1 ≤ |t-s|) :
    (∑ t ∈ S, ‖mrtExponentialPolynomial P a (fun p => -Real.log (p:ℝ)) t‖^2) ≤
      (2*Real.log 4)*(Y+(S.card:ℝ)*Y*Real.exp (-Real.log Y/L^(3/4:ℝ))*L^2)*
        ∑ p ∈ P, ‖a p‖^2/Real.log (p:ℝ) := by
…

Mentions: OAI.TwoPointCorrelations.mrtExponentialPolynomial