OAI/Probability/Ballisticity/Stationary/ArrayFiniteClasses.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.StationaryArrayLaw.finite_current_classes line 18
2. lemma OAI.DirectionalTransience.StationaryArrayLaw.finite_classes_all_times line 58
3. def OAI.DirectionalTransience.ArrayRelated line 83
4. lemma OAI.DirectionalTransience.arrayRelated_measurable line 87
5. lemma OAI.DirectionalTransience.array_offset_self line 92
6. lemma OAI.DirectionalTransience.array_offset_add line 97
7. lemma OAI.DirectionalTransience.arrayRelated_refl line 107
8. lemma OAI.DirectionalTransience.arrayRelated_symm line 110
9. lemma OAI.DirectionalTransience.arrayRelated_trans line 115
10. lemma OAI.DirectionalTransience.arrayRelated_current line 122
11. lemma OAI.DirectionalTransience.array_positive_coordinate_represented line 129
12. lemma OAI.DirectionalTransience.array_next_full line 143
13. lemma OAI.DirectionalTransience.array_forward_survives line 167