OAI/InformationTheory/Entanglement/HilbertLawMetric.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SecretKey.hilbertENorm_add_le line 13
  2. lemma OAI.SecretKey.hilbertVariation_congr line 19
  3. lemma OAI.SecretKey.hilbertVariation_add_le line 29
  4. lemma OAI.SecretKey.hilbertVariation_neg line 43
  5. lemma OAI.SecretKey.hilbertVariation_difference_comm line 46
  6. theorem OAI.SecretKey.hilbertVariation_difference_triangle line 54
  7. def OAI.SecretKey.hilbertClassicalDistance line 67
  8. lemma OAI.SecretKey.hilbertClassicalDistance_ne_top line 70
  9. lemma OAI.SecretKey.hilbertClassicalDistance_triangle line 75
  10. lemma OAI.SecretKey.hilbertClassicalDistance_le_two line 81