ResidueCounts.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Residue counts on arbitrary finite consecutive intervals

An interval is represented by its starting residue A and its length N. Thus this includes arbitrary translates, including intervals starting at negative integers. We prove the exact quotient-and-remainder count, the one-count discrepancy, and the total-variation estimate used by the finite residue comparison in the manuscript.

def OAI.TwoPointCorrelations.residueCount line 22
Source documentation
Number of offsets 0 ≤ j < N whose translated residue equals r.
Also declared: OAI/NumberTheory/TwoPoint/Bounds/ResidueCounts.lean:22 (same declaration text).
```
def residueCount {D : ℕ} [NeZero D] (A : ZMod D) (N : ℕ) (r : ZMod D) : ℕ :=
…
```
lemma OAI.TwoPointCorrelations.residueCount_add line 25
Also declared: OAI/NumberTheory/TwoPoint/Bounds/ResidueCounts.lean:25 (same declaration text).
lemma OAI.TwoPointCorrelations.residueCount_period line 34
Also declared: OAI/NumberTheory/TwoPoint/Bounds/ResidueCounts.lean:34 (same declaration text).
lemma OAI.TwoPointCorrelations.residueCount_multiple line 56
Also declared: OAI/NumberTheory/TwoPoint/Bounds/ResidueCounts.lean:56 (same declaration text).
lemma OAI.TwoPointCorrelations.residueCount_short line 63
Also declared: OAI/NumberTheory/TwoPoint/Bounds/ResidueCounts.lean:63 (same declaration text).
theorem OAI.TwoPointCorrelations.residueCount_exact line 88
Source documentation
Exact residue count on an arbitrary translated interval.
Also declared: OAI/NumberTheory/TwoPoint/Bounds/ResidueCounts.lean:88 (same declaration text).
```
theorem residueCount_exact {D : ℕ} [NeZero D] (A r : ZMod D) (N : ℕ) :
    residueCount A N r = N / D + if (r - A).val < N % D then 1 else 0 := by
…
```
Mentions: OAI.TwoPointCorrelations.residueCount
theorem OAI.TwoPointCorrelations.residueCount_discrepancy line 97
Source documentation
The count differs from interval length divided by modulus by at most one.
Also declared: OAI/NumberTheory/TwoPoint/Bounds/ResidueCounts.lean:97 (same declaration text).
```
theorem residueCount_discrepancy {D : ℕ} [NeZero D] (A r : ZMod D) (N : ℕ) :
    |(residueCount A N r : ℝ) - (N : ℝ) / D| ≤ 1 := by
…
```
Mentions: OAI.TwoPointCorrelations.residueCount
def OAI.TwoPointCorrelations.residueProbability line 115
Source documentation
The residue law of a uniformly selected origin from an interval.
Also declared: OAI/NumberTheory/TwoPoint/Bounds/ResidueCounts.lean:115 (same declaration text).
```
noncomputable def residueProbability {D : ℕ} [NeZero D] (A : ZMod D)
    (N : ℕ) (r : ZMod D) : ℝ := (residueCount A N r : ℝ) / N
```
Mentions: OAI.TwoPointCorrelations.residueCount
lemma OAI.TwoPointCorrelations.residueCount_sum line 118
Also declared: OAI/NumberTheory/TwoPoint/Bounds/ResidueCounts.lean:118 (same declaration text).
lemma OAI.TwoPointCorrelations.residueProbability_sum line 124
Also declared: OAI/NumberTheory/TwoPoint/Bounds/ResidueCounts.lean:124 (same declaration text).
lemma OAI.TwoPointCorrelations.residueProbability_discrepancy line 130
Also declared: OAI/NumberTheory/TwoPoint/Bounds/ResidueCounts.lean:130 (same declaration text).
def OAI.TwoPointCorrelations.residueTotalVariation line 142
Source documentation
Half the ℓ¹ difference from the uniform residue law.
Also declared: OAI/NumberTheory/TwoPoint/Bounds/ResidueCounts.lean:142 (same declaration text).
```
noncomputable def residueTotalVariation {D : ℕ} [NeZero D] (A : ZMod D) (N : ℕ) : ℝ :=
…
```
theorem OAI.TwoPointCorrelations.residueTotalVariation_le line 146
Source documentation
The stronger D/(2N) bound implies the D/N estimate used in the paper.
Also declared: OAI/NumberTheory/TwoPoint/Bounds/ResidueCounts.lean:146 (same declaration text).
```
theorem residueTotalVariation_le {D : ℕ} [NeZero D] (A : ZMod D)
    (N : ℕ) (hN : 0 < N) : residueTotalVariation A N ≤ (D : ℝ) / (2 * N) := by
…
```
Mentions: OAI.TwoPointCorrelations.residueTotalVariation