OAI/Probability/Ballisticity/Crossings/OffDiagonalCenteredCross.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.abs_le_abs_sub_add line 15
2. def OAI.DirectionalTransience.centeredClipCross line 20
3. lemma OAI.DirectionalTransience.measurable_centeredClipCross line 25
4. lemma OAI.DirectionalTransience.centeredClipCross_bound line 31
5. lemma OAI.DirectionalTransience.shared_centered_cross_eventual_bound line 37
6. lemma OAI.DirectionalTransience.same_height_separated_exists line 89
7. lemma OAI.DirectionalTransience.uniform_eventually_of_dependent_sequences line 99
8. lemma OAI.DirectionalTransience.shared_centered_cross_uniform_bound line 115