OAI/Probability/Ballisticity/Geometry/RawWindow.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DirectionalTransience.RawCurrentData line 16
2. def OAI.DirectionalTransience.rawCurrentWindow line 19
3. lemma OAI.DirectionalTransience.sampled_stoppedWindow_law line 29
4. lemma OAI.DirectionalTransience.rawCurrentWindow_measurable line 56
5. theorem OAI.DirectionalTransience.rawCurrentWindow_kl_le line 73