OAI/Dynamics/EntropyCounterexample/EntropyCoding.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Problem340.EntropyCoding.SparseCode line 7
2. theorem OAI.Problem340.EntropyCoding.card_sparseCode_le line 10
3. theorem OAI.Problem340.EntropyCoding.exists_dynCover_of_finite_code line 37
4. def OAI.Problem340.EntropyCoding.center line 53
5. theorem OAI.Problem340.EntropyCoding.exists_dynCover_of_sparse_code line 58
6. theorem OAI.Problem340.EntropyCoding.card_filter_fin_eq_range line 83
7. def OAI.Problem340.EntropyCoding.exceptionalBlocks line 99
8. theorem OAI.Problem340.EntropyCoding.exists_dynCover_of_sparse_visits line 104
9. theorem OAI.Problem340.EntropyCoding.coverMincard_le_of_sparse_visits line 136