OAI/Probability/Ballisticity/Walk/QuenchedRegularPathAe.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.quenched_regularPath_ae line 203
2. lemma OAI.DirectionalTransience.relativeGoodMass_le_tubePrefix line 211
3. lemma OAI.DirectionalTransience.integral_tubePrefix_lower_bound line 232
4. theorem OAI.DirectionalTransience.slope_tube_single_threat line 245