ModFivePrimes.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

The fixed modulus-five prime-number input used by the manuscript.

Published source: D. Koukoulopoulos, The Distribution of Prime Numbers, AMS, 2019, Theorem 12.1 (Siegel--Walfisz), with modulus 5 fixed. That theorem is stated for the prime-counting function. ModFiveThetaInput is its standard partial-summation consequence for the logarithmically weighted prime count, specialized to the two selections needed here. The complementary selection includes the single prime 5, which changes the error by a bounded amount. Source: https://dms.umontreal.ca/~koukoulo/documents/publications/primes.pdf

No primes depending on the application are deleted in this published input. Removing a finite exceptional prime set has an explicit bounded cost.

def OAI.TwoPointCorrelations.ModFivePrime line 25
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePrimes.lean:25 (same declaration text).
def OAI.TwoPointCorrelations.modFiveDensity line 28
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePrimes.lean:28 (same declaration text).
def OAI.TwoPointCorrelations.modFivePrimesUpTo line 30
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePrimes.lean:30 (same declaration text).
def OAI.TwoPointCorrelations.modFiveLogWeight line 33
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePrimes.lean:33 (same declaration text).
def OAI.TwoPointCorrelations.modFiveTheta line 36
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePrimes.lean:36 (same declaration text).
def OAI.TwoPointCorrelations.deletedModFivePrimes line 39
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePrimes.lean:39 (same declaration text).
def OAI.TwoPointCorrelations.deletedModFiveTheta line 42
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePrimes.lean:42 (same declaration text).
def OAI.TwoPointCorrelations.ModFiveThetaInput line 47
Source documentation
The precise published input: a fixed-modulus consequence of Koukoulopoulos, Theorem 12.1, before any application-dependent exclusions.
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePrimes.lean:47 (same declaration text).
```
def ModFiveThetaInput : Prop :=
…
```
lemma OAI.TwoPointCorrelations.modFiveTheta_eq_sum line 52
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePrimes.lean:52 (same declaration text).
lemma OAI.TwoPointCorrelations.modFivePrimesUpTo_prime line 56
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePrimes.lean:56 (same declaration text).
lemma OAI.TwoPointCorrelations.modFivePrimesUpTo_le line 60
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePrimes.lean:60 (same declaration text).
lemma OAI.TwoPointCorrelations.modFivePrimesUpTo_mono line 64
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePrimes.lean:64 (same declaration text).
lemma OAI.TwoPointCorrelations.modFivePrimesUpTo_disjoint line 71
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePrimes.lean:71 (same declaration text).
lemma OAI.TwoPointCorrelations.log_nat_nonneg line 81
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePrimes.lean:81 (same declaration text).
lemma OAI.TwoPointCorrelations.deletedModFiveTheta_error line 87
Source documentation
The entire cost of removing a finite exceptional prime set is explicit.
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePrimes.lean:87 (same declaration text).
```
lemma deletedModFiveTheta_error (E : Finset ℕ) (one : Bool) (x : ℝ) :
    |deletedModFiveTheta E one x - modFiveTheta one x| ≤
      ∑ p ∈ E, Real.log p := by
…
```
Mentions: OAI.TwoPointCorrelations.deletedModFiveTheta, OAI.TwoPointCorrelations.modFiveTheta
theorem OAI.TwoPointCorrelations.ModFiveThetaInput.deleted_error line 102
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePrimes.lean:102 (same declaration text).