OAI/InformationTheory/DimensionTen/StateKey.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Dimension-ten key bounds for finite total terminal readouts and their trace-norm closure.

  1. lemma OAI.DimensionTen.rho_inClass line 16
  2. def OAI.DimensionTen.SecretBitSeparation line 38
  3. def OAI.DimensionTen.CompletedBitSeparation line 63
  4. lemma OAI.DimensionTen.secretBitSeparation_of_inClass line 70
  5. lemma OAI.DimensionTen.completedBitSeparation_of_inClass line 79
  6. theorem OAI.DimensionTen.main_state line 86