OAI/Analysis/HardSphere/Allocation/CoarsePhysical.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.Comparison.coarse_joint_reference line 14
  2. def OAI.HardSphere.Groups.physicalBranchDatum line 41
  3. lemma OAI.HardSphere.Groups.frozenPaths_joint_measurable line 48
  4. lemma OAI.HardSphere.Groups.physicalBranchDatum_measurable line 61
  5. lemma OAI.HardSphere.Groups.datumPermitted_branch line 78
  6. def OAI.HardSphere.Groups.datumIndividualReference line 103
  7. instance OAI.HardSphere.Groups.datumIndividualReference_finite line 110
  8. lemma OAI.HardSphere.Groups.datumIndividualReference_apply line 115
  9. def OAI.HardSphere.Groups.datumGroupReference line 123
  10. instance OAI.HardSphere.Groups.datumGroupReference_finite line 131
  11. lemma OAI.HardSphere.Groups.datumGroupReference_apply line 137
  12. def OAI.HardSphere.Groups.projectGroup line 156
  13. lemma OAI.HardSphere.Groups.projectGroup_measurable line 158
  14. def OAI.HardSphere.Groups.selectedPhysicalPath line 162
  15. lemma OAI.HardSphere.Groups.selectedPhysicalPath_measurable line 166
  16. lemma OAI.HardSphere.Groups.selectedPhysicalPath_apply line 173
  17. def OAI.HardSphere.Groups.datumPhysicalReference line 181
  18. instance OAI.HardSphere.Groups.datumPhysicalReference_finite line 186
  19. theorem OAI.HardSphere.Groups.actual_allocated_physical_coarse_fiber line 193