OAI/Analysis/HardSphere/Geometry/SmoothSiteWeight.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.smoothSiteWeight line 24
  2. lemma OAI.HardSphere.smoothSiteWeight_pos line 27
  3. lemma OAI.HardSphere.smoothSiteWeight_bounds line 30
  4. lemma OAI.HardSphere.smoothSiteWeight_le line 36
  5. def OAI.HardSphere.smoothSiteWeightMultiplier line 41
  6. lemma OAI.HardSphere.smoothSiteWeightMultiplier_apply line 45
  7. lemma OAI.HardSphere.smoothSiteWeightMultiplier_real line 48
  8. lemma OAI.HardSphere.smoothSiteWeight_continuous line 52
  9. lemma OAI.HardSphere.smoothSiteWeight_partial_sq line 55
  10. def OAI.HardSphere.smoothWeightedCount line 74
  11. def OAI.HardSphere.smoothWeightedCountMultiplier line 77
  12. lemma OAI.HardSphere.smoothWeightedCountMultiplier_apply line 80
  13. lemma OAI.HardSphere.smoothWeightedCountMultiplier_real line 86
  14. lemma OAI.HardSphere.smoothWeightedCount_nonneg line 90
  15. lemma OAI.HardSphere.smoothWeightedCount_le line 93
  16. lemma OAI.HardSphere.smoothWeightedCount_bounds line 99
  17. lemma OAI.HardSphere.smoothWeightedCount_continuous line 106
  18. lemma OAI.HardSphere.smoothWeightedCount_gradient line 110
  19. lemma OAI.HardSphere.groundPositionLaw_integral line 135
  20. lemma OAI.HardSphere.groundPositionLaw_integrable line 142
  21. lemma OAI.HardSphere.groundPositionLaw_probability line 149
  22. lemma OAI.HardSphere.bounded_mgf_integrable line 158
  23. lemma OAI.HardSphere.bounded_integrableExpSet line 170
  24. lemma OAI.HardSphere.bounded_cgf_le line 177