OAI/InformationTheory/Entanglement/HilbertTraceIdeal.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SecretKey.symmetric_bessel_trace line 13
2. lemma OAI.SecretKey.positive_contraction_family_trace line 33
3. def OAI.SecretKey.positiveSupportApprox line 51
4. lemma OAI.SecretKey.positiveSupportApprox_continuous line 53
5. lemma OAI.SecretKey.positiveSupportApprox_norm line 58
6. lemma OAI.SecretKey.positiveSupportApprox_error line 64
7. lemma OAI.SecretKey.positiveSupportApprox_operator line 80