ResidueBox.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Exact residue laws for one interval and three independent intervals. The box discrepancy is derived by tensoring the one-dimensional count, without estimating each individual three-dimensional residue atom.

lemma OAI.TwoPointCorrelations.finiteTotalVariation_product line 15
Also declared: OAI/NumberTheory/TwoPointCorrelations/ResidueBox.lean:15 (same declaration text).
def OAI.TwoPointCorrelations.uniformZModLaw line 44
Also declared: OAI/NumberTheory/TwoPointCorrelations/ResidueBox.lean:44 (same declaration text).
def OAI.TwoPointCorrelations.intervalResidueLaw line 49
Also declared: OAI/NumberTheory/TwoPointCorrelations/ResidueBox.lean:49 (same declaration text).
lemma OAI.TwoPointCorrelations.intervalResidueLaw_totalVariation line 55
Also declared: OAI/NumberTheory/TwoPointCorrelations/ResidueBox.lean:55 (same declaration text).
lemma OAI.TwoPointCorrelations.intervalResidueLaw_average line 62
Source documentation
The residue mass is the exact pushforward of uniform interval sampling.
Also declared: OAI/NumberTheory/TwoPointCorrelations/ResidueBox.lean:62 (same declaration text).
```
lemma intervalResidueLaw_average {D : ℕ} [NeZero D]
    (A : ZMod D) (N : ℕ) (hN : 0 < N) (f : ZMod D → ℝ) :
    (intervalResidueLaw A N hN).average f =
      (∑ j ∈ range N, f (A + (j : ZMod D))) / N := by
…
```
Mentions: OAI.TwoPointCorrelations.intervalResidueLaw
def OAI.TwoPointCorrelations.residueCubeLaw line 76
Also declared: OAI/NumberTheory/TwoPointCorrelations/ResidueBox.lean:76 (same declaration text).
def OAI.TwoPointCorrelations.uniformResidueCubeLaw line 82
Also declared: OAI/NumberTheory/TwoPointCorrelations/ResidueBox.lean:82 (same declaration text).
theorem OAI.TwoPointCorrelations.residueCube_totalVariation line 86
Also declared: OAI/NumberTheory/TwoPointCorrelations/ResidueBox.lean:86 (same declaration text).
theorem OAI.TwoPointCorrelations.residueCube_probability_discrepancy line 110
Source documentation
Any simultaneous collection of congruence conditions has the same 3D/N box error; the number of allowed residue vectors is irrelevant.
Also declared: OAI/NumberTheory/TwoPointCorrelations/ResidueBox.lean:110 (same declaration text).
```
theorem residueCube_probability_discrepancy {D : ℕ} [NeZero D]
    (A : ZMod D × ZMod D × ZMod D) (N : ℕ) (hN : 0 < N)
    (E : (ZMod D × ZMod D × ZMod D) → Prop) :
    |(residueCubeLaw A N hN).probability E - (uniformResidueCubeLaw D).probability E| ≤
      3 * D / (N : ℝ) := by
…
```
Mentions: OAI.TwoPointCorrelations.residueCubeLaw, OAI.TwoPointCorrelations.uniformResidueCubeLaw