OAI/Probability/Ballisticity/Geometry/TubePrefixMass.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalTransience.tubePrefixMass line 207
2. lemma OAI.DirectionalTransience.tubePrefixMass_toReal line 211
3. lemma OAI.DirectionalTransience.measurable_tubePrefixMass line 218
4. def OAI.DirectionalTransience.tubeLayerMass line 230
5. lemma OAI.DirectionalTransience.tubeLayerMass_eq line 235
6. lemma OAI.DirectionalTransience.tubeLayerMass_joint_rows line 249
7. lemma OAI.DirectionalTransience.tubeLayerMass_lower_rows line 269
8. lemma OAI.DirectionalTransience.tubeLayerMass_upper_rows line 276
9. def OAI.DirectionalTransience.TubeThreat line 283
10. lemma OAI.DirectionalTransience.measurableSet_tubeThreat_upper line 287
11. def OAI.DirectionalTransience.FirstTubeThreat line 308
12. lemma OAI.DirectionalTransience.firstTubeThreat_disjoint line 313
13. lemma OAI.DirectionalTransience.firstTubeThreat_iUnion line 323
14. lemma OAI.DirectionalTransience.firstTubeThreat_lower_rows line 343
15. lemma OAI.DirectionalTransience.tubeThreat_probability_le line 375
16. lemma OAI.DirectionalTransience.fresh_random_tube_threat line 385