OAI/NumberTheory/TotientAsymptotic/LowerPrimeCutoff.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The lower bound on the largest prime has negligible cost in every actual fiber.

  1. def OAI.TotientAsymptotic.headCutoffLoss line 13
  2. lemma OAI.TotientAsymptotic.headCutoffLoss_tendsto line 16
  3. lemma OAI.TotientAsymptotic.lower_prime_cutoff_negligible line 52
  4. theorem OAI.TotientAsymptotic.shifted_prime_uniform_asymptotic line 75

    Source documentation

    Complete largest-prime asymptotic, with the manuscript's lower cutoff.

    theorem shifted_prime_uniform_asymptotic (hpnt : PrimeNumberTheoremInput)
    {a : ℝ} (ha : 0 < a) {ε : ℝ} (hε : 0 < ε) :
    ∀ᶠ x : ℝ in atTop, ∀ D : ℕ, 0 < D →
      Real.log (D : ℝ) ≤ (Real.log x)^(4/5 : ℝ) → ∀ t : ℝ, a*x ≤ t → t ≤ x →
      |((shiftedPrimeSet x t D).card : ℝ)-t/(D*Real.log x)| ≤ ε*(t/(D*Real.log x)) := by
…

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