OAI/Analysis/HardSphere/Geometry/HalfShiftCover.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.GridGeometry.half_shift_cover line 25
  2. lemma OAI.HardSphere.GridGeometry.floor_grid_periodic line 41
  3. def OAI.HardSphere.GridGeometry.index line 49
  4. lemma OAI.HardSphere.GridGeometry.index_coe line 52
  5. lemma OAI.HardSphere.GridGeometry.index_pair_cover line 55
  6. lemma OAI.HardSphere.GridGeometry.measurable_index line 82
  7. lemma OAI.HardSphere.GridGeometry.index_in_cell line 92
  8. lemma OAI.HardSphere.SphericalCoordinates.pointFin_preserving_base line 107
  9. lemma OAI.HardSphere.SphericalCoordinates.configurationFin_preserving_base line 118
  10. lemma OAI.HardSphere.cubeParameter_preserving_base line 128
  11. def OAI.HardSphere.gridSectorMeasure line 137
  12. lemma OAI.HardSphere.gridSectorMeasure_le line 140
  13. def OAI.HardSphere.gridSectorRestriction line 145
  14. lemma OAI.HardSphere.gridSectorRestriction_ae line 152
  15. lemma OAI.HardSphere.gridSector_norm line 163
  16. lemma OAI.HardSphere.SmoothTest.gridSector_norm line 174
  17. lemma OAI.HardSphere.SmoothTest.cube_gradient_lintegral_base line 187