OAI/Analysis/HardSphere/Allocation/PhysicalRouteFactors.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.Groups.pointAsPath line 15
  2. lemma OAI.HardSphere.Groups.pointAsPath_measurable line 17
  3. lemma OAI.HardSphere.Groups.pointAsPath_apply line 21
  4. def OAI.HardSphere.Groups.cellPathReference line 23
  5. instance OAI.HardSphere.Groups.cellPathReference_probability line 26
  6. def OAI.HardSphere.Groups.routeDensityBound line 35
  7. lemma OAI.HardSphere.Groups.vertex_le_routeDensity line 37
  8. lemma OAI.HardSphere.Groups.endpoint_le_routeDensity line 38
  9. def OAI.HardSphere.Groups.encodeFirstEndpoint line 44
  10. def OAI.HardSphere.Groups.encodeLastEndpoint line 46
  11. lemma OAI.HardSphere.Groups.encodeFirstEndpoint_measurable line 48
  12. lemma OAI.HardSphere.Groups.encodeLastEndpoint_measurable line 50
  13. lemma OAI.HardSphere.Groups.encoded_endpoint_physical line 53
  14. def OAI.HardSphere.Groups.physicalRouteFactor line 102
  15. instance OAI.HardSphere.Groups.physicalRouteFactor_finite line 116
  16. def OAI.HardSphere.Groups.routeFirstReference line 124
  17. def OAI.HardSphere.Groups.routeSecondReference line 131
  18. theorem OAI.HardSphere.Groups.physicalRouteFactor_physical line 138