OAI/Analysis/HardSphere/PathBounds/PathTailConstant.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.staysAllowed_of_neg line 20
2. lemma OAI.HardSphere.killedObservable_of_neg line 27
3. lemma OAI.HardSphere.killedTransition_of_neg line 32
4. lemma OAI.HardSphere.freeTrajectory_dist_le line 41
5. lemma OAI.HardSphere.killedObservable_eq_of_small_path line 66
6. lemma OAI.HardSphere.coordinateWiener_tail8 line 85
7. lemma OAI.HardSphere.killedAverage_free_bound line 104
8. def OAI.HardSphere.pathTailConstant line 145
9. lemma OAI.HardSphere.pathTailConstant_nonneg line 149
10. lemma OAI.HardSphere.coordinateWiener_tail8_real line 151
11. lemma OAI.HardSphere.killedAverage_free_order4 line 165
12. lemma OAI.HardSphere.killedTransition_continuous_ae_core line 193
13. lemma OAI.HardSphere.killedTransition_free_order4 line 207
14. lemma OAI.HardSphere.killedTransition_free_firstOrder line 234