OAI/Analysis/HardSphere/Geometry/Vertex.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.HardSphere.Lattice.Vertex line 15
  2. def OAI.HardSphere.Lattice.step line 17
  3. lemma OAI.HardSphere.Lattice.step_apply_same line 19
  4. lemma OAI.HardSphere.Lattice.step_apply_ne line 21
  5. lemma OAI.HardSphere.Lattice.step_comm line 23
  6. def OAI.HardSphere.Lattice.cubicalPotential line 29
  7. lemma OAI.HardSphere.Lattice.update_step_zero line 32
  8. lemma OAI.HardSphere.Lattice.step_update_zero line 34
  9. lemma OAI.HardSphere.Lattice.update_step_other line 36
  10. theorem OAI.HardSphere.Lattice.cubicalPotential_step line 41
  11. def OAI.HardSphere.Lattice.nearestStep line 85
  12. def OAI.HardSphere.Lattice.starStep line 88
  13. lemma OAI.HardSphere.Lattice.nearestStep_symm line 90
  14. lemma OAI.HardSphere.Lattice.nearestStep_step line 93
  15. lemma OAI.HardSphere.Lattice.nearestStep_eq_step line 97
  16. def OAI.HardSphere.Lattice.withinReach line 112
  17. def OAI.HardSphere.Lattice.NNConnected line 115
  18. def OAI.HardSphere.Lattice.starConnected line 118
  19. def OAI.HardSphere.Lattice.NNComplementComponent line 121
  20. def OAI.HardSphere.Lattice.nnBoundary line 125
  21. lemma OAI.HardSphere.Lattice.boundary_of_cross line 128
  22. def OAI.HardSphere.Lattice.unitCube line 135
  23. lemma OAI.HardSphere.Lattice.unitCube_self line 137
  24. lemma OAI.HardSphere.Lattice.unitCube_step line 138
  25. lemma OAI.HardSphere.Lattice.unitCube_step_step line 143
  26. lemma OAI.HardSphere.Lattice.unitCube_star line 156
  27. def OAI.HardSphere.Lattice.edgeLabel line 163
  28. def OAI.HardSphere.Lattice.cubeFlag line 167
  29. def OAI.HardSphere.Lattice.indicatorTwo line 170
  30. lemma OAI.HardSphere.Lattice.edgeLabel_symm line 172
  31. lemma OAI.HardSphere.Lattice.edgeLabel_zero_of_same line 175
  32. lemma OAI.HardSphere.Lattice.cubeFlag_eq line 184
  33. lemma OAI.HardSphere.Lattice.edgeLabel_unitCube line 198
  34. lemma OAI.HardSphere.Lattice.edgeLabel_square line 223
  35. lemma OAI.HardSphere.Lattice.zmod_two_neg line 240
  36. lemma OAI.HardSphere.Lattice.starStep_symm line 242
  37. lemma OAI.HardSphere.Lattice.withinReach_preserves line 245
  38. lemma OAI.HardSphere.Lattice.exists_boundary_potential line 253
  39. theorem OAI.HardSphere.Lattice.nnBoundary_starConnected line 291
  40. def OAI.HardSphere.Lattice.avoidingStep line 336
  41. def OAI.HardSphere.Lattice.avoidingReach line 339
  42. def OAI.HardSphere.Lattice.exterior line 342
  43. def OAI.HardSphere.Lattice.fill line 345
  44. def OAI.HardSphere.Lattice.exteriorShell line 347
  45. def OAI.HardSphere.Lattice.coordinateBox line 350
  46. def OAI.HardSphere.Lattice.coordinateRay line 353
  47. lemma OAI.HardSphere.Lattice.coordinateRay_zero line 356
  48. lemma OAI.HardSphere.Lattice.coordinateRay_injective line 359
  49. lemma OAI.HardSphere.Lattice.coordinateRay_step line 367
  50. lemma OAI.HardSphere.Lattice.coordinateRay_reachable line 376
  51. lemma OAI.HardSphere.Lattice.coordinateRay_exterior line 383
  52. lemma OAI.HardSphere.Lattice.upper_ray_exterior line 392