OAI/InformationTheory/Entanglement/HilbertTrace.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SecretKey.hilbertTrace line 12
  2. def OAI.SecretKey.HasFinitePositiveTrace line 15
  3. lemma OAI.SecretKey.hilbert_parseval line 19
  4. lemma OAI.SecretKey.positive_diagonal_sqrt line 28
  5. lemma OAI.SecretKey.symmetric_finite_compression_trace line 39
  6. lemma OAI.SecretKey.positive_finite_compression_trace line 63
  7. lemma OAI.SecretKey.positiveTrace_change_basis line 73
  8. lemma OAI.SecretKey.hilbertTrace_add line 86
  9. lemma OAI.SecretKey.hilbertTrace_sub line 93
  10. lemma OAI.SecretKey.finitePositiveTrace_of_le line 100
  11. def OAI.SecretKey.hilbertTraceNorm line 110
  12. def OAI.SecretKey.HermitianTraceClass line 112
  13. lemma OAI.SecretKey.hermitian_parts_finite line 114
  14. lemma OAI.SecretKey.hilbertTraceNorm_jordan line 122