OAI/Analysis/HardSphere/Geometry/PointFin.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.SphericalCoordinates.pointFin line 23
  2. lemma OAI.HardSphere.SphericalCoordinates.pointFin_apply line 28
  3. lemma OAI.HardSphere.SphericalCoordinates.pointFin_preserving line 32
  4. def OAI.HardSphere.SphericalCoordinates.configurationFin line 43
  5. lemma OAI.HardSphere.SphericalCoordinates.configurationFin_apply line 46
  6. lemma OAI.HardSphere.SphericalCoordinates.configurationFin_single line 49
  7. lemma OAI.HardSphere.SphericalCoordinates.configurationFin_preserving line 57
  8. lemma OAI.HardSphere.SphericalCoordinates.sqRadius_eq_sum line 63
  9. def OAI.HardSphere.cubeParameter line 72
  10. lemma OAI.HardSphere.cubeParameter_preserving line 75
  11. lemma OAI.HardSphere.addCircle_dist_coe_sq_le line 87
  12. lemma OAI.HardSphere.cubeParameter_distance line 95
  13. lemma OAI.HardSphere.SmoothTest.cube_zero line 106
  14. lemma OAI.HardSphere.SmoothTest.cube_smooth line 120
  15. lemma OAI.HardSphere.SmoothTest.cube_derivative line 124
  16. lemma OAI.HardSphere.SmoothTest.cube_gradient line 136
  17. lemma OAI.HardSphere.smooth_norm_lintegral line 150
  18. lemma OAI.HardSphere.cube_energy_coefficient_nonneg line 161
  19. lemma OAI.HardSphere.SmoothTest.cube_gradient_lintegral line 169
  20. lemma OAI.HardSphere.SmoothTest.energy_lower line 184
  21. lemma OAI.HardSphere.dirichlet_energy_lower line 201
  22. lemma OAI.HardSphere.IsGroundVector.energy_lower line 210
  23. lemma OAI.HardSphere.IsGroundVector.energy_per_particle_lower line 216