OAI/Probability/Ballisticity/Stationary/ArrayMarkedEntropy.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DirectionalTransience.MarkedCurrentData line 13
2. def OAI.DirectionalTransience.markedData line 14
3. lemma OAI.DirectionalTransience.markedData_measurable line 16
4. def OAI.DirectionalTransience.selectUpperField line 19
5. lemma OAI.DirectionalTransience.selectUpperField_measurable line 22
6. def OAI.DirectionalTransience.markedUpper line 29
7. lemma OAI.DirectionalTransience.markedUpper_measurable line 31
8. lemma OAI.DirectionalTransience.marked_window_law line 34
9. lemma OAI.DirectionalTransience.StationaryArrayLaw.marked_upper_entropy line 58