PrimaryPrimePNTProofCounting.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Finite counting comparison with split rational primes.

lemma OAI.CubicFirstMoment.primaryPrime_primeNorm_count line 12
Source documentation
Prime-norm primary elements account for exactly twice the split rational count.
```
lemma primaryPrime_primeNorm_count (X : ℝ) (hX : 0 ≤ X) :
    ((primeCutoff X).filter (fun z => (normNat z).Prime)).card =
      2 * ((Nat.primesLE ⌊X⌋₊).filter (fun p => p % 3 = 1)).card := by
…
```
Mentions: OAI.CubicFirstMoment.primeCutoff, OAI.CubicFirstMoment.normNat
lemma OAI.CubicFirstMoment.primaryPrime_squareNorm_count_le line 46
Source documentation
The remaining primary primes have square norm and contribute at most a square-root error.
```
lemma primaryPrime_squareNorm_count_le (X : ℝ) (hX : 0 ≤ X) :
    ((primeCutoff X).filter (fun z => ¬(normNat z).Prime)).card ≤
      2 * (Nat.sqrt ⌊X⌋₊ + 1) := by
…
```
Mentions: OAI.CubicFirstMoment.primeCutoff, OAI.CubicFirstMoment.normNat
theorem OAI.CubicFirstMoment.primaryPrimeCount_comparison line 76
Source documentation
Literal count comparison; no prime ideal theorem is assumed.
```
theorem primaryPrimeCount_comparison (X : ℝ) (hX : 0 ≤ X) :
    let P := ((Nat.primesLE ⌊X⌋₊).filter (fun p => p % 3 = 1)).card
…
```