OAI/Analysis/HardSphere/Geometry/KilledObservable.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.killedObservable line 19
  2. lemma OAI.HardSphere.killedObservable_measurable line 23
  3. lemma OAI.HardSphere.killedObservable_bound line 29
  4. def OAI.HardSphere.killedAverage line 36
  5. lemma OAI.HardSphere.killedAverage_measurable line 40
  6. lemma OAI.HardSphere.killedAverage_bound line 46
  7. lemma OAI.HardSphere.killedAverage_memLp line 54
  8. lemma OAI.HardSphere.integrable_killedAverage_pairing line 61
  9. lemma OAI.HardSphere.killedTransition_bounded_pairing line 76
  10. lemma OAI.HardSphere.killedTransition_bounded line 108
  11. def OAI.HardSphere.splitObservable line 131
  12. lemma OAI.HardSphere.splitObservable_measurable line 136
  13. lemma OAI.HardSphere.splitObservable_bound line 142
  14. lemma OAI.HardSphere.killedObservable_split line 150
  15. lemma OAI.HardSphere.split_fixedTrajectory_measurable line 166
  16. lemma OAI.HardSphere.split_fixedTrajectory line 175
  17. lemma OAI.HardSphere.killedAverage_add line 191