OAI/Probability/Ballisticity/Estimates/BadOccupationLimit.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalTransience.OperationalConstants.paddedTimes line 15
2. def OAI.DirectionalTransience.OperationalConstants.paddedStages line 20
3. lemma OAI.DirectionalTransience.OperationalConstants.paddedTimes_measurable line 26
4. lemma OAI.DirectionalTransience.OperationalConstants.paddedStages_measurable line 32
5. lemma OAI.DirectionalTransience.OperationalConstants.activeCount_measurable line 38
6. lemma OAI.DirectionalTransience.OperationalConstants.activeCount_le line 44
7. def OAI.DirectionalTransience.OperationalConstants.occupation line 49
8. lemma OAI.DirectionalTransience.OperationalConstants.bad_counts_tendsto line 54
9. theorem OAI.DirectionalTransience.OperationalConstants.bad_occupation_stationary_limit line 76