OAI/Analysis/HardSphere/Operators/Stationary.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HardSphere.weightedKilledTransition line 13
2. lemma OAI.HardSphere.weightedKilledTransition_pairing line 20
3. def OAI.HardSphere.weightedKilledAverage line 40
4. lemma OAI.HardSphere.weightedKilledAverage_measurable line 46
5. lemma OAI.HardSphere.weightedKilledAverage_bound line 53
6. lemma OAI.HardSphere.weightedKilledAverage_memLp line 64
7. lemma OAI.HardSphere.integrable_weightedAverage_pairing line 73
8. lemma OAI.HardSphere.weightedKilledTransition_bounded_pairing line 93
9. lemma OAI.HardSphere.weightedKilledTransition_bounded line 134
10. lemma OAI.HardSphere.weightedKilledAverage_prefix line 166
11. lemma OAI.HardSphere.weightedKilledTransition_prefix line 212
12. lemma OAI.HardSphere.weightedKilledTransition_indicator_pairing line 254
13. lemma OAI.HardSphere.IsGroundVector.prefix_norm_setIntegral line 270
14. lemma OAI.HardSphere.IsGroundVector.groundPathLaw_prefix line 306
15. lemma OAI.HardSphere.splitTime_reverse line 329
16. lemma OAI.HardSphere.reverse_prefix_reverse line 337
17. lemma OAI.HardSphere.IsGroundVector.groundPathLaw_suffix line 348
18. lemma OAI.HardSphere.groundPathLaw_absolutelyContinuous line 358
19. lemma OAI.HardSphere.freePathLaw_zero_eval line 362
20. lemma OAI.HardSphere.IsGroundVector.groundPathLaw_marginal line 371
21. lemma OAI.HardSphere.IsGroundVector.groundPathLaw_middle line 403
22. lemma OAI.HardSphere.IsGroundVector.groundPathLaw_close_event line 419
23. theorem OAI.HardSphere.spatial_stationary_close_tail line 430