OAI/Probability/LatticePassage/Model.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CompanionFPP.Vertex line 15
  2. abbrev OAI.CompanionFPP.Plane line 16
  3. def OAI.CompanionFPP.lattice line 18
  4. abbrev OAI.CompanionFPP.Edge line 23
  5. abbrev OAI.CompanionFPP.Environment line 24
  6. instance OAI.CompanionFPP.expOneProbability line 26
  7. def OAI.CompanionFPP.environmentLaw line 29
  8. def OAI.CompanionFPP.embed line 32
  9. def OAI.CompanionFPP.scaleVertex line 34
  10. structure OAI.CompanionFPP.TimeNorm line 36
  11. def OAI.CompanionFPP.HasTimeConstant line 40
  12. def OAI.CompanionFPP.StrictlyConvexUnitSphere line 45
  13. def OAI.CompanionFPP.StrictlyConvexLimitShape line 49
  14. def OAI.CompanionFPP.MainTarget line 54