OAI/Analysis/HardSphere/Geometry/SpatialPartitionEnergy.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HardSphere.spatialPartitionEnergy line 24
2. lemma OAI.HardSphere.spatialPartitionEnergy_nonneg line 28
3. theorem OAI.HardSphere.spatial_spectral_average line 33
4. def OAI.HardSphere.SphericalCoordinates.reindexPoint line 89
5. lemma OAI.HardSphere.SphericalCoordinates.reindexPoint_apply line 93
6. lemma OAI.HardSphere.SphericalCoordinates.reindexPoint_single line 96
7. lemma OAI.HardSphere.SphericalCoordinates.reindexPoint_preserving line 108
8. def OAI.HardSphere.SphericalCoordinates.indexGradSq line 115
9. lemma OAI.HardSphere.SphericalCoordinates.indexGradSq_reindex line 122
10. lemma OAI.HardSphere.SphericalCoordinates.continuous_indexGradSq line 130
11. lemma OAI.HardSphere.SphericalCoordinates.finite_cube_energy line 138