OAI/Probability/Ballisticity/Renewal/DurationMoment.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.conditioned_wordDuration_integrable line 13
2. lemma OAI.DirectionalTransience.conditioned_wordDuration_mean_positive line 24
3. lemma OAI.DirectionalTransience.conditioned_word_temporal_strong_law line 39
4. lemma OAI.DirectionalTransience.scalar_cut_speed line 63
5. def OAI.DirectionalTransience.VelocityPaths line 122

   Also declared: ComparatorChallenges/VelocityHemisphere.lean:82 (same declaration text).

6. lemma OAI.DirectionalTransience.measurableSet_velocityPaths line 125
7. lemma OAI.DirectionalTransience.velocityPaths_of_suffix line 131
8. lemma OAI.DirectionalTransience.conditioned_to_annealed_velocity line 155