OAI/Analysis/MarkovType/FiniteFirstCrossing.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MarkovSuperreflexivity.FinitePartitionFiltration.firstCrossing line 16
2. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.firstCrossing_le line 19
3. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.firstCrossing_spec line 26
4. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.firstCrossing_eq_terminal_of_no_crossing line 32
5. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.exists_crossing_iff_firstCrossing line 38
6. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.firstCrossing_min line 45
7. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.firstCrossing_le_iff_of_lt line 53
8. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.isStoppingTime_firstCrossing line 68
9. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.firstCrossing_value_eq_of_stopped_rel line 87
10. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.firstCrossing_event_stopped line 95