OAI/Analysis/HardSphere/Geometry/NominalDrift.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.Lattice.nominalDrift line 14
  2. lemma OAI.HardSphere.Lattice.nominalDrift_step line 16
  3. lemma OAI.HardSphere.Lattice.nominalDrift_lipschitz line 27
  4. def OAI.HardSphere.Lattice.nominalVertices line 32
  5. lemma OAI.HardSphere.Lattice.nominal_first line 37
  6. lemma OAI.HardSphere.Lattice.nominal_initial line 40
  7. lemma OAI.HardSphere.Lattice.nominal_final line 45
  8. lemma OAI.HardSphere.Lattice.nominal_speed line 51
  9. def OAI.HardSphere.Lattice.firstPathNoise line 77
  10. def OAI.HardSphere.Lattice.secondPathNoise line 78
  11. lemma OAI.HardSphere.Lattice.nominal_difference line 80
  12. def OAI.HardSphere.Lattice.nominalCover line 87
  13. lemma OAI.HardSphere.Lattice.mem_nominalCover line 90
  14. lemma OAI.HardSphere.Lattice.nominal_mem_cover line 104
  15. lemma OAI.HardSphere.Lattice.nominalCover_projection line 107
  16. lemma OAI.HardSphere.Lattice.nominalCover_reach line 114
  17. lemma OAI.HardSphere.Lattice.torusNear_least_iff line 138
  18. lemma OAI.HardSphere.Lattice.pairDifference_abs_le line 151
  19. lemma OAI.HardSphere.Lattice.nominal_near_iff line 157