OAI/Probability/CriticalZ3/BoxGeometry.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.CriticalZ3.Box line 13
2. theorem OAI.CriticalZ3.Box.ext line 20
3. def OAI.CriticalZ3.Box.vertices line 23
4. def OAI.CriticalZ3.Box.Contains line 25
5. theorem OAI.CriticalZ3.Box.mem_vertices line 27
6. def OAI.CriticalZ3.Box.bonds line 31
7. theorem OAI.CriticalZ3.Box.mem_bonds line 34
8. def OAI.CriticalZ3.Box.expand line 38
9. def OAI.CriticalZ3.Box.cube line 46
10. theorem OAI.CriticalZ3.Box.contains_cube line 51
11. theorem OAI.CriticalZ3.Box.contains_expand line 56
12. theorem OAI.CriticalZ3.Box.expand_mono line 63
13. theorem OAI.CriticalZ3.Box.expand_expand line 71
14. theorem OAI.CriticalZ3.Box.neighbor_coordinates line 74
15. theorem OAI.CriticalZ3.Box.neighbor_distance line 86
16. theorem OAI.CriticalZ3.Box.neighbor_in_expand line 93
17. theorem OAI.CriticalZ3.Box.exterior_neighbor_unique line 103

    Source documentation

    The uniqueness used by the shell-closing argument, including corners.

    theorem exterior_neighbor_unique (B : Box) {y z z' : Vertex}
        (hy : ¬ B.Contains y) (hz : B.Contains z) (hz' : B.Contains z')
        (hyz : NearestNeighbor y z) (hyz' : NearestNeighbor y z') : z = z' := by
    …

    Mentions: OAI.CriticalZ3.Box, OAI.CriticalZ3.Vertex, OAI.CriticalZ3.NearestNeighbor

18. def OAI.CriticalZ3.Box.seedCenter line 132
19. theorem OAI.CriticalZ3.Box.seedCenter_bounds line 135
20. theorem OAI.CriticalZ3.Box.seed_contained line 140
21. theorem OAI.CriticalZ3.Box.seed_contains_entry line 149
22. theorem OAI.CriticalZ3.Box.seed_center_near line 160
23. theorem OAI.CriticalZ3.Box.expanded_seed_width line 169
24. theorem OAI.CriticalZ3.Box.card_cube line 176

    Source documentation

    The exact number of candidates excluded in one greedy selection.

    theorem card_cube (c : Vertex) (m : ℕ) : (cube c m).vertices.card = (2*m+1)^3 := by
    …

    Mentions: OAI.CriticalZ3.Vertex, OAI.CriticalZ3.Box.cube

25. theorem OAI.CriticalZ3.Box.disjoint_seeds line 184
26. theorem OAI.CriticalZ3.Box.separated_subset line 196
27. theorem OAI.CriticalZ3.Box.separated_centers line 249
28. def OAI.CriticalZ3.Box.translateVertex line 264
29. def OAI.CriticalZ3.Box.translateBond line 266
30. theorem OAI.CriticalZ3.Box.translateVertex_injective line 268
31. theorem OAI.CriticalZ3.Box.translateBond_injective line 275
32. theorem OAI.CriticalZ3.Box.step_translate line 281
33. theorem OAI.CriticalZ3.Box.cube_contains_translate line 287
34. theorem OAI.CriticalZ3.Box.cube_vertices_translate line 291
35. theorem OAI.CriticalZ3.Box.cube_bonds_translate line 304
36. theorem OAI.CriticalZ3.Box.cube_bonds_card line 321
37. def OAI.CriticalZ3.Box.Within line 325
38. theorem OAI.CriticalZ3.Box.within_symm line 328
39. theorem OAI.CriticalZ3.Box.within_path_symm line 332
40. theorem OAI.CriticalZ3.Box.line_step line 338
41. theorem OAI.CriticalZ3.Box.line_contains line 345
42. theorem OAI.CriticalZ3.Box.line_path_le line 352
43. theorem OAI.CriticalZ3.Box.line_path line 367
44. theorem OAI.CriticalZ3.Box.connected line 377

    Source documentation

    Every nonempty integer rectangle is nearest-neighbor connected internally.

    theorem connected (B : Box) {x y : Vertex} (hx : B.Contains x) (hy : B.Contains y) :
        Relation.ReflTransGen B.Within x y := by
    …

    Mentions: OAI.CriticalZ3.Box, OAI.CriticalZ3.Vertex