OAI/Probability/Ballisticity/Estimates/FavorablePairFraction.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.favorable_pair_probability line 13
2. lemma OAI.DirectionalTransience.favorable_fraction_probability line 31
3. lemma OAI.DirectionalTransience.integral_le_of_tail_domination line 71
4. def OAI.DirectionalTransience.capExcessTest line 85
5. lemma OAI.DirectionalTransience.capExcessTest_nonneg line 88
6. lemma OAI.DirectionalTransience.capExcessTest_tail line 91
7. lemma OAI.DirectionalTransience.capExcessTest_tail_empty line 113
8. lemma OAI.DirectionalTransience.capExcess_integral_comparison line 124
9. lemma OAI.DirectionalTransience.capped_tail_le_excess line 143
10. lemma OAI.DirectionalTransience.capExcess_le_scaled_tail line 154