OAI/Analysis/HardSphere/Allocation/NearLift.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.Groups.nearestLift_eq_of_near line 16
  2. lemma OAI.HardSphere.Groups.near_lift_unique line 27
  3. theorem OAI.HardSphere.Groups.canonical_certificate_useful_list line 34
  4. lemma OAI.HardSphere.Groups.labelStartLift_project line 107
  5. lemma OAI.HardSphere.Groups.labelEndLift_project line 111
  6. lemma OAI.HardSphere.Groups.exposed_selected_near line 121
  7. def OAI.HardSphere.Groups.canonicalShift line 154
  8. lemma OAI.HardSphere.Groups.canonicalShift_period line 158
  9. lemma OAI.HardSphere.Groups.canonicalShift_anchor line 165
  10. lemma OAI.HardSphere.Groups.canonicalShift_start line 171
  11. lemma OAI.HardSphere.Groups.canonicalShift_end line 182
  12. lemma OAI.HardSphere.Groups.physicalMutual_shift_preimage line 193
  13. lemma OAI.HardSphere.Groups.canonical_reference_transport line 205
  14. theorem OAI.HardSphere.Groups.actual_allocated_canonical_reference line 247