OAI/Probability/Ballisticity/Estimates/UniformLowerMass.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.DirectionalTransience.uniform_lower_mass_from_sequencesline 13 - theorem
OAI.DirectionalTransience.clipping_uniform_originline 43 - lemma
OAI.DirectionalTransience.quenchedTube_translationline 89 - lemma
OAI.DirectionalTransience.quenchedTube_probability_translationline 97 - lemma
OAI.DirectionalTransience.quenchedTube_zeroline 111 - theorem
OAI.DirectionalTransience.clipping_uniformline 118