OAI/Analysis/HardSphere/Geometry/SelectedEnergyAddCompl.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.selectedEnergy_add_compl line 23
  2. lemma OAI.HardSphere.complement_removed_card line 28
  3. theorem OAI.HardSphere.productPartition_spectral_localization line 38
  4. abbrev OAI.HardSphere.SpatialLift line 83
  5. def OAI.HardSphere.spatialProject line 85
  6. lemma OAI.HardSphere.continuous_spatialProject line 87
  7. lemma OAI.HardSphere.spatialProject_sub line 90
  8. lemma OAI.HardSphere.lipschitz_spatialProject line 95
  9. def OAI.HardSphere.torusMollify line 107
  10. lemma OAI.HardSphere.torusMollify_lift line 110
  11. lemma OAI.HardSphere.torusMollify_integrable line 116
  12. lemma OAI.HardSphere.torusMollify_smooth line 122
  13. lemma OAI.HardSphere.torusMollify_lipschitz line 129
  14. lemma OAI.HardSphere.torusMollify_approximation line 146
  15. def OAI.HardSphere.mollifiedSpatialMultiplier line 161