OAI/Analysis/HardSphere/Allocation/PhysicalMixedObservation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.Groups.physicalCodeTag line 18
  2. def OAI.HardSphere.Groups.taggedPhysicalBathKernel line 24
  3. instance OAI.HardSphere.Groups.taggedPhysicalBathKernel_markov line 30
  4. def OAI.HardSphere.Groups.physicalCodeObserver line 34
  5. instance OAI.HardSphere.Groups.physicalCodeObserver_markov line 44
  6. theorem OAI.HardSphere.Groups.physicalCodedRoute_same_observed line 49
  7. lemma OAI.HardSphere.Groups.unitTarget_project line 90
  8. lemma OAI.HardSphere.Groups.cellPathReference_support line 104
  9. lemma OAI.HardSphere.Groups.physicalPrimary_extra line 115
  10. def OAI.HardSphere.Groups.physicalTagEvent line 130
  11. lemma OAI.HardSphere.Groups.physicalTagEvent_measurable line 134
  12. theorem OAI.HardSphere.Groups.physicalCodedRoute_tag_support line 140