OAI/Probability/Ballisticity/Estimates/SurvivalConditional.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.conditional_survivalViolation_bound line 15
2. lemma OAI.DirectionalTransience.arrayContinuation_shift line 64
3. lemma OAI.DirectionalTransience.actualArrayMap_continuation_ae line 76
4. lemma OAI.DirectionalTransience.OperationalConstants.paddedTimes_int_mono line 100
5. lemma OAI.DirectionalTransience.OperationalConstants.bad_limit_continuation line 109
6. lemma OAI.DirectionalTransience.survivalViolation_shift line 140
7. lemma OAI.DirectionalTransience.survivalViolation_iterate line 147
8. lemma OAI.DirectionalTransience.input_survivalViolation_bound line 156
9. lemma OAI.DirectionalTransience.input_env_mass line 185
10. lemma OAI.DirectionalTransience.actualOccupation_survivalViolation_bound line 192