OAI/Analysis/MatrixSigning/Realization/ValueDataRealization.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CurrentKS.Realization.ValueData line 13
  2. abbrev OAI.CurrentKS.Realization.valueDataCode line 14
  3. def OAI.CurrentKS.Realization.vdD line 16
  4. def OAI.CurrentKS.Realization.vdRest line 17
  5. def OAI.CurrentKS.Realization.vdAtoms line 18
  6. def OAI.CurrentKS.Realization.vdParams line 19
  7. def OAI.CurrentKS.Realization.vdX line 20
  8. def OAI.CurrentKS.Realization.vdTheta line 21
  9. def OAI.CurrentKS.Realization.vdEps line 22
  10. def OAI.CurrentKS.Realization.realDimension line 23
  11. def OAI.CurrentKS.Realization.valueDimension line 25
  12. def OAI.CurrentKS.Realization.valueData line 29
  13. abbrev OAI.CurrentKS.Realization.matrixVarCode line 33
  14. def OAI.CurrentKS.Realization.coordinateIndex line 35
  15. def OAI.CurrentKS.Realization.coordinateIndexRealizes line 37
  16. lemma OAI.CurrentKS.Realization.coordinateIndex_value line 48
  17. def OAI.CurrentKS.Realization.coordinateEntry line 57
  18. def OAI.CurrentKS.Realization.coordinateData line 69
  19. def OAI.CurrentKS.Realization.coordinates line 72
  20. def OAI.CurrentKS.Realization.matrixVariableData line 76
  21. def OAI.CurrentKS.Realization.matrixVariable line 78
  22. lemma OAI.CurrentKS.Realization.coordinates_data line 81
  23. lemma OAI.CurrentKS.Realization.matrixVariable_data line 92
  24. def OAI.CurrentKS.Realization.weightedSumData line 97
  25. def OAI.CurrentKS.Realization.weightedSum line 100
  26. lemma OAI.CurrentKS.Realization.weightedSum_data line 105
  27. def OAI.CurrentKS.Realization.sandwichData line 117
  28. def OAI.CurrentKS.Realization.sandwich line 119
  29. lemma OAI.CurrentKS.Realization.sandwich_data line 121