OAI/InformationTheory/SecretKey/DimensionTenModel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The normalized Choi state and key separation in the finite terminal-readout model.

  1. def OAI.ZeroKey.TenDimensional.rho line 15
  2. def OAI.ZeroKey.TenDimensional.MainClaim line 18