OAI/Analysis/HardSphere/Bridges/BridgeAverage.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.Bridge.averageCost line 15
  2. lemma OAI.HardSphere.Bridge.legCost_nonneg line 18
  3. lemma OAI.HardSphere.Bridge.liftedDiameter_continuous line 22
  4. lemma OAI.HardSphere.Bridge.legCost_continuous line 29
  5. lemma OAI.HardSphere.Bridge.averageCost_lintegral line 40
  6. lemma OAI.HardSphere.Bridge.averageCost_tail line 58
  7. def OAI.HardSphere.Bridge.fluctuationMoment line 84
  8. lemma OAI.HardSphere.Bridge.fluctuationMoment_nonneg line 85
  9. lemma OAI.HardSphere.Bridge.incrementFluctuation_power_mean line 89
  10. lemma OAI.HardSphere.Bridge.incrementFluctuation_tail line 107
  11. def OAI.HardSphere.Bridge.legMeshRatio line 142
  12. lemma OAI.HardSphere.Bridge.legMeshRatio_tail line 145
  13. lemma OAI.HardSphere.Bridge.legMeshMax_tail line 160