OAI/Analysis/MatrixSigning/Realization/VarianceRealization.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CurrentKS.Realization.MatrixGrid line 13
  2. abbrev OAI.CurrentKS.Realization.matrixGridDataCode line 17
  3. def OAI.CurrentKS.Realization.MatrixGrid.data line 18
  4. def OAI.CurrentKS.Realization.matrixGridCode line 19
  5. def OAI.CurrentKS.Realization.mgView line 20
  6. def OAI.CurrentKS.Realization.mgN line 22
  7. def OAI.CurrentKS.Realization.mgRest line 23
  8. def OAI.CurrentKS.Realization.mgM line 24
  9. def OAI.CurrentKS.Realization.mgDen line 25
  10. def OAI.CurrentKS.Realization.MatrixGrid.test line 26
  11. def OAI.CurrentKS.Realization.mgShift line 29
  12. def OAI.CurrentKS.Realization.mgTest line 41
  13. abbrev OAI.CurrentKS.Realization.gridStateCode line 47
  14. def OAI.CurrentKS.Realization.gridStepData line 48
  15. def OAI.CurrentKS.Realization.gridStep line 50
  16. lemma OAI.CurrentKS.Realization.grid_iterate line 58
  17. def OAI.CurrentKS.Realization.gridUpper line 66
  18. lemma OAI.CurrentKS.Realization.foldAdd_matrixData line 75
  19. lemma OAI.CurrentKS.Realization.matrix_fold_sum line 84
  20. def OAI.CurrentKS.Realization.fVariance line 91
  21. def OAI.CurrentKS.Realization.fVarianceGrid line 105
  22. def OAI.CurrentKS.Realization.varianceQuery line 118
  23. def OAI.CurrentKS.Realization.faceNormalized line 121
  24. def OAI.CurrentKS.Realization.normalizedRun line 129