OAI/Analysis/HardSphere/Bridges/BridgeAssemble.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.Wiener.assembleBridge line 16
  2. lemma OAI.HardSphere.Wiener.assembleBridge_continuous line 23
  3. lemma OAI.HardSphere.Wiener.assembleBridge_split line 32
  4. lemma OAI.HardSphere.Wiener.bridge_midpoint_disintegration line 63
  5. def OAI.HardSphere.Wiener.bridgeReverse line 88
  6. lemma OAI.HardSphere.Wiener.center_reverse line 90
  7. lemma OAI.HardSphere.Wiener.bridgeReverse_preserving line 101
  8. def OAI.HardSphere.Bridge.midpointNoise line 125
  9. instance OAI.HardSphere.Bridge.(instance at line 126) line 126
  10. def OAI.HardSphere.Bridge.assembleNoise line 128
  11. lemma OAI.HardSphere.Bridge.assembleNoise_continuous line 130
  12. lemma OAI.HardSphere.Bridge.scalar_assemble_law line 135
  13. lemma OAI.HardSphere.Bridge.assembleNoise_preserving line 145
  14. def OAI.HardSphere.Bridge.reverseNoise line 166
  15. lemma OAI.HardSphere.Bridge.reverseNoise_continuous line 167
  16. lemma OAI.HardSphere.Bridge.reverseNoise_preserving line 168
  17. lemma OAI.HardSphere.Bridge.left_add_right line 174
  18. def OAI.HardSphere.Bridge.midpointPoint line 180
  19. lemma OAI.HardSphere.Bridge.trial_assemble line 182