OAI/Analysis/HardSphere/Geometry/GridActivePenalty.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.gridActivePenalty line 28
  2. lemma OAI.HardSphere.continuous_gridActivePenalty line 34
  3. lemma OAI.HardSphere.selectedEnergy_nonneg line 41
  4. lemma OAI.HardSphere.selectedEnergy_ofReal line 44
  5. lemma OAI.HardSphere.SmoothTest.active_grid_energy line 51
  6. lemma OAI.HardSphere.dirichlet_active_grid_energy line 70
  7. def OAI.HardSphere.gridSite line 81
  8. lemma OAI.HardSphere.measurable_gridSite line 87
  9. lemma OAI.HardSphere.gridSector_site_ae line 93
  10. def OAI.HardSphere.gridActiveCount line 114
  11. lemma OAI.HardSphere.measurable_gridActiveCount line 119
  12. lemma OAI.HardSphere.gridActivePenalty_eq_integral line 125
  13. lemma OAI.HardSphere.dirichlet_physical_grid_energy line 154
  14. lemma OAI.HardSphere.coordinate_distance_le line 162
  15. def OAI.HardSphere.halfGridBase line 167
  16. lemma OAI.HardSphere.halfGrid_pair_cover line 170
  17. def OAI.HardSphere.nearLabels line 185
  18. lemma OAI.HardSphere.nearLabels_card_le_grids line 190
  19. lemma OAI.HardSphere.dirichlet_near_energy_grid line 203