OAI/NumberTheory/JointDickman/Analysis/MellinRealScale.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.floor_rpow_eventually_lower line 10
2. lemma OAI.JointDickman.mellin_real_scale_eventually line 24
3. theorem OAI.JointDickman.sparse_prime_reciprocal_real line 50

   Source documentation

   Arbitrary sufficiently large real prime lengths are allowed; the integer auxiliary scale is no longer visible to applications.

   theorem sparse_prime_reciprocal_real (B : ℝ) (hB : 1 ≤ B) :
       ∃ C γ : ℝ, 0 < C ∧ 0 < γ ∧
         ∀ᶠ N : ℝ in atTop, ∀ (Q : Finset ℕ) (S : Finset ℝ),
         (∀ p ∈ Q, p.Prime ∧ N ≤ (p:ℝ) ∧ (p:ℝ) ≤ 2*N) →
         (∀ x ∈ S, ∀ y ∈ S, x ≠ y → 1 ≤ |x-y|) →
         (∀ x ∈ S, ∀ y ∈ S, |x-y| ≤ N^B) →
         (S.card:ℝ) ≤ N^γ →
         ∀ 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
   …