OAI/InformationTheory/Entanglement/HermitianBanach.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SecretKey.hermitianTraceClass_real_smul line 11
  2. lemma OAI.SecretKey.hilbertTraceNorm_real_smul line 19
  3. lemma OAI.SecretKey.hilbertTraceNorm_nonneg line 25
  4. lemma OAI.SecretKey.opNorm_le_traceNorm line 28
  5. def OAI.SecretKey.hermitianTraceSpace line 32
  6. def OAI.SecretKey.HermitianTrace line 38
  7. instance OAI.SecretKey.HermitianTrace.hermitianTraceAddCommGroup line 41
  8. instance OAI.SecretKey.HermitianTrace.hermitianTraceModule line 42
  9. def OAI.SecretKey.HermitianTrace.operator line 43
  10. lemma OAI.SecretKey.HermitianTrace.property line 44
  11. instance OAI.SecretKey.HermitianTrace.hermitianTraceNorm line 45
  12. lemma OAI.SecretKey.HermitianTrace.operator_add line 46
  13. lemma OAI.SecretKey.HermitianTrace.operator_sub line 47
  14. lemma OAI.SecretKey.HermitianTrace.operator_smul line 48
  15. lemma OAI.SecretKey.HermitianTrace.operator_zero line 49
  16. lemma OAI.SecretKey.HermitianTrace.norm_eq line 50
  17. lemma OAI.SecretKey.HermitianTrace.core line 51
  18. instance OAI.SecretKey.HermitianTrace.hermitianTraceNormedAddCommGroup line 62
  19. instance OAI.SecretKey.HermitianTrace.hermitianTraceNormedSpace line 63
  20. def OAI.SecretKey.HermitianTrace.inclusion line 65
  21. lemma OAI.SecretKey.traceNorm_fatou_bound line 74
  22. instance OAI.SecretKey.HermitianTrace.completeSpace line 99