OAI/Analysis/HardSphere/Operators/FreeTransition.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.wiener_initial_zero line 18
2. lemma OAI.HardSphere.coordinateWiener_initial_zero line 23
3. lemma OAI.HardSphere.freeTrajectory_initial_ae line 29
4. def OAI.HardSphere.freeTransition line 36
5. lemma OAI.HardSphere.freeTransition_pairing line 40
6. lemma OAI.HardSphere.freeTransition_continuous_pairing line 50
7. lemma OAI.HardSphere.integrable_free_character line 61
8. lemma OAI.HardSphere.freeTransition_character_pairing line 76
9. lemma OAI.HardSphere.freeTransition_character line 106