OAI/Probability/Ballisticity/Estimates/ScaledMaxMoment.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.sq_min_nonneg line 14
2. lemma OAI.DirectionalTransience.cappedMoment_scaled_eq line 20
3. lemma OAI.DirectionalTransience.iid_scaled_max_moment_le line 31
4. lemma OAI.DirectionalTransience.scaled_max_moment_ratio_bound line 42
5. lemma OAI.DirectionalTransience.successful_small_variance_bound line 73
6. lemma OAI.DirectionalTransience.exists_block_count line 129
7. lemma OAI.DirectionalTransience.eventually_ceil_horizon_covered line 141