OAI/Probability/Ballisticity/Estimates/SharedWordCylinderLower.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.shared_wordCylinder_lower line 255
2. lemma OAI.DirectionalTransience.signedHeight_add_step_other line 272
3. lemma OAI.DirectionalTransience.transverse_two_step_hit line 276
4. lemma OAI.DirectionalTransience.direction_one_step_hit line 300
5. lemma OAI.DirectionalTransience.elliptic_raw_gap_growth line 321