OAI/InformationTheory/Entanglement/FirstBitLaw.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SecretKey.uniformKeyLaw line 13
2. lemma OAI.SecretKey.uniformKeyLaw_value line 19
3. lemma OAI.SecretKey.firstBitPush_value line 26
4. lemma OAI.SecretKey.firstBitPush_ideal_value line 33
5. theorem OAI.SecretKey.first_bit_contract line 49