OAI/Analysis/HardSphere/Geometry/EuclideanTorus.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.HardSphere.EuclideanTorus line 24
  2. def OAI.HardSphere.euclideanTorusPoint line 26
  3. lemma OAI.HardSphere.euclideanTorusPoint_dist line 28
  4. def OAI.HardSphere.spatialSiteDistance line 32
  5. def OAI.HardSphere.spatialMetricConstant line 35
  6. lemma OAI.HardSphere.spatialMetricConstant_pos line 37
  7. lemma OAI.HardSphere.spatialSiteDistance_lipschitz line 41
  8. lemma OAI.HardSphere.spatialSiteDistance_nonneg line 52
  9. lemma OAI.HardSphere.spatialSiteDistance_le line 55
  10. lemma OAI.HardSphere.spatialSiteDistance_attained line 60
  11. def OAI.HardSphere.spatialDistanceBump line 67
  12. def OAI.HardSphere.smoothSpatialDistance line 76
  13. lemma OAI.HardSphere.smoothSpatialDistance_lipschitz line 79
  14. lemma OAI.HardSphere.smoothSpatialDistance_approximation line 83
  15. def OAI.HardSphere.spatialDistanceMultiplier line 90
  16. lemma OAI.HardSphere.spatialDistanceMultiplier_apply line 94
  17. lemma OAI.HardSphere.spatialDistanceMultiplier_real line 97
  18. lemma OAI.HardSphere.spatialDistanceMultiplier_partial_bound line 101
  19. def OAI.HardSphere.spatialAngle line 138
  20. def OAI.HardSphere.spatialSine line 139
  21. def OAI.HardSphere.spatialCosine line 140
  22. lemma OAI.HardSphere.spatialAngle_smooth line 142
  23. lemma OAI.HardSphere.spatialSine_smooth line 144
  24. lemma OAI.HardSphere.spatialCosine_smooth line 146
  25. lemma OAI.HardSphere.spatialAngle_hasDerivAt line 149
  26. lemma OAI.HardSphere.spatialSine_deriv line 155
  27. lemma OAI.HardSphere.spatialCosine_deriv line 158
  28. def OAI.HardSphere.spatialInside line 162
  29. def OAI.HardSphere.spatialOutside line 164
  30. lemma OAI.HardSphere.spatialInside_apply line 167
  31. lemma OAI.HardSphere.spatialOutside_apply line 169
  32. lemma OAI.HardSphere.spatialInside_real line 171
  33. lemma OAI.HardSphere.spatialOutside_real line 174
  34. lemma OAI.HardSphere.spatialPartition_unity line 178
  35. lemma OAI.HardSphere.spatialInside_norm_le line 190
  36. lemma OAI.HardSphere.spatialInside_one line 196
  37. lemma OAI.HardSphere.spatialInside_zero line 203
  38. lemma OAI.HardSphere.spatialInside_partial line 210
  39. lemma OAI.HardSphere.spatialOutside_partial line 217
  40. lemma OAI.HardSphere.spatialPartition_partial_zero line 225
  41. theorem OAI.HardSphere.spatialPartition_partial_bound line 235