OAI/Analysis/HardSphere/Bridges/MeshLegHit.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.Bridge.combinedSegmentHit line 13
  2. lemma OAI.HardSphere.Bridge.combined_segment_sum_bound line 18
  3. def OAI.HardSphere.Bridge.meshRemainder line 57
  4. lemma OAI.HardSphere.Bridge.meshRemainder_pos line 64
  5. lemma OAI.HardSphere.Bridge.meshStart_lt_one line 68
  6. lemma OAI.HardSphere.Bridge.mesh_suffix_time line 72
  7. lemma OAI.HardSphere.Bridge.mesh_remaining line 80
  8. lemma OAI.HardSphere.Bridge.mesh_covers line 88
  9. lemma OAI.HardSphere.Bridge.inverse_heat_antitone line 113
  10. lemma OAI.HardSphere.Bridge.inverse_heat_tail line 118
  11. def OAI.HardSphere.Bridge.meshHitUnion line 128
  12. lemma OAI.HardSphere.Bridge.mesh_hit_sum line 132