OAI/Dynamics/EntropyCounterexample/RegisterEntropyCoding.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem340.RegisterEntropyCoding.netMaxcard_le_card_code line 11
2. theorem OAI.Problem340.RegisterEntropyCoding.netMaxcard_le_register_code line 30
3. theorem OAI.Problem340.RegisterEntropyCoding.netMaxcard_le_of_radius_angle line 60
4. lemma OAI.Problem340.RegisterEntropyCoding.register_bound_le_polynomial line 89
5. theorem OAI.Problem340.RegisterEntropyCoding.netMaxcard_le_card_code_after_one line 99