OAI/Probability/Ballisticity/Geometry/TubePrefixMonoRadius.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.tubePrefix_mono_radius line 231
2. lemma OAI.DirectionalTransience.tubePrefixMass_mono_radius line 241
3. lemma OAI.DirectionalTransience.tubePrefixMass_comp_le line 246
4. lemma OAI.DirectionalTransience.directBridge_lintegral line 262
5. lemma OAI.DirectionalTransience.single_step_tubePrefixAt line 271
6. lemma OAI.DirectionalTransience.directBridge_tubeMass_le line 310
7. lemma OAI.DirectionalTransience.bridged_continuation_le_tube line 336
8. lemma OAI.DirectionalTransience.tubePrefixMass_ne_top line 362
9. theorem OAI.DirectionalTransience.short_block_slope_survival line 368