OAI/Analysis/HardSphere/Bridges/BridgeWiener.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.Bridge.rawNoise line 15
  2. def OAI.HardSphere.Bridge.centeredNoise line 16
  3. lemma OAI.HardSphere.Bridge.rawNoise_preserving line 17
  4. lemma OAI.HardSphere.Bridge.centeredNoise_preserving line 24
  5. lemma OAI.HardSphere.Bridge.lifted_coord_le line 31
  6. lemma OAI.HardSphere.Bridge.centeredNoise_eval line 41
  7. def OAI.HardSphere.Bridge.rawPath line 56
  8. lemma OAI.HardSphere.Bridge.rawPath_lift line 58
  9. lemma OAI.HardSphere.Bridge.mesh_time_dist line 64
  10. lemma OAI.HardSphere.Bridge.centered_leg_mesh_coord line 72
  11. lemma OAI.HardSphere.Bridge.centered_leg_mesh_diameter line 103
  12. def OAI.HardSphere.Bridge.legCost line 127
  13. def OAI.HardSphere.Bridge.bridgeMeanCost line 130
  14. lemma OAI.HardSphere.Bridge.bridgeMeanCost_pos line 131
  15. lemma OAI.HardSphere.Bridge.legCost_bound line 133
  16. lemma OAI.HardSphere.Bridge.legCost_moment line 147