OAI/InformationTheory/Entanglement/HilbertMeasureEmbedding.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SecretKey.hilbertTrace_real_smul line 15
2. lemma OAI.SecretKey.hilbertCompress_smul line 20
3. lemma OAI.SecretKey.hilbertErase_real_smul line 25
4. lemma OAI.SecretKey.finitePositiveTrace_real_smul line 31
5. lemma OAI.SecretKey.PositiveMatrixMeasure.ext_entry line 42
6. def OAI.SecretKey.PositiveMatrixMeasure.hilbertEmbedding line 47
7. lemma OAI.SecretKey.PositiveMatrixMeasure.hilbertEmbedding_recovered line 63