OAI/Probability/Ballisticity/Estimates/CurvePolicyMaximal.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.curvePolicy_average_lateral_bound line 15
2. lemma OAI.DirectionalTransience.curvePolicy_event_iid line 29
3. lemma OAI.DirectionalTransience.curvePolicy_maximal_tail line 48
4. lemma OAI.DirectionalTransience.policySafe_iff line 74
5. lemma OAI.DirectionalTransience.curvePolicy_word_height line 90
6. lemma OAI.DirectionalTransience.signedHeight_sum_of_constant line 116
7. lemma OAI.DirectionalTransience.finitePolicyPMF_take line 135
8. def OAI.DirectionalTransience.priorRows line 154
9. lemma OAI.DirectionalTransience.finitePolicyPMF_prior_local line 157
10. lemma OAI.DirectionalTransience.disjoint_prior_rows line 175
11. lemma OAI.DirectionalTransience.finitePolicyPMF_fresh_test line 182