OAI/Probability/Ballisticity/Geometry/TubeEndpoint.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalTransience.tubeEndpoint line 210
2. lemma OAI.DirectionalTransience.tubeEndpoint_apply line 214
3. lemma OAI.DirectionalTransience.tubeEndpoint_total line 223
4. instance OAI.DirectionalTransience.tubeEndpoint_finite line 230
5. lemma OAI.DirectionalTransience.tubeEndpoint_rows line 234
6. def OAI.DirectionalTransience.tubeEndpointMixture line 250
7. lemma OAI.DirectionalTransience.tubeEndpointMixture_total line 254
8. lemma OAI.DirectionalTransience.tubeEndpointMixture_total_le line 261
9. instance OAI.DirectionalTransience.tubeEndpointMixture_finite line 269
10. lemma OAI.DirectionalTransience.tubeEndpointMixture_lower_rows line 274
11. lemma OAI.DirectionalTransience.two_tube_threat_bound line 299