OAI/Probability/Ballisticity/Crossings/NearCrossEstimates.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.normalJointPast_weighted_square_integrable line 14
2. lemma OAI.DirectionalTransience.normalJointPast_near_cross line 24
3. def OAI.DirectionalTransience.SeparatedCrossBound line 57
4. lemma OAI.DirectionalTransience.normalJointPast_cross_bound line 66