OAI/NumberTheory/JointDickman/Arithmetic/SparsePrimeReciprocal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.sparse_prime_reciprocal_sampling line 14

   Source documentation

   The prime density in both the sampling matrix and its coefficient mass gives the squared-logarithm saving required for the exceptional class.

   theorem sparse_prime_reciprocal_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:ℝ)^κ →
         ∀ f : ℕ → ℂ, OneBounded f →
         (∑ t ∈ S, ‖mrtExponentialPolynomial Q (fun p => f p/(p:ℂ))
           (fun n => -Real.log (n:ℝ)) t‖^2) ≤ C/(Real.log N)^2 := by
   …