OAI/Analysis/HardSphere/Bridges/CollisionBudget.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.Bridge.mesh_collision_budget line 16
  2. def OAI.HardSphere.Bridge.torusLegHit line 63
  3. lemma OAI.HardSphere.Bridge.torusLegHit_subset line 70
  4. lemma OAI.HardSphere.Bridge.torusLegHit_sum line 90
  5. def OAI.HardSphere.Bridge.meshCount line 133
  6. lemma OAI.HardSphere.Bridge.meshCount_pos line 134
  7. lemma OAI.HardSphere.Bridge.meshCount_lower line 136
  8. lemma OAI.HardSphere.Bridge.meshCount_upper line 143
  9. lemma OAI.HardSphere.Bridge.mesh_endpoint_index line 152
  10. def OAI.HardSphere.Bridge.endpointIndex line 168
  11. lemma OAI.HardSphere.Bridge.endpointIndex_pos line 169
  12. lemma OAI.HardSphere.Bridge.endpointIndex_gap line 174
  13. lemma OAI.HardSphere.Bridge.endpointIndex_scale line 187