OAI/Probability/Ballisticity/PositiveEscape.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.uniformElliptic_directional_zero_one line 10
2. lemma OAI.DirectionalTransience.dot_div_right line 20
3. lemma OAI.DirectionalTransience.dot_self_pos_of_ne_zero line 24
4. lemma OAI.DirectionalTransience.transientPaths_div_pos line 31
5. lemma OAI.DirectionalTransience.velocity_of_positive_escape line 37
6. lemma OAI.DirectionalTransience.escape_probability_one_of_velocity line 61
7. lemma OAI.DirectionalTransience.unit_direction_ne_zero line 73