OAI/NumberTheory/CubicMoment/Estimates/PrimaryPrimePNTProofTheta.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Prime-power removal for the mod-three von Mangoldt mean.

  1. def OAI.CubicFirstMoment.rationalProgressionPrimes line 13

    Source documentation

    Rational primes in one residue class, with the literal real cutoff.

    def rationalProgressionPrimes (a : ℕ) (X : ℝ) : Finset ℕ :=
…
  2. def OAI.CubicFirstMoment.rationalProgressionCount line 16
  3. def OAI.CubicFirstMoment.rationalProgressionTheta line 19
  4. def OAI.CubicFirstMoment.modThreePsi line 22
  5. theorem OAI.CubicFirstMoment.modThreePsi_limit line 25
  6. lemma OAI.CubicFirstMoment.rationalProgression_primePower_gap line 40
  7. lemma OAI.CubicFirstMoment.sqrt_log_div_tendsto_zero line 78
  8. theorem OAI.CubicFirstMoment.rationalProgressionTheta_limit line 91