OAI/Analysis/MatrixSigning/Realization/ValueEvalRealization.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CurrentKS.Realization.ValueEvalData line 11
  2. abbrev OAI.CurrentKS.Realization.valueEvalCode line 12
  3. def OAI.CurrentKS.Realization.veP line 13
  4. def OAI.CurrentKS.Realization.veY line 14
  5. def OAI.CurrentKS.Realization.veD line 15
  6. def OAI.CurrentKS.Realization.veN line 16
  7. def OAI.CurrentKS.Realization.veEye line 17
  8. def OAI.CurrentKS.Realization.veEps line 18
  9. def OAI.CurrentKS.Realization.veTime line 20
  10. def OAI.CurrentKS.Realization.veVariable line 22
  11. def OAI.CurrentKS.Realization.sumData line 24
  12. def OAI.CurrentKS.Realization.veSum line 25
  13. lemma OAI.CurrentKS.Realization.sumData_value line 27
  14. def OAI.CurrentKS.Realization.etaData line 31
  15. def OAI.CurrentKS.Realization.eta line 34
  16. lemma OAI.CurrentKS.Realization.etaData_value line 42
  17. def OAI.CurrentKS.Realization.matrixAddData line 50
  18. def OAI.CurrentKS.Realization.matrixScaleData line 52
  19. def OAI.CurrentKS.Realization.eyeData line 53
  20. def OAI.CurrentKS.Realization.schurEvalData line 55
  21. def OAI.CurrentKS.Realization.schurEval line 61
  22. lemma OAI.CurrentKS.Realization.time_getD line 67
  23. lemma OAI.CurrentKS.Realization.schurEval_data line 73
  24. def OAI.CurrentKS.Realization.lowerBoxData line 84
  25. def OAI.CurrentKS.Realization.lowerBox line 86
  26. def OAI.CurrentKS.Realization.upperBoxData line 89
  27. def OAI.CurrentKS.Realization.upperBox line 91
  28. def OAI.CurrentKS.Realization.tinyMatrix line 94
  29. lemma OAI.CurrentKS.Realization.tinyMatrix_data line 96
  30. def OAI.CurrentKS.Realization.valueEvalData line 99
  31. def OAI.CurrentKS.Realization.Realizes.blockWith line 105
  32. def OAI.CurrentKS.Realization.valueEval line 109
  33. lemma OAI.CurrentKS.Realization.lowerBox_data line 114
  34. lemma OAI.CurrentKS.Realization.upperBox_data line 122
  35. lemma OAI.CurrentKS.Realization.pencil_blockDiagonal_eval line 131
  36. lemma OAI.CurrentKS.Realization.valueEval_data line 139