OAI/Probability/LatticeSurface/Coercivity/HoleEdges.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SparseHoles.Edge line 23
  2. def OAI.SparseHoles.neighbors line 25
  3. lemma OAI.SparseHoles.mem_neighbors line 28
  4. lemma OAI.SparseHoles.neighbors_card line 40
  5. def OAI.SparseHoles.edgesAt line 45
  6. lemma OAI.SparseHoles.edgesAt_card line 49
  7. lemma OAI.SparseHoles.edgeAt_self line 52
  8. lemma OAI.SparseHoles.mem_edgesAt line 56
  9. def OAI.SparseHoles.incidentEdges line 72
  10. lemma OAI.SparseHoles.mem_incidentEdges line 76
  11. lemma OAI.SparseHoles.incidentEdges_card line 82
  12. def OAI.SparseHoles.rimFin line 89
  13. lemma OAI.SparseHoles.coe_rimFin line 91
  14. lemma OAI.SparseHoles.mem_rimFin line 94
  15. def OAI.SparseHoles.rimEdges line 98
  16. lemma OAI.SparseHoles.mem_rimEdges line 102
  17. lemma OAI.SparseHoles.rim_walk_edges line 112
  18. def OAI.SparseHoles.edgeAbs line 120
  19. lemma OAI.SparseHoles.edgeAbs_mk line 123
  20. lemma OAI.SparseHoles.edgeAbs_nonneg line 125
  21. lemma OAI.SparseHoles.walk_telescope line 129
  22. lemma OAI.SparseHoles.path_power line 142
  23. lemma OAI.SparseHoles.rim_power line 157