OAI/Probability/Ballisticity/Estimates/RawDropBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.OperationalConstants.dropCut_integrable line 16
2. lemma OAI.DirectionalTransience.OperationalConstants.raw_dropCut_integral line 26
3. lemma OAI.DirectionalTransience.OperationalConstants.shortDrop_integrable line 51
4. lemma OAI.DirectionalTransience.OperationalConstants.raw_dropCut_lower line 60
5. lemma OAI.DirectionalTransience.OperationalConstants.raw_dropCut_upper line 98
6. lemma OAI.DirectionalTransience.mark_lintegral_bound_of_weak_limit line 141
7. lemma OAI.DirectionalTransience.mark_integrable_of_lintegral_bound line 171