OAI/Probability/Ballisticity/Walk/StationaryGrowth.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalTransience.orbitAverage line 12
2. lemma OAI.DirectionalTransience.orbitAverage_measurable line 15
3. lemma OAI.DirectionalTransience.orbitAverage_bounds line 20
4. lemma OAI.DirectionalTransience.orbitAverage_integral line 29
5. lemma OAI.DirectionalTransience.lp_orbitAverage line 42
6. lemma OAI.DirectionalTransience.stationary_bounded_growth_limit line 61
7. lemma OAI.DirectionalTransience.growth_limit_respects_symmetry line 111
8. lemma OAI.DirectionalTransience.stationary_positive_growth line 122