OAI/Probability/LatticeSurface/Dynamics/ShiftData.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FeasibleShift.component line 13
  2. def OAI.FeasibleShift.contactGraph line 17
  3. def OAI.FeasibleShift.prescription line 22
  4. def OAI.FeasibleShift.averagedShift line 27
  5. abbrev OAI.FeasibleShift.FreeSites line 31
  6. def OAI.FeasibleShift.extendHeight line 33
  7. def OAI.FeasibleShift.freeShift line 37
  8. def OAI.FeasibleShift.heightPolytope line 41
  9. def OAI.FeasibleShift.neighbors line 46
  10. def OAI.FeasibleShift.shiftGraph line 50
  11. def OAI.FeasibleShift.localSites line 55
  12. structure OAI.FeasibleShift.ShiftData line 59
  13. def OAI.FeasibleShift.ShiftData.polytope line 97
  14. def OAI.FeasibleShift.ShiftData.law line 99
  15. def OAI.FeasibleShift.ShiftData.shift line 101
  16. def OAI.FeasibleShift.ShiftData.map line 104