OAI/Analysis/HardSphere/Geometry/Point.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.HardSphere.SphericalCoordinates.Point line 20
  2. def OAI.HardSphere.SphericalCoordinates.angle line 21
  3. def OAI.HardSphere.SphericalCoordinates.spherePoint line 23
  4. lemma OAI.HardSphere.SphericalCoordinates.measurable_angle line 26
  5. lemma OAI.HardSphere.SphericalCoordinates.polar_integral line 28
  6. lemma OAI.HardSphere.SphericalCoordinates.cylindrical_integral line 34
  7. lemma OAI.HardSphere.SphericalCoordinates.spherical_integral line 52
  8. def OAI.HardSphere.SphericalCoordinates.sqRadius line 74
  9. def OAI.HardSphere.SphericalCoordinates.direction line 76
  10. lemma OAI.HardSphere.SphericalCoordinates.spherePoint_eq line 79
  11. lemma OAI.HardSphere.SphericalCoordinates.sqRadius_smul line 82
  12. lemma OAI.HardSphere.SphericalCoordinates.direction_unit line 86
  13. lemma OAI.HardSphere.SphericalCoordinates.ray_terminal line 92
  14. def OAI.HardSphere.SphericalCoordinates.axis0 line 123
  15. def OAI.HardSphere.SphericalCoordinates.axis1 line 124
  16. def OAI.HardSphere.SphericalCoordinates.axis2 line 125
  17. def OAI.HardSphere.SphericalCoordinates.gradSq line 127
  18. lemma OAI.HardSphere.SphericalCoordinates.linear_unit_bound line 131
  19. lemma OAI.HardSphere.SphericalCoordinates.gradSq_nonneg line 152
  20. lemma OAI.HardSphere.SphericalCoordinates.continuous_gradSq line 155
  21. lemma OAI.HardSphere.SphericalCoordinates.ray_deriv_bound line 163