OAI/Probability/Ballisticity/Geometry/TubePrefix.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.quenched_prefix_event_congr line 198
2. lemma OAI.DirectionalTransience.measurable_quenched_prefix_event_rows line 218
3. def OAI.DirectionalTransience.TubePrefixAt line 228
4. lemma OAI.DirectionalTransience.measurableSet_tubePrefixAt line 235
5. lemma OAI.DirectionalTransience.tubePrefixAt_prefix line 250
6. def OAI.DirectionalTransience.TubePrefix line 264
7. lemma OAI.DirectionalTransience.measurableSet_tubePrefix line 267
8. lemma OAI.DirectionalTransience.tubePrefixAt_disjoint line 271
9. lemma OAI.DirectionalTransience.quenched_tubePrefix_congr line 278
10. lemma OAI.DirectionalTransience.measurable_quenched_tubePrefix_rows line 288