OAI/Analysis/HardSphere/Geometry/SubsetPointLinear.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HardSphere.SphericalCoordinates.subsetPointLinear line 24
2. def OAI.HardSphere.SphericalCoordinates.subsetPointFill line 28
3. lemma OAI.HardSphere.SphericalCoordinates.subsetPointFill_affine line 32
4. lemma OAI.HardSphere.SphericalCoordinates.subsetPointLinear_single line 38
5. lemma OAI.HardSphere.SphericalCoordinates.contDiff_subsetPointFill line 51
6. lemma OAI.HardSphere.SphericalCoordinates.indexGradSq_subset line 59
7. lemma OAI.HardSphere.SphericalCoordinates.lintegral_subsetPointFill line 73
8. lemma OAI.HardSphere.SphericalCoordinates.subset_cube_energy line 86
9. lemma OAI.HardSphere.SphericalCoordinates.sector_cell_energy line 123
10. lemma OAI.HardSphere.SphericalCoordinates.subdivided_cell_energy line 142