OAI/Analysis/HardSphere/Bridges/BridgeHighMoment.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.Wiener.normPowerMean line 15
  2. lemma OAI.HardSphere.Wiener.normPowerMean_nonneg line 16
  3. lemma OAI.HardSphere.Wiener.integrable_normPower line 17
  4. lemma OAI.HardSphere.Wiener.loose_add_pow line 20
  5. lemma OAI.HardSphere.Wiener.prefix_normPower line 33
  6. lemma OAI.HardSphere.Wiener.increment_wiener_power line 39
  7. lemma OAI.HardSphere.Wiener.increment_bridge_power line 49
  8. lemma OAI.HardSphere.Bridge.sum_three_power line 87
  9. lemma OAI.HardSphere.Bridge.incrementSize_memLp_power line 99
  10. lemma OAI.HardSphere.Bridge.incrementSize_power_mean line 105
  11. def OAI.HardSphere.Bridge.pathCoordinates line 143
  12. lemma OAI.HardSphere.Bridge.liftedDiameter_coord_le line 145
  13. lemma OAI.HardSphere.Bridge.leg_mesh_coord_bound line 160
  14. lemma OAI.HardSphere.Bridge.leg_mesh_diameter line 186