OAI/NumberTheory/TwoPointCorrelations/ResidueBox.lean

GitHub source file

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.

  1. lemma OAI.TwoPointCorrelations.finiteTotalVariation_product line 15

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/ResidueBox.lean:15 (same declaration text).

  2. def OAI.TwoPointCorrelations.uniformZModLaw line 44

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/ResidueBox.lean:44 (same declaration text).

  3. def OAI.TwoPointCorrelations.intervalResidueLaw line 49

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/ResidueBox.lean:49 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.intervalResidueLaw_totalVariation line 55

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/ResidueBox.lean:55 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.intervalResidueLaw_average line 62

    Source documentation

    The residue mass is the exact pushforward of uniform interval sampling.

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/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

  6. def OAI.TwoPointCorrelations.residueCubeLaw line 76

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/ResidueBox.lean:76 (same declaration text).

  7. def OAI.TwoPointCorrelations.uniformResidueCubeLaw line 82

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/ResidueBox.lean:82 (same declaration text).

  8. theorem OAI.TwoPointCorrelations.residueCube_totalVariation line 86

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/ResidueBox.lean:86 (same declaration text).

  9. 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/TwoPoint/Bounds/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