OAI/Analysis/HardSphere/Bridges/ReverseTime.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HardSphere.Wiener.reverseTime line 16
2. lemma OAI.HardSphere.Wiener.reverseTime_reverse line 20
3. lemma OAI.HardSphere.Wiener.reverseTime_zero line 24
4. lemma OAI.HardSphere.Wiener.reverseTime_one line 25
5. def OAI.HardSphere.Wiener.reverseIncrements line 27
6. lemma OAI.HardSphere.Wiener.reverseIncrements_apply line 31
7. lemma OAI.HardSphere.Wiener.endpoint_shift_projection_algebra line 34
8. lemma OAI.HardSphere.Wiener.reverseIncrements_law line 78
9. lemma OAI.HardSphere.Wiener.reverseIncrements_preserving line 103