OAI/Probability/Ballisticity/Geometry/StoppedTubeEndpoint.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalTransience.stoppedTubeEndpoint line 221
2. instance OAI.DirectionalTransience.stoppedTubeEndpoint_finite line 225
3. lemma OAI.DirectionalTransience.stoppedTubeEndpoint_rows line 231
4. lemma OAI.DirectionalTransience.stoppedTubeEndpoint_supported line 243
5. lemma OAI.DirectionalTransience.signedHeight_add_nsmul_step line 253
6. def OAI.DirectionalTransience.bridgedRestart line 261
7. lemma OAI.DirectionalTransience.bridgedRestart_probability line 267
8. lemma OAI.DirectionalTransience.bridgedRestart_supported line 275
9. lemma OAI.DirectionalTransience.bridgedRestart_rows line 289
10. theorem OAI.DirectionalTransience.canonical_two_tube_threat line 326