OAI/InformationTheory/SecretKey/DimensionTen.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Key separation for the dimension-ten state in the finite terminal-readout model.

  1. lemma OAI.ZeroKey.TenDimensional.rho_density line 18
  2. lemma OAI.ZeroKey.TenDimensional.trace_ne_zero line 20
  3. lemma OAI.ZeroKey.TenDimensional.rho_not_separable line 23
  4. lemma OAI.ZeroKey.TenDimensional.rho_productfree line 25
  5. def OAI.ZeroKey.TenDimensional.TransferInput line 30
  6. def OAI.ZeroKey.TenDimensional.PPTInput line 33
  7. lemma OAI.ZeroKey.TenDimensional.rho_inClass_conditional line 36
  8. theorem OAI.ZeroKey.TenDimensional.main_state_conditional line 43
  9. theorem OAI.ZeroKey.TenDimensional.pptInput line 59
  10. theorem OAI.ZeroKey.TenDimensional.transferInput line 62
  11. theorem OAI.ZeroKey.TenDimensional.rho_inClass line 66
  12. theorem OAI.ZeroKey.TenDimensional.main_state line 69