OAI/Analysis/MatrixSigning/Realization/VectorRealization.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.Realization.singleton line 13
  2. def OAI.CurrentKS.Realization.joinList line 16
  3. def OAI.CurrentKS.Realization.Realizes.filterCtx line 22
  4. def OAI.CurrentKS.Realization.chooseFold line 36
  5. lemma OAI.CurrentKS.Realization.chooseFold_find line 39
  6. def OAI.CurrentKS.Realization.Realizes.findValue line 47
  7. def OAI.CurrentKS.Realization.zipDefault line 79
  8. def OAI.CurrentKS.Realization.Realizes.zipWith line 82
  9. lemma OAI.CurrentKS.Realization.getD_ofFn line 95
  10. lemma OAI.CurrentKS.Realization.range_map_fin line 100
  11. lemma OAI.CurrentKS.Realization.zipDefault_ofFn line 108
  12. abbrev OAI.CurrentKS.Realization.vectorCode line 117
  13. abbrev OAI.CurrentKS.Realization.matrixCode line 118
  14. abbrev OAI.CurrentKS.Realization.MatrixData line 119
  15. def OAI.CurrentKS.Realization.vectorAdd line 121
  16. def OAI.CurrentKS.Realization.vectorScaleBody line 123
  17. def OAI.CurrentKS.Realization.vectorScale line 126
  18. def OAI.CurrentKS.Realization.matrixAdd line 128
  19. def OAI.CurrentKS.Realization.matrixScale line 130
  20. def OAI.CurrentKS.Realization.dotValue line 132
  21. def OAI.CurrentKS.Realization.dot line 134
  22. def OAI.CurrentKS.Realization.matVecValue line 137
  23. def OAI.CurrentKS.Realization.matVec line 139
  24. def OAI.CurrentKS.Realization.quadraticValue line 144
  25. def OAI.CurrentKS.Realization.quadratic line 146
  26. def OAI.CurrentKS.Realization.matrixData line 151
  27. lemma OAI.CurrentKS.Realization.vectorAdd_ofFn line 154
  28. lemma OAI.CurrentKS.Realization.matrixAdd_data line 158
  29. lemma OAI.CurrentKS.Realization.matrixScale_data line 165
  30. lemma OAI.CurrentKS.Realization.dot_ofFn line 170
  31. lemma OAI.CurrentKS.Realization.matVec_data line 175
  32. lemma OAI.CurrentKS.Realization.quadratic_data line 180