OAI/Probability/Ballisticity/Crossings/FiniteHitOscillation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.large_finite_difference_step line 156
2. def OAI.DirectionalTransience.FiniteHitOscillation line 182
3. lemma OAI.DirectionalTransience.measurableSet_finiteHitOscillation line 186
4. theorem OAI.DirectionalTransience.conditioned_finite_increment_small line 194
5. theorem OAI.DirectionalTransience.shared_finite_increment_small line 220