OAI/NumberTheory/CubicMoment/Estimates/PrimaryPrimePNTProofMangoldt.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The mod-three prime progression input, from the proved Wiener--Ikehara theorem and Mathlib's unconditional residue-class von Mangoldt continuation.

  1. theorem OAI.CubicFirstMoment.modThree_mangoldt_mean line 13

    Source documentation

    The required progression PNT at the von Mangoldt level.

    theorem modThree_mangoldt_mean (a : ZMod 3) (ha : IsUnit a) :
    Tendsto (fun N : ℕ => cumsum (vonMangoldt.residueClass a) N / N)
      atTop (𝓝 (1/2 : ℝ)) := by
…