OAI/Probability/Ballisticity/Walk/ProfileGrowth2.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalTransience.HorizontalLayer line 13
2. instance OAI.DirectionalTransience.(instance at line 15) line 15
3. instance OAI.DirectionalTransience.(instance at line 16) line 16
4. instance OAI.DirectionalTransience.(instance at line 17) line 17
5. lemma OAI.DirectionalTransience.horizontal_coordinate_surjective line 19
6. def OAI.DirectionalTransience.horizontalCoordinateKernel line 26
7. instance OAI.DirectionalTransience.horizontalCoordinateKernel_finite line 31
8. lemma OAI.DirectionalTransience.horizontalCoordinateKernel_apply line 36
9. lemma OAI.DirectionalTransience.horizontalCoordinateKernel_total line 44
10. lemma OAI.DirectionalTransience.coordinate_outwardMass line 50
11. lemma OAI.DirectionalTransience.horizontal_pair_height line 65
12. theorem OAI.DirectionalTransience.actual_profile_tail_growth line 72