OAI/NumberTheory/TotientAsymptotic/PrimeInterval.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TotientAsymptotic.primeInterval line 10
2. lemma OAI.TotientAsymptotic.primeInterval_card line 13
3. lemma OAI.TotientAsymptotic.prime_interval_uniform line 30

   Source documentation

   Counts may vanish: the positive part is encoded by min(l,u), so no relative estimate for a short or empty prime interval is assumed.

   lemma prime_interval_uniform (hpnt : PrimeNumberTheoremInput)
       {a b ε : ℝ} (ha : 0 < a) (hb : 0 < b) (hε : 0 < ε) :
       ∀ᶠ x : ℝ in atTop, ∀ D l u : ℝ, 1 ≤ D →
         Real.log D ≤ (Real.log x)^(4/5 : ℝ) →
         a*x/D ≤ l → a*x/D ≤ u → u ≤ b*x/D →
         |((primeInterval l u).card : ℝ)-(u-min l u)/Real.log x| ≤
           ε*x/(D*Real.log x) := by
   …

   Mentions: OAI.TotientAsymptotic.PrimeNumberTheoremInput, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.primeInterval