OAI/Probability/Ballisticity/Geometry/HeightTubeWindow.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalTransience.heightTubeEndpointEvent line 14
2. lemma OAI.DirectionalTransience.measurableSet_heightTubeEndpointEvent line 17
3. lemma OAI.DirectionalTransience.heightPolygon_window_implies_tube line 27
4. lemma OAI.DirectionalTransience.half_layer_grid_tendsto line 50