OAI/Probability/LatticeSurface/Coercivity/SparseAmbient.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SparseBlocks.steps line 180
2. lemma OAI.SparseBlocks.steps_card line 182
3. lemma OAI.SparseBlocks.adj_iff_steps line 184
4. lemma OAI.SparseBlocks.finiteGraph_degree line 190
5. lemma OAI.SparseBlocks.adj_sub line 199
6. def OAI.SparseBlocks.largeBox line 203
7. lemma OAI.SparseBlocks.largeBox_mem line 206
8. def OAI.SparseBlocks.boxHom line 211
9. lemma OAI.SparseBlocks.boxHom_surj line 221
10. lemma OAI.SparseBlocks.largeBox_connected line 229
11. lemma OAI.SparseBlocks.exists_ambient line 232