OAI/Analysis/FourierLLogL/Procedure/Tree.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FourierLLogL.Dyadic.Procedure.top_avg line 15
2. lemma OAI.FourierLLogL.Dyadic.Procedure.lose_eq line 20
3. lemma OAI.FourierLLogL.Dyadic.Procedure.win_eq line 23
4. lemma OAI.FourierLLogL.Dyadic.Procedure.split_pos line 27
5. def OAI.FourierLLogL.Dyadic.Procedure.bonus line 37
6. def OAI.FourierLLogL.Dyadic.Procedure.playing line 39
7. def OAI.FourierLLogL.Dyadic.Procedure.totalUse line 42
8. def OAI.FourierLLogL.Dyadic.Procedure.stage line 43
9. lemma OAI.FourierLLogL.Dyadic.Procedure.begin_ok line 46
10. theorem OAI.FourierLLogL.Dyadic.Procedure.plant line 58