OAI/Analysis/MatrixSigning/Machines/ComplexBridge.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W01.toComplex line 10
  2. theorem OAI.KS.W01.toComplex_re line 12
  3. theorem OAI.KS.W01.toComplex_im line 13
  4. theorem OAI.KS.W01.toComplex_injective line 15
  5. theorem OAI.KS.W01.mem_range_toComplex line 21
  6. def OAI.KS.W01.vectorToComplex line 29
  7. theorem OAI.KS.W01.vectorToComplex_injective line 32
  8. def OAI.KS.W01.encodeEntries line 38
  9. def OAI.KS.W01.readEntriesN line 41
  10. theorem OAI.KS.W01.readEntriesN_flatMap_append line 48
  11. def OAI.KS.W01.readEntries line 55
  12. theorem OAI.KS.W01.readEntries_encode_append line 59
  13. theorem OAI.KS.W01.encodeEntries_injective line 63
  14. def OAI.KS.W01.encodeVector line 71
  15. theorem OAI.KS.W01.encodeVector_injective line 74
  16. theorem OAI.KS.W01.encodeComplex_length_pos line 80
  17. theorem OAI.KS.W01.entries_count_le_bits line 84