OAI/Probability/LatticeSurface/Coercivity/SparseGeometry.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SparseBlocks.sites line 203
2. lemma OAI.SparseBlocks.mem_sites line 207
3. lemma OAI.SparseBlocks.mem_enlarged line 213
4. def OAI.SparseBlocks.origin line 216
5. def OAI.SparseBlocks.translate line 218
6. lemma OAI.SparseBlocks.translate_injective line 221
7. lemma OAI.SparseBlocks.translate_mem line 225
8. lemma OAI.SparseBlocks.translate_surj line 233
9. lemma OAI.SparseBlocks.translate_adj line 244
10. lemma OAI.SparseBlocks.translate_dist line 249
11. lemma OAI.SparseBlocks.card_sites line 255
12. lemma OAI.SparseBlocks.sites_disjoint line 262
13. lemma OAI.SparseBlocks.L_pos line 284
14. lemma OAI.SparseBlocks.block_subset_sites line 290
15. lemma OAI.SparseBlocks.face_neighbor_sites line 301