OAI/Probability/Ballisticity/Estimates/VisibleFailure.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalTransience.VisibleFailure line 144
2. lemma OAI.DirectionalTransience.measurableSet_visibleFailure line 148
3. lemma OAI.DirectionalTransience.visibleFailure_prefix line 157
4. lemma OAI.DirectionalTransience.future_truth_not_visible line 177
5. def OAI.DirectionalTransience.VisibleHistory line 190
6. lemma OAI.DirectionalTransience.measurableSet_visibleHistory line 193
7. lemma OAI.DirectionalTransience.visibleHistory_at_height_prefix line 200
8. theorem OAI.DirectionalTransience.shared_visible_history_bound line 225