OAI/Probability/Ballisticity/Estimates/PrefixVariation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.regularPath_cross line 137
2. lemma OAI.DirectionalTransience.hitWordsEvent_compl_on line 142
3. lemma OAI.DirectionalTransience.regularPath_hitWords_cover line 165
4. lemma OAI.DirectionalTransience.prefix_event_real_compl line 181
5. def OAI.DirectionalTransience.prefixVariation line 195
6. lemma OAI.DirectionalTransience.prefixVariation_bound line 203
7. lemma OAI.DirectionalTransience.sharedNoDropMass_tendsto_gap line 259
8. lemma OAI.DirectionalTransience.prefix_error_tendsto_zero line 277