OAI/Probability/Ballisticity/Geometry/RecordIndexPrefixHeight.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.recordIndexPrefix_height line 224
2. lemma OAI.DirectionalTransience.tubePrefixAt_top_witness line 237
3. lemma OAI.DirectionalTransience.tubePrefixAt_top_deviation line 273
4. lemma OAI.DirectionalTransience.tubeEndpoint_deviation line 280
5. lemma OAI.DirectionalTransience.signedCoordinate_add_distinct_step line 291
6. lemma OAI.DirectionalTransience.directBridge_deviation line 297
7. lemma OAI.DirectionalTransience.tubePrefix_zero_of_initial line 327
8. lemma OAI.DirectionalTransience.tubePrefixMass_zero line 339
9. lemma OAI.DirectionalTransience.stoppedTubeEndpoint_total line 351
10. lemma OAI.DirectionalTransience.firstThreat_previous_mass line 360
11. lemma OAI.DirectionalTransience.firstThreat_bridge_mass line 375
12. lemma OAI.DirectionalTransience.noThreat_mass_lower line 385
13. lemma OAI.DirectionalTransience.normalized_tubePrefixMass line 401
14. lemma OAI.DirectionalTransience.firstThreat_noSecond_retained_mass line 410