OAI/InformationTheory/Entanglement/HilbertLawAlgebra.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SecretKey.finitePositiveTrace_sum line 13
  2. lemma OAI.SecretKey.hermitianTraceClass_sum line 21
  3. lemma OAI.SecretKey.hilbertTrace_sum line 30
  4. def OAI.SecretKey.PositiveHilbertMeasure.familySum line 43
  5. lemma OAI.SecretKey.PositiveHilbertMeasure.familySum_value line 56
  6. def OAI.SecretKey.PositiveHilbertMeasure.scale line 59
  7. lemma OAI.SecretKey.PositiveHilbertMeasure.scale_value line 73
  8. lemma OAI.SecretKey.hilbertVariation_zero line 76
  9. lemma OAI.SecretKey.hilbertVariation_sum_le line 79