OAI/InformationTheory/Entanglement/HilbertLawDistance.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SecretKey.hilbertVariation line 15
  2. lemma OAI.SecretKey.variation_le_hilbertVariation line 18
  3. def OAI.SecretKey.hilbertIdeal line 30
  4. lemma OAI.SecretKey.hilbertIdeal_positive line 32
  5. lemma OAI.SecretKey.hilbertErase_ideal line 40
  6. def OAI.SecretKey.hilbertCQDistance line 51
  7. theorem OAI.SecretKey.hilbertCQDistance_recovery line 55