OAI/InformationTheory/Entanglement/CPBlocks.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SecretKey.cp_pure_block line 13
2. lemma OAI.SecretKey.cp_filtered_bound line 32
3. lemma OAI.SecretKey.cp_filtered_reverse line 44
4. lemma OAI.SecretKey.trace_filter line 55
5. lemma OAI.SecretKey.trace_psd_product_nonneg line 60
6. lemma OAI.SecretKey.cp_effect_direct line 65
7. lemma OAI.SecretKey.cp_effect_reverse line 74