OAI/Probability/Ballisticity/Geometry/TubeHeightMono.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.tubePrefix_eq_curvePrefix line 15
2. lemma OAI.DirectionalTransience.tubePrefix_mono_height_ae line 19
3. lemma OAI.DirectionalTransience.quenchedTube_mono_height line 33
4. lemma OAI.DirectionalTransience.tubePrefix_mono_width line 49
5. lemma OAI.DirectionalTransience.curvePolicy_real_tube_probability line 59