OAI/Probability/Ballisticity/Estimates/BufferFirstFailure.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalTransience.BelowHeight line 14
2. def OAI.DirectionalTransience.PairAtHeight line 17
3. def OAI.DirectionalTransience.rowHeightFiltration line 20
4. def OAI.DirectionalTransience.bufferTraversalMass line 32
5. lemma OAI.DirectionalTransience.bufferTraversalMass_adapted line 36
6. def OAI.DirectionalTransience.bufferFirstFailure line 68
7. lemma OAI.DirectionalTransience.bufferFirstFailure_stopping line 72
8. lemma OAI.DirectionalTransience.bufferFirstFailure_bounds line 78
9. lemma OAI.DirectionalTransience.before_bufferFirstFailure_pass line 84
10. lemma OAI.DirectionalTransience.bufferFirstFailure_fails_of_lt line 91