OAI/NumberTheory/JointDickman/Arithmetic/PrimePresenceBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.prime_presence_coefficient_mass line 11
2. lemma OAI.JointDickman.prime_presence_coefficient_bound line 32
3. lemma OAI.JointDickman.power_phase_divisor_bound line 45
4. theorem OAI.JointDickman.primePresence_phase_bound line 73

   Source documentation

   A finite, uniform oscillatory estimate. Its inputs are the literal prime set and the cardinality bound for products below the cutoff.

   theorem primePresence_phase_bound (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
       (z : ℕ → ℂ) (hz : ∀ p ∈ P, ‖z p‖ ≤ 1) (t : ℝ) (N J : ℕ)
       {Y : ℝ} (hY : 0 ≤ Y)
       (hcard : ∀ D ∈ boundedPrimeSubsets P N, D.card ≤ J) :
       ‖halaszPhaseMean (primePresence P z) t N‖ ≤
         (2*(N:ℝ)/(1+|t|)+9*(1+|t|)*Y)*Real.exp (2*∑ p ∈ P, 1/(p:ℝ)) +
           (N:ℝ)*2^J*primeSubsetTail P Y N := by
   …

   Mentions: OAI.JointDickman.boundedPrimeSubsets, OAI.JointDickman.primePresence, OAI.JointDickman.primeSubsetTail