OAI/Analysis/HardSphere/Bridges/BridgeSplit.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HardSphere.Wiener.bridgePrefix line 14
2. lemma OAI.HardSphere.Wiener.bridgePrefix_apply line 15
3. lemma OAI.HardSphere.Wiener.bridgePrefix_eq line 23
4. lemma OAI.HardSphere.Wiener.bridgePrefix_law line 33
5. lemma OAI.HardSphere.Wiener.prefixRemainder_gaussian line 50
6. lemma OAI.HardSphere.Wiener.prefixRemainder_independent line 67
7. lemma OAI.HardSphere.Wiener.prefixValue_gaussian line 88
8. lemma OAI.HardSphere.Wiener.prefixValue_independent line 105
9. lemma OAI.HardSphere.Wiener.bridge_three_law line 128