OAI/InformationTheory/Entanglement/HilbertChannel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SecretKey.cp_trace_positive line 14
2. structure OAI.SecretKey.TraceChannel line 30
3. lemma OAI.SecretKey.finitePositiveTrace_add line 35
4. theorem OAI.SecretKey.hilbertTraceNorm_triangle line 41
5. lemma OAI.SecretKey.TraceChannel.positive line 60
6. lemma OAI.SecretKey.TraceChannel.real_trace line 64
7. theorem OAI.SecretKey.TraceChannel.traceNorm_contract line 68