OAI/Probability/Ballisticity/Walk/RetentionRowsAllHeights.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.retainedPairLaw_zero line 13
2. lemma OAI.DirectionalTransience.retainedPairLaw_joint_rows_all line 18
3. lemma OAI.DirectionalTransience.upwardRetainedLaw_joint_rows line 35
4. lemma OAI.DirectionalTransience.strip_subset_below_height line 50
5. lemma OAI.DirectionalTransience.rowSigma_below_height_mono line 67
6. lemma OAI.DirectionalTransience.retainedPairLaw_at_height_rows line 75
7. lemma OAI.DirectionalTransience.upwardRetainedLaw_at_height_rows line 88
8. lemma OAI.DirectionalTransience.bufferFirstFailure_eq_measurable line 112
9. lemma OAI.DirectionalTransience.bufferStageRetainedLaw_at_stop_lt line 125
10. lemma OAI.DirectionalTransience.bufferStageRetainedLaw_stopped_rows line 136