OAI/Probability/Ballisticity/Estimates/ScheduledCellSuccess.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalTransience.scheduledCellSuccess line 13
2. lemma OAI.DirectionalTransience.scheduledCellSuccess_or_failure line 27
3. lemma OAI.DirectionalTransience.no_cell_success_subset_exhaustion line 45
4. theorem OAI.DirectionalTransience.actual_cell_no_success line 59
5. lemma OAI.DirectionalTransience.budget_profile_prefix_certificate line 90
6. theorem OAI.DirectionalTransience.protection_prefix_certificate line 100
7. theorem OAI.DirectionalTransience.protection_prefix_after_retention line 124