OAI/Probability/Ballisticity/Estimates/GlobalTuple.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.globalEndpointProfile_support line 13
2. def OAI.DirectionalTransience.globalTupleProfile line 27
3. lemma OAI.DirectionalTransience.globalTupleProfile_mass line 36
4. lemma OAI.DirectionalTransience.globalTupleProfile_measurable_below line 52
5. lemma OAI.DirectionalTransience.injection_candidate_unique line 73
6. lemma OAI.DirectionalTransience.finite_injection_choice line 88