OAI/Analysis/HardSphere/Geometry/CubeCell.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HardSphere.CubeCell line 34
2. def OAI.HardSphere.unitSectorMeasure line 36
3. lemma OAI.HardSphere.unitSectorMeasure_le line 39
4. def OAI.HardSphere.unitSectorRestriction line 44
5. lemma OAI.HardSphere.unitSectorRestriction_ae line 51
6. lemma OAI.HardSphere.SmoothTest.unitSector_norm line 62
7. def OAI.HardSphere.unitCellPenalty line 78
8. lemma OAI.HardSphere.continuous_unitCellPenalty line 84
9. lemma OAI.HardSphere.SmoothTest.cell_energy line 90
10. lemma OAI.HardSphere.dirichlet_cell_energy line 120
11. lemma OAI.HardSphere.SphericalCoordinates.selected_sector_cell_energy line 134
12. lemma OAI.HardSphere.SphericalCoordinates.selected_subdivided_cell_energy line 168