OAI/Probability/Ballisticity/Stationary/StationaryProfile.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalTransience.coordinateProfile line 12
2. instance OAI.DirectionalTransience.coordinateProfile_finite line 16
3. lemma OAI.DirectionalTransience.coordinateProfile_apply line 22
4. lemma OAI.DirectionalTransience.profile_statistic_nonpos line 27
5. lemma OAI.DirectionalTransience.iterate_identDistrib line 40
6. structure OAI.DirectionalTransience.StationaryProfileSystem line 48
7. theorem OAI.DirectionalTransience.stationary_profile_mean_nonpos line 84