OAI/Probability/Ballisticity/Estimates/MedianAeConst.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.median_eq_of_ae_const line 64
2. lemma OAI.DirectionalTransience.recordMedian_zero line 84
3. theorem OAI.DirectionalTransience.recordMedian_additive_uniform line 95
4. lemma OAI.DirectionalTransience.approximate_additive_linear_on_interval line 150
5. lemma OAI.DirectionalTransience.approximate_additive_common_slope line 203
6. theorem OAI.DirectionalTransience.height_center_linearization line 221
7. lemma OAI.DirectionalTransience.height_center_slope_small line 268