OAI/Probability/Ballisticity/Estimates/RadixBudget.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.radix16_budget_ratio line 12
2. lemma OAI.DirectionalTransience.adapted_weighted_product_moment line 63
3. lemma OAI.DirectionalTransience.adapted_weighted_exp_sum_tail line 83
4. def OAI.DirectionalTransience.lateBudget line 133
5. lemma OAI.DirectionalTransience.lateBudget_pos line 135
6. lemma OAI.DirectionalTransience.lateBudget_sum_le line 138
7. lemma OAI.DirectionalTransience.lateBudget_gaps line 155
8. lemma OAI.DirectionalTransience.fixed_budget_momentENN line 170
9. theorem OAI.DirectionalTransience.scheduled_late_step_bounds line 184