OAI/Probability/Ballisticity/Estimates/DescendingTrials.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.signedHeight_step_ge line 13
2. lemma OAI.DirectionalTransience.integer_first_descent line 18
3. def OAI.DirectionalTransience.BoxStrip line 44
4. lemma OAI.DirectionalTransience.down_hit_disjoint_cross line 47
5. lemma OAI.DirectionalTransience.down_hit_mass_le line 73
6. theorem OAI.DirectionalTransience.quenched_descending_trials line 89