OAI/NumberTheory/CubicMoment/Estimates/PrimaryPrimePNTProof.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The primary-prime PNT, from rational progressions and actual Eisenstein splitting.

  1. lemma OAI.CubicFirstMoment.sqrt_log_remainder_tendsto_zero line 12
  2. theorem OAI.CubicFirstMoment.primaryPrimePNT_proved line 26

    Source documentation

    The ordinary prime-ideal theorem in exactly the normalization used by the mains. No prime-distribution or splitting hypothesis remains.

    theorem primaryPrimePNT_proved : PrimaryPrimePNT := by
…

    Mentions: OAI.CubicFirstMoment.PrimaryPrimePNT