OAI/Probability/Ballisticity/Estimates/NormalizedSharedRestrict.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.normalized_shared_restrict line 125
2. lemma OAI.DirectionalTransience.normalized_independent_restrict line 131
3. lemma OAI.DirectionalTransience.hitWordsEvent_subset_hit line 142
4. theorem OAI.DirectionalTransience.conditioned_prefix_comparison line 151