OAI/Probability/Ballisticity/Stationary/StationaryProfile2.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DirectionalTransience.FullMarkedArray line 12
2. def OAI.DirectionalTransience.fullMarkedShift line 13
3. lemma OAI.DirectionalTransience.fullMarkedShift_iterate_fst line 16
4. def OAI.DirectionalTransience.StationaryArrayLaw.actualProfileSystem line 28
5. theorem OAI.DirectionalTransience.StationaryArrayLaw.impossible line 99