OAI/Probability/Ballisticity/Estimates/PairUpwardRetention.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalTransience.pairUp line 15
2. lemma OAI.DirectionalTransience.rawPairEndpointLaw_upward line 18
3. lemma OAI.DirectionalTransience.rawPairMixture_upward line 38
4. lemma OAI.DirectionalTransience.pairUp_preserves_gap line 53
5. def OAI.DirectionalTransience.upwardRetainedLaw line 59
6. lemma OAI.DirectionalTransience.upwardRetainedLaw_le line 64
7. lemma OAI.DirectionalTransience.upwardRetainedLaw_mass line 75
8. lemma OAI.DirectionalTransience.upwardRetainedLaw_support line 83