OAI/Probability/Ballisticity/Estimates/MeasureAdd.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.inMeasure_add_zero line 165
2. lemma OAI.DirectionalTransience.common_count_fixed_error line 184
3. theorem OAI.DirectionalTransience.transverse_firstHit_fixed_sum_error line 230
4. lemma OAI.DirectionalTransience.fluctuation_tail_bound line 273
5. lemma OAI.DirectionalTransience.double_floor_count_bounds line 296
6. theorem OAI.DirectionalTransience.transverse_bad_radius_spread line 314