OAI/Probability/Ballisticity/Estimates/CommonOccupationBound.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalTransience.PhysicalGapExit line 17
2. lemma OAI.DirectionalTransience.measurableSet_physicalGapExit line 21
3. lemma OAI.DirectionalTransience.smallCommonCount_expectation_eq_sum line 28
4. theorem OAI.DirectionalTransience.smallCommonCount_expectation_le line 54
5. theorem OAI.DirectionalTransience.occupation_finite_bound line 131