OAI/Analysis/HardSphere/Geometry/RadiusLaw.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.radiusLaw line 22
  2. instance OAI.HardSphere.radiusLaw_probability line 23
  3. instance OAI.HardSphere.radiusLaw_noAtoms line 24
  4. lemma OAI.HardSphere.radiusLaw_tail_eq line 28
  5. lemma OAI.HardSphere.radiusLaw_tail line 39
  6. lemma OAI.HardSphere.radius_integral_bound line 47
  7. lemma OAI.HardSphere.spatialSine_deriv_continuous_radius line 65
  8. lemma OAI.HardSphere.spatialCosine_deriv_continuous_radius line 72
  9. def OAI.HardSphere.spatialEnergyError line 79
  10. lemma OAI.HardSphere.spatialEnergyError_nonneg line 83
  11. lemma OAI.HardSphere.spatialEnergyError_continuous_radius line 86
  12. lemma OAI.HardSphere.spatialInside_average line 95
  13. theorem OAI.HardSphere.spatialEnergyError_average line 107
  14. lemma OAI.HardSphere.L2_bounded_weight_integrable line 137
  15. lemma OAI.HardSphere.radius_configuration_bound line 147
  16. lemma OAI.HardSphere.spatialInside_joint_continuous line 170
  17. lemma OAI.HardSphere.spatialEnergyError_joint_continuous line 178
  18. def OAI.HardSphere.weightedSiteCount line 195
  19. lemma OAI.HardSphere.weightedSiteCount_nonneg line 198
  20. lemma OAI.HardSphere.weightedSiteCount_le line 203
  21. lemma OAI.HardSphere.weightedSiteCount_continuous line 212
  22. lemma OAI.HardSphere.spatialInside_configuration_average line 220
  23. theorem OAI.HardSphere.spatialEnergyError_configuration_average line 246