OAI/Probability/Ballisticity/Estimates/CappedLoss.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalTransience.cappedLogLoss line 12
2. lemma OAI.DirectionalTransience.cappedLogLoss_bounds line 15
3. lemma OAI.DirectionalTransience.lt_cappedLogLoss_iff line 23
4. lemma OAI.DirectionalTransience.measurable_cappedLogLoss line 45
5. lemma OAI.DirectionalTransience.integrable_cappedLogLoss line 52
6. lemma OAI.DirectionalTransience.integrable_exp_cappedLogLoss line 61
7. lemma OAI.DirectionalTransience.exp_moment_of_tail line 81
8. lemma OAI.DirectionalTransience.exp_le_half_exp line 145
9. lemma OAI.DirectionalTransience.late_step_tail_arithmetic line 152