OAI/Combinatorics/RamseyFive/Trees/TreeExposure.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.TreeCodec.Address line 16
2. instance OAI.SharpRamseyFive.TreeCodec.addressFintype line 20
3. def OAI.SharpRamseyFive.TreeCodec.label line 28
4. def OAI.SharpRamseyFive.TreeCodec.probe line 36
5. theorem OAI.SharpRamseyFive.TreeCodec.probe_event_bound line 48
6. def OAI.SharpRamseyFive.TreeCodec.observe line 93
7. theorem OAI.SharpRamseyFive.TreeCodec.observe_event_bound line 98
8. lemma OAI.SharpRamseyFive.FiniteEntropy.sum_adaptive line 113
9. lemma OAI.SharpRamseyFive.TreeCodec.left_continuation_mean line 126
10. lemma OAI.SharpRamseyFive.TreeCodec.right_continuation_mean line 135
11. def OAI.SharpRamseyFive.TreeCodec.contextAt line 147
12. def OAI.SharpRamseyFive.TreeCodec.pathBudget line 151
13. lemma OAI.SharpRamseyFive.TreeCodec.pathBudget_nonneg line 157
14. theorem OAI.SharpRamseyFive.TreeCodec.context_cost_bound line 167