OAI/Probability/Ballisticity/Crossings/LowerObservedCut.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.commonTrueRecord_time_eq line 16
2. lemma OAI.DirectionalTransience.selectedBoundaryAt_le line 23
3. def OAI.DirectionalTransience.lowerCutCriterion line 37
4. lemma OAI.DirectionalTransience.lowerCutCriterion_height line 41
5. lemma OAI.DirectionalTransience.lowerCut_selected_escape line 44
6. lemma OAI.DirectionalTransience.lowerCut_escape_event line 66
7. theorem OAI.DirectionalTransience.shared_lower_selected_potential_drift line 89