OAI/NumberTheory/TotientAsymptotic/WeightedPrimeCount.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TotientAsymptotic.weighted_endpoint_bounds line 10
2. theorem OAI.TotientAsymptotic.weighted_prime_count line 38

   Source documentation

   Ordinary PNT at two long-scale endpoints suffices, uniformly for all allowed integers A,D. The estimate remains additive for empty intervals.

   theorem weighted_prime_count (hpnt : PrimeNumberTheoremInput)
       {C ε : ℝ} (hC : 1 ≤ C) (hε : 0 < ε) :
       ∀ᶠ x : ℝ in atTop, ∀ k D A : ℕ, 1 ≤ k → 0 < D → D ≤ A →
         (A : ℝ) ≤ C*D → Real.log (D : ℝ) ≤ (Real.log x)^(4/5 : ℝ) →
         |((intervalHeads x k D A).card : ℝ)-
           (x/(D*Real.log x))*fk k ((A : ℝ)/D)| ≤ ε*(x/(D*Real.log x)) := by
   …

   Mentions: OAI.TotientAsymptotic.PrimeNumberTheoremInput, OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.intervalHeads, OAI.TotientAsymptotic.fk