OAI/Analysis/HardSphere/Allocation/PhysicalAverageMoment.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.Groups.physicalAverageLikelihood line 18
  2. lemma OAI.HardSphere.Groups.physicalAverageLikelihood_measurable line 26
  3. lemma OAI.HardSphere.Groups.physicalAverageLikelihood_square line 37
  4. theorem OAI.HardSphere.Groups.physicalAverage_moment line 59
  5. def OAI.HardSphere.Groups.physicalGoodLikelihood line 104
  6. lemma OAI.HardSphere.Groups.physicalGoodLikelihood_measurable line 111
  7. theorem OAI.HardSphere.Groups.physicalGoodLikelihood_moment line 119