OAI/Probability/LatticeSurface/Coercivity/SparseColor.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SparseBlocks.Vertex line 9
2. def OAI.SparseBlocks.residue line 20
3. def OAI.SparseBlocks.color line 27
4. lemma OAI.SparseBlocks.residue_eq_dvd line 30
5. lemma OAI.SparseBlocks.color_distance line 39
6. def OAI.SparseBlocks.offsets line 51
7. lemma OAI.SparseBlocks.offsets_mem line 54
8. lemma OAI.SparseBlocks.offsets_card line 57
9. lemma OAI.SparseBlocks.perturbed_color_distance line 62