OAI/InformationTheory/Entanglement/HilbertVectorMeasure.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SecretKey.HermitianTrace.coefficient line 14
  2. lemma OAI.SecretKey.HermitianTrace.coefficient_apply line 17
  3. lemma OAI.SecretKey.HermitianTrace.ext_coefficient line 19
  4. def OAI.SecretKey.PositiveHilbertMeasure.traceValue line 28
  5. lemma OAI.SecretKey.PositiveHilbertMeasure.traceValue_operator line 32
  6. lemma OAI.SecretKey.PositiveHilbertMeasure.traceValue_coefficient line 35
  7. lemma OAI.SecretKey.PositiveHilbertMeasure.traceValue_norm line 38
  8. lemma OAI.SecretKey.PositiveHilbertMeasure.traceValue_empty line 42
  9. lemma OAI.SecretKey.PositiveHilbertMeasure.traceValue_hasSum line 47
  10. def OAI.SecretKey.PositiveHilbertMeasure.traceVectorMeasure line 61
  11. lemma OAI.SecretKey.PositiveHilbertMeasure.traceVectorMeasure_apply line 66
  12. lemma OAI.SecretKey.PositiveHilbertMeasure.traceVectorMeasure_coefficient line 67