OAI/Probability/Ballisticity/Estimates/CellBadEvent.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.cell_bad_event_subset line 12
2. lemma OAI.DirectionalTransience.cells_bad_probability line 44
3. def OAI.DirectionalTransience.stageBadEvent line 83
4. theorem OAI.DirectionalTransience.finite_stage_assembly line 89
5. lemma OAI.DirectionalTransience.noDropProduct_le_raw line 139
6. lemma OAI.DirectionalTransience.fullStream_noDrop_lower line 153
7. theorem OAI.DirectionalTransience.fullStream_small_mass_probability line 165