OAI/Analysis/HardSphere/Geometry/SelectedUnitCellPenalty.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.selectedUnitCellPenalty line 25
  2. lemma OAI.HardSphere.continuous_selectedUnitCellPenalty line 31
  3. lemma OAI.HardSphere.SmoothTest.selected_cell_energy line 37
  4. lemma OAI.HardSphere.dirichlet_selected_cell_energy line 67
  5. def OAI.HardSphere.unitIndex line 77
  6. lemma OAI.HardSphere.measurable_unitIndex line 83
  7. def OAI.HardSphere.unitSite line 94
  8. lemma OAI.HardSphere.measurable_unitSite line 97
  9. lemma OAI.HardSphere.unitIndex_coe line 103
  10. lemma OAI.HardSphere.cube_ae_halfOpen line 115
  11. lemma OAI.HardSphere.unitSector_site_ae line 127
  12. def OAI.HardSphere.unitOccupation line 150
  13. def OAI.HardSphere.occupationWeight line 154
  14. lemma OAI.HardSphere.occupationWeight_nonneg line 159
  15. lemma OAI.HardSphere.unitSector_norm line 166
  16. lemma OAI.HardSphere.selectedUnitCellPenalty_eq_integral line 176
  17. lemma OAI.HardSphere.dirichlet_physical_cell_energy line 212