OAI/InformationTheory/AmplitudeDamping/CapacityConverse.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GAD.codeEnsemble line 12
2. theorem OAI.GAD.code_success_dim_bound line 22
3. theorem OAI.GAD.code_messages_bound line 33
4. theorem OAI.GAD.code_entropy_bound line 44
5. theorem OAI.GAD.code_log_dimension_bound line 66
6. theorem OAI.GAD.code_log_rate_bound line 80
7. theorem OAI.GAD.achievable_upper line 107