SparsePrimeMellin.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Sparse prime Mellin sampling in polynomial frequency ranges

theorem OAI.JointDickman.sparse_prime_mellin_sampling line 12

Source documentation

An unconditional prime-density sampling bound. The sparse sample exponent may depend on the fixed polynomial frequency range.

theorem sparse_prime_mellin_sampling (B : ℝ) (hB : 1 ≤ B) :
    ∃ C κ : ℝ, 0 < C ∧ 0 < κ ∧
      ∀ᶠ q : ℕ in atTop, ∀ (N : ℝ) (Q : Finset ℕ) (S : Finset ℝ),
      (q:ℝ)^10 ≤ N → N ≤ (q:ℝ)^11 →
      (∀ p ∈ Q, p.Prime ∧ N ≤ (p:ℝ) ∧ (p:ℝ) ≤ 2*N) →
      (∀ x ∈ S, ∀ y ∈ S, x ≠ y → 1 ≤ |x-y|) →
      (∀ x ∈ S, ∀ y ∈ S, |x-y| ≤ (q:ℝ)^B) →
      (S.card:ℝ) ≤ (q:ℝ)^κ →
      ∀ a : ℕ → ℂ,
      (∑ t ∈ S, ‖mrtExponentialPolynomial Q a (fun n => -Real.log (n:ℝ)) t‖^2) ≤
        C*N/Real.log N * ∑ p ∈ Q, ‖a p‖^2 := by
…