OAI/Probability/Ballisticity/Geometry/WindowWeak.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.DirectionalTransience.currentDataProfiles_secondCountable line 15
2. instance OAI.DirectionalTransience.currentDataProfiles_compact line 17
3. instance OAI.DirectionalTransience.currentFields_compact line 19
4. instance OAI.DirectionalTransience.currentWindow_compact line 21
5. instance OAI.DirectionalTransience.currentWindow_secondCountable line 22
6. instance OAI.DirectionalTransience.currentWindow_opens line 24
7. instance OAI.DirectionalTransience.currentDataProfiles_borel line 25
8. instance OAI.DirectionalTransience.currentDataProfiles_opens line 27
9. lemma OAI.DirectionalTransience.actualCurrentLaw_include line 30
10. lemma OAI.DirectionalTransience.actualCurrentLaw_tendsto line 42
11. def OAI.DirectionalTransience.currentReferenceLaw line 55
12. lemma OAI.DirectionalTransience.currentReferenceLaw_tendsto line 60
13. theorem OAI.DirectionalTransience.actualCurrentLaw_kl_weak_limit line 70