OAI/Analysis/HardSphere/Bridges/PhysicalLegCollision.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.Bridge.meshInterval_diameter line 15
  2. lemma OAI.HardSphere.Bridge.meshRemainder_early_bound line 26
  3. lemma OAI.HardSphere.Bridge.physical_leg_collision line 37
  4. lemma OAI.HardSphere.Bridge.interval_start_displacement line 88
  5. lemma OAI.HardSphere.Bridge.no_collision_endpoint_window line 105
  6. lemma OAI.HardSphere.Bridge.collision_after_window line 117
  7. lemma OAI.HardSphere.Bridge.prefix_mesh_half line 137
  8. lemma OAI.HardSphere.Bridge.prefix_mesh_regular line 143
  9. lemma OAI.HardSphere.Bridge.prefix_window_diameter line 158
  10. lemma OAI.HardSphere.Bridge.trial_initial_projection line 173
  11. lemma OAI.HardSphere.Bridge.trial_hit_first line 180
  12. lemma OAI.HardSphere.Bridge.reverse_suffix_midpoint line 210
  13. lemma OAI.HardSphere.Bridge.trialCutoff_reverse line 216
  14. lemma OAI.HardSphere.Bridge.trial_hit_cases line 250