OAI/Probability/Ballisticity/Renewal/VelocityWords.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalTransience.renewalVelocity line 12
2. lemma OAI.DirectionalTransience.conditioned_velocity_from_duration line 16
3. lemma OAI.DirectionalTransience.renewalVelocity_projection line 44
4. lemma OAI.DirectionalTransience.velocity_from_integrable_words line 63
5. lemma OAI.DirectionalTransience.signed_coordinate_ballisticity line 75
6. lemma OAI.DirectionalTransience.velocityPaths_projection line 92
7. lemma OAI.DirectionalTransience.conditioned_word_height_strong_law line 99
8. lemma OAI.DirectionalTransience.velocity_positive_original_direction line 112
9. theorem OAI.DirectionalTransience.directional_transience_implies_ballisticity_unit line 152