OAI/Analysis/HardSphere/Bridges/PairSubtype.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.Bridge.pairedPathsRaw line 17
  2. lemma OAI.HardSphere.Bridge.pairedPathsRaw_fst line 22
  3. lemma OAI.HardSphere.Bridge.pairedPathsRaw_snd line 27
  4. def OAI.HardSphere.Bridge.pairedPathsOn line 33
  5. lemma OAI.HardSphere.Bridge.pairedPathsOn_physical line 37
  6. lemma OAI.HardSphere.Bridge.pairedPathsOn_auxiliary line 71
  7. def OAI.HardSphere.Bridge.pointPathRaw line 106
  8. lemma OAI.HardSphere.Bridge.pointPathRaw_fst line 110
  9. lemma OAI.HardSphere.Bridge.pointPathRaw_probability line 130
  10. lemma OAI.HardSphere.Bridge.pointPathRaw_midpoint line 139
  11. lemma OAI.HardSphere.Bridge.targetUniform_le_cell line 148
  12. def OAI.HardSphere.Bridge.pointPathOn line 155
  13. lemma OAI.HardSphere.Bridge.pointPathOn_physical line 159