OAI/Probability/Ballisticity/Estimates/RecordPrefixControl.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.fixed_real_tail_small line 174
2. def OAI.DirectionalTransience.recordPrefixControl line 189
3. lemma OAI.DirectionalTransience.measurable_recordPrefixControl line 195
4. lemma OAI.DirectionalTransience.recordPrefixControl_prefix line 206
5. lemma OAI.DirectionalTransience.recordPrefixControl_endpoint line 218
6. lemma OAI.DirectionalTransience.medianTube_suffix_subset_ae line 227