OAI/Analysis/HardSphere/Cutoffs/CubicMoment.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.PathCutoff.diameterRatio line 16
  2. def OAI.HardSphere.PathCutoff.cubicCost line 18
  3. lemma OAI.HardSphere.PathCutoff.diameterRatio_continuous line 20
  4. lemma OAI.HardSphere.PathCutoff.diameterRatio_nonneg line 22
  5. lemma OAI.HardSphere.PathCutoff.cubicCost_continuous line 24
  6. lemma OAI.HardSphere.PathCutoff.cubicCost_nonneg line 26
  7. lemma OAI.HardSphere.PathCutoff.cubicCost_reverse line 30
  8. lemma OAI.HardSphere.PathCutoff.free_cubicCost_le line 38
  9. lemma OAI.HardSphere.PathCutoff.free_cubicCost_integrable line 47
  10. def OAI.HardSphere.PathCutoff.cubicMean line 58
  11. lemma OAI.HardSphere.PathCutoff.cubicMean_nonneg line 59
  12. lemma OAI.HardSphere.PathCutoff.free_cubicMean_le line 61
  13. def OAI.HardSphere.PathCutoff.cappedWeight line 65
  14. lemma OAI.HardSphere.PathCutoff.cappedWeight_measurable line 67
  15. def OAI.HardSphere.PathCutoff.meanCost line 70
  16. lemma OAI.HardSphere.PathCutoff.meanCost_nonneg line 71
  17. lemma OAI.HardSphere.PathCutoff.free_cap_moment line 76
  18. def OAI.HardSphere.PathCutoff.capSum line 103
  19. lemma OAI.HardSphere.PathCutoff.capSum_continuous line 105
  20. lemma OAI.HardSphere.PathCutoff.cap_product_eq line 109
  21. lemma OAI.HardSphere.PathCutoff.orig_exp_pow line 114
  22. lemma OAI.HardSphere.PathCutoff.mesh_cap_moment line 118
  23. lemma OAI.HardSphere.PathCutoff.mesh_cap_tail line 126