OAI/Probability/Ballisticity/Entropy/BadWindowEntropy.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.OperationalConstants.paddedTimes_stopping line 17
2. lemma OAI.DirectionalTransience.OperationalConstants.paddedTimes_mono line 25
3. lemma OAI.DirectionalTransience.OperationalConstants.paddedTimes_active line 32
4. def OAI.DirectionalTransience.OperationalConstants.windowEntropyConstant line 40
5. lemma OAI.DirectionalTransience.OperationalConstants.windowEntropyConstant_nonneg line 43
6. lemma OAI.DirectionalTransience.OperationalConstants.bad_window_kl_le line 49
7. lemma OAI.DirectionalTransience.OperationalConstants.bad_occupation_currentOffsets line 92
8. theorem OAI.DirectionalTransience.OperationalConstants.bad_limit_window_entropy line 101