OAI/Probability/Ballisticity/Estimates/CellAttempt.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalTransience.cellSeedMass line 13
2. def OAI.DirectionalTransience.cellEarlyMass line 17
3. def OAI.DirectionalTransience.cellEarlyProfile line 22
4. lemma OAI.DirectionalTransience.cellSeedMass_measurable line 31
5. lemma OAI.DirectionalTransience.cellEarlyMass_measurable line 51
6. lemma OAI.DirectionalTransience.cellEarlyProfile_measurable line 69
7. lemma OAI.DirectionalTransience.cellEarlyProfile_retained line 81
8. def OAI.DirectionalTransience.failedOpportunityBlocks line 120
9. lemma OAI.DirectionalTransience.failedOpportunityBlocks_bound line 124
10. theorem OAI.DirectionalTransience.opportunity_exhaustion_probability line 144