OAI/Analysis/MatrixSigning/Realization/OriginalSignRealization.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.Realization.recordTraceData line 12
  2. def OAI.CurrentKS.Realization.recordTrace line 15
  3. lemma OAI.CurrentKS.Realization.recordTrace_data line 20
  4. def OAI.CurrentKS.Realization.originalTrace line 29
  5. def OAI.CurrentKS.Realization.originalTraces line 32
  6. def OAI.CurrentKS.Realization.originalScale line 35
  7. def OAI.CurrentKS.Realization.originalOrientation line 37
  8. def OAI.CurrentKS.Realization.nonzeroIndicesData line 42
  9. def OAI.CurrentKS.Realization.nonzeroIndices line 44
  10. lemma OAI.CurrentKS.Realization.nonzeroIndices_data line 52
  11. def OAI.CurrentKS.Realization.originalIndices line 65
  12. abbrev OAI.CurrentKS.Realization.originalCount line 68
  13. def OAI.CurrentKS.Realization.originalCountRealizes line 70
  14. def OAI.CurrentKS.Realization.originalIndex line 73
  15. def OAI.CurrentKS.Realization.originalNormalizedMatrix line 81
  16. def OAI.CurrentKS.Realization.originalFace line 99
  17. def OAI.CurrentKS.Realization.originalFaceRealizes line 102
  18. def OAI.CurrentKS.Realization.originalNormalizedSigns line 108
  19. def OAI.CurrentKS.Realization.originalExtendedSigns line 112
  20. def OAI.CurrentKS.Realization.originalOutputBit line 120
  21. def OAI.CurrentKS.Realization.originalSigningFramed line 129