OAI/Analysis/HardSphere/Geometry/StarOffsets.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.Lattice.lower_ray_exterior line 16
  2. theorem OAI.HardSphere.Lattice.fill_subset_coordinateBox line 24
  3. lemma OAI.HardSphere.Lattice.exteriorShell_good line 35
  4. def OAI.HardSphere.Lattice.starOffsets line 40
  5. lemma OAI.HardSphere.Lattice.starOffsets_card line 43
  6. lemma OAI.HardSphere.Lattice.starStep_mem_offsets line 49
  7. lemma OAI.HardSphere.Lattice.exteriorShell_subset_offsets line 61
  8. lemma OAI.HardSphere.Lattice.exteriorShell_finite line 66
  9. theorem OAI.HardSphere.Lattice.exteriorShell_card_le line 70
  10. lemma OAI.HardSphere.Lattice.withinReach_symm line 84
  11. lemma OAI.HardSphere.Lattice.withinReach_mono line 92
  12. lemma OAI.HardSphere.Lattice.nearestStep_update line 100
  13. lemma OAI.HardSphere.Lattice.withinReach_axis_le line 107
  14. lemma OAI.HardSphere.Lattice.withinReach_axis line 128
  15. def OAI.HardSphere.Lattice.intervalBox line 139
  16. def OAI.HardSphere.Lattice.mixVertex line 142
  17. lemma OAI.HardSphere.Lattice.mixVertex_zero line 144
  18. lemma OAI.HardSphere.Lattice.mixVertex_three line 145
  19. lemma OAI.HardSphere.Lattice.mixVertex_box line 148
  20. lemma OAI.HardSphere.Lattice.mixVertex_succ line 151
  21. theorem OAI.HardSphere.Lattice.intervalBox_reach line 160
  22. lemma OAI.HardSphere.Lattice.box_reach line 183
  23. lemma OAI.HardSphere.Lattice.withinReach_end line 186
  24. lemma OAI.HardSphere.Lattice.withinReach_invariant line 192
  25. lemma OAI.HardSphere.Lattice.avoidingReach_symm line 201
  26. lemma OAI.HardSphere.Lattice.exterior_of_reach line 205
  27. def OAI.HardSphere.Lattice.integerBox line 212
  28. lemma OAI.HardSphere.Lattice.mem_integerBox line 215
  29. lemma OAI.HardSphere.Lattice.finite_coordinate_bound line 218
  30. lemma OAI.HardSphere.Lattice.outside_box_reach line 227
  31. lemma OAI.HardSphere.Lattice.exterior_reach_anchor line 261
  32. theorem OAI.HardSphere.Lattice.exterior_avoidingReach line 267
  33. theorem OAI.HardSphere.Lattice.exterior_NNConnected line 273
  34. def OAI.HardSphere.Lattice.doubleVertex line 279
  35. def OAI.HardSphere.Lattice.thickCube line 281
  36. def OAI.HardSphere.Lattice.thicken line 283
  37. lemma OAI.HardSphere.Lattice.mem_thicken line 286
  38. lemma OAI.HardSphere.Lattice.double_mem_cube line 299
  39. lemma OAI.HardSphere.Lattice.thickCube_subset line 302
  40. lemma OAI.HardSphere.Lattice.thickCube_NNConnected line 305
  41. lemma OAI.HardSphere.Lattice.thicken_adjacent_centers line 315
  42. lemma OAI.HardSphere.Lattice.thicken_star_reach line 334
  43. lemma OAI.HardSphere.Lattice.thicken_NNConnected line 342
  44. def OAI.HardSphere.Lattice.complementComponent line 353
  45. lemma OAI.HardSphere.Lattice.complementComponent_spec line 356
  46. lemma OAI.HardSphere.Lattice.double_mem_thicken_iff line 367
  47. lemma OAI.HardSphere.Lattice.double_step line 381
  48. lemma OAI.HardSphere.Lattice.splitPoint_not_thicken line 390