OAI/Probability/LatticeSurface/Coercivity/HoleGeometry.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SparseHoles.Vertex line 20
  2. def OAI.SparseHoles.grid line 22
  3. def OAI.SparseHoles.rim line 31
  4. lemma OAI.SparseHoles.abs_small line 34
  5. lemma OAI.SparseHoles.adj_cases line 38
  6. lemma OAI.SparseHoles.adj_right line 53
  7. lemma OAI.SparseHoles.adj_up line 57
  8. def OAI.SparseHoles.label line 61
  9. lemma OAI.SparseHoles.label_symm line 66
  10. lemma OAI.SparseHoles.label_same line 69
  11. lemma OAI.SparseHoles.square_rim line 80
  12. lemma OAI.SparseHoles.label_closed line 91
  13. lemma OAI.SparseHoles.label_potential line 123
  14. lemma OAI.SparseHoles.boundary_in_set line 168
  15. lemma OAI.SparseHoles.constant_of_connected line 193
  16. lemma OAI.SparseHoles.subcut_complete line 200
  17. lemma OAI.SparseHoles.rim_preconnected line 233
  18. def OAI.SparseHoles.offsets8 line 263
  19. lemma OAI.SparseHoles.offsets8_card line 266
  20. lemma OAI.SparseHoles.rim_finite_bound line 268
  21. theorem OAI.SparseHoles.rim_paths line 299