OAI/Probability/Ballisticity/Estimates/MeasurableCountableSample.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TailDecorrelation.measurable_countable_sample line 21
2. lemma OAI.TailDecorrelation.sampled_exponential_integrable line 28
3. lemma OAI.TailDecorrelation.sampled_locality line 57
4. lemma OAI.TailDecorrelation.sampled_entropy_decorrelation line 77
5. lemma OAI.TailDecorrelation.limsup_le_of_nonneg_eventual line 107
6. lemma OAI.DirectionalTransience.analytic_rows_eq line 125
7. lemma OAI.DirectionalTransience.pair_neighborhoods_escape line 129
8. lemma OAI.DirectionalTransience.integrable_and_mean_le_of_exp line 149
9. theorem OAI.DirectionalTransience.actual_sampled_tail_decorrelation line 174