PrimaryPrimePNTProofAP.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The natural prime density of the split rational residue class.

The von Mangoldt input is derived from the Wiener--Ikehara theorem and Mathlib's residue-class continuation.

theorem OAI.CubicFirstMoment.rationalProgressionCount_one_limit line 14
Source documentation
The class 1 mod 3 has natural prime density one half.
```
theorem rationalProgressionCount_one_limit :
    Tendsto (fun X => rationalProgressionCount 1 X * Real.log X / X)
      atTop (𝓝 (1/2)) := by
…
```
Mentions: OAI.CubicFirstMoment.rationalProgressionCount