OAI/Probability/Ballisticity/Estimates/LocalRadiusOrder.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.fluctuationRadius_order_above line 12
2. lemma OAI.DirectionalTransience.fluctuationRadius_stage_order line 27
3. def OAI.DirectionalTransience.episodeScaleRadius line 52
4. structure OAI.DirectionalTransience.OperationalConstants line 56
5. lemma OAI.DirectionalTransience.operational_constants_exist line 86