OAI/Analysis/MatrixSigning/Matrices/Space.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CurrentKS.HermitianCoordinates.Space line 17
  2. def OAI.CurrentKS.HermitianCoordinates.decode line 21
  3. def OAI.CurrentKS.HermitianCoordinates.encode line 24
  4. lemma OAI.CurrentKS.HermitianCoordinates.decode_hermitian line 27
  5. def OAI.CurrentKS.HermitianCoordinates.assemble line 38
  6. def OAI.CurrentKS.HermitianCoordinates.extract line 39
  7. lemma OAI.CurrentKS.HermitianCoordinates.extract_assemble line 41
  8. lemma OAI.CurrentKS.HermitianCoordinates.assemble_extract line 49
  9. lemma OAI.CurrentKS.HermitianCoordinates.decode_add line 74
  10. lemma OAI.CurrentKS.HermitianCoordinates.decode_smul line 81
  11. def OAI.CurrentKS.HermitianCoordinates.assembleLinear line 89
  12. lemma OAI.CurrentKS.HermitianCoordinates.norm_decode_entry line 94
  13. lemma OAI.CurrentKS.HermitianCoordinates.norm_assemble_sq line 107
  14. lemma OAI.CurrentKS.HermitianCoordinates.norm_assemble line 120
  15. def OAI.CurrentKS.HermitianCoordinates.assembleCLM line 130
  16. lemma OAI.CurrentKS.HermitianCoordinates.norm_assembleCLM line 133