OAI/Probability/LatticeSurface/Dynamics/LatticeShift.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.FeasibleShift.localSites_card_bound line 243
  2. structure OAI.FeasibleShift.LatticeData line 263
  3. def OAI.FeasibleShift.LatticeData.toShiftData line 298
  4. def OAI.FeasibleShift.LatticeData.polytope line 370
  5. def OAI.FeasibleShift.LatticeData.law line 372
  6. def OAI.FeasibleShift.LatticeData.map line 374
  7. theorem OAI.FeasibleShift.feasible_lattice_shifts_product line 379