UniformResidues.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform residue coordinates realized on one common finite carrier.

def OAI.TwoPointCorrelations.uniformResidueLaw line 14
Source documentation
A uniform residue modulo p, embedded into Fin B. The zero-weight padding allows different prime moduli to share the same sample type.
```
noncomputable def uniformResidueLaw (B p : ℕ) (hp : 0 < p) (hpB : p ≤ B) :
    FiniteLaw (Fin B) where
…
```
Mentions: OAI.TwoPointCorrelations.FiniteLaw
lemma OAI.TwoPointCorrelations.uniformResidueLaw_weight line 22
lemma OAI.TwoPointCorrelations.uniformResidueLaw_support line 27
lemma OAI.TwoPointCorrelations.uniformResidueLaw_castLE line 32
lemma OAI.TwoPointCorrelations.uniformResidueLaw_independent_support line 40
Source documentation
Every actual residue assignment with nonzero product mass lies below its coordinate's modulus. This applies to the very same sample used for the mixed-difference identity.
```
lemma uniformResidueLaw_independent_support {ι : Type*} [Fintype ι] [DecidableEq ι]
    (B : ℕ) (p : ι → ℕ) (hp : ∀ i, 0 < p i) (hpB : ∀ i, p i ≤ B)
    (x : ι → Fin B) :
    (FiniteLaw.independent (fun i => uniformResidueLaw B (p i) (hp i) (hpB i))).weight x ≠ 0 ↔
      ∀ i, (x i).val < p i := by
…
```
Mentions: OAI.TwoPointCorrelations.FiniteLaw.independent, OAI.TwoPointCorrelations.uniformResidueLaw