OAI/Probability/Ballisticity/Estimates/SuccessfulScaledTail.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.successfulMedian_scaled_tail_comparison line 14
2. def OAI.DirectionalTransience.unitCap line 72
3. lemma OAI.DirectionalTransience.continuous_unitCap line 75
4. lemma OAI.DirectionalTransience.unitCap_tail line 79
5. lemma OAI.DirectionalTransience.unitCap_coe_of_nonneg line 85
6. def OAI.DirectionalTransience.unitCapLaw line 88
7. lemma OAI.DirectionalTransience.unitCapLaw_tail line 95
8. lemma OAI.DirectionalTransience.unitCapLaw_tail_upper line 108
9. lemma OAI.DirectionalTransience.unitCapLaw_integral_tail_square line 121
10. lemma OAI.DirectionalTransience.raw_capped_tail_moment_transfer line 135