OAI/Analysis/HardSphere/Bridges/BridgeResidual.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.Wiener.centerMap line 13
  2. lemma OAI.HardSphere.Wiener.centerMap_apply line 16
  3. lemma OAI.HardSphere.Wiener.centerMap_path line 21
  4. lemma OAI.HardSphere.Wiener.bridgeLaw_center line 25
  5. instance OAI.HardSphere.Wiener.bridgeLaw_isGaussian line 31
  6. lemma OAI.HardSphere.Wiener.finite_bridge_gaussian line 35
  7. lemma OAI.HardSphere.Wiener.bridge_eval_law line 45
  8. lemma OAI.HardSphere.Wiener.bridge_covariance line 50
  9. def OAI.HardSphere.Wiener.bridgeRemainder line 62
  10. lemma OAI.HardSphere.Wiener.bridgeRemainder_apply line 65
  11. lemma OAI.HardSphere.Wiener.bridgeRemainder_eq line 70
  12. lemma OAI.HardSphere.Wiener.bridgeRemainder_law line 80
  13. lemma OAI.HardSphere.Wiener.bridgeRemainder_joint_gaussian line 99
  14. lemma OAI.HardSphere.Wiener.bridgeRemainder_independent line 115
  15. def OAI.HardSphere.coordinateBridge line 141
  16. instance OAI.HardSphere.coordinateBridge_probability line 142
  17. def OAI.HardSphere.gaussianCoordinates line 146
  18. instance OAI.HardSphere.gaussianCoordinates_probability line 147
  19. def OAI.HardSphere.reconstructCoordinates line 151
  20. lemma OAI.HardSphere.reconstructCoordinates_continuous line 154
  21. lemma OAI.HardSphere.reconstructCoordinates_preserving line 158
  22. lemma OAI.HardSphere.bridge_endpoints line 171
  23. lemma OAI.HardSphere.coordinateBridge_endpoints line 177
  24. lemma OAI.HardSphere.reconstruct_free_endpoints line 183