OAI/InformationTheory/Entanglement/HermitianInstrument.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SecretKey.HermitianTrace.asTraceClass line 16
  2. lemma OAI.SecretKey.HermitianTrace.asTraceClass_operator line 21
  3. lemma OAI.SecretKey.HermitianTrace.asTraceClass_add line 22
  4. lemma OAI.SecretKey.HermitianTrace.asTraceClass_smul line 23
  5. instance OAI.SecretKey.HermitianTrace.(instance at line 27) line 27
  6. instance OAI.SecretKey.HermitianTrace.(instance at line 28) line 28
  7. lemma OAI.SecretKey.TraceInstrument.event_positive_trace_bound line 35
  8. lemma OAI.SecretKey.TraceInstrument.event_traceNorm_bound line 49
  9. def OAI.SecretKey.TraceInstrument.hermitianEventApply line 66
  10. lemma OAI.SecretKey.TraceInstrument.hermitianEventApply_add line 72
  11. lemma OAI.SecretKey.TraceInstrument.hermitianEventApply_smul line 79
  12. def OAI.SecretKey.TraceInstrument.hermitianEventLinear line 86
  13. lemma OAI.SecretKey.TraceInstrument.hermitianEventLinear_norm line 90
  14. def OAI.SecretKey.TraceInstrument.hermitianEvent line 97
  15. lemma OAI.SecretKey.TraceInstrument.event_integral line 101