OAI/Probability/ClassicalON/CoarsePaths.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClassicalON.LatticeGraph.cellVisited line 9
2. def OAI.ClassicalON.LatticeGraph.coarseCluster line 12
3. theorem OAI.ClassicalON.LatticeGraph.fine_edge_radius line 17
4. theorem OAI.ClassicalON.LatticeGraph.coarse_reachable_of_walk line 25
5. theorem OAI.ClassicalON.LatticeGraph.coarse_walk_visited line 40
6. theorem OAI.ClassicalON.LatticeGraph.coarse_walk_radius line 50
7. theorem OAI.ClassicalON.LatticeGraph.connected_has_coarse_code line 59
8. theorem OAI.ClassicalON.LatticeGraph.connected_code_crossings line 89