OAI/Analysis/MatrixSigning/Realization/RoundedStepRealization.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CurrentKS.Realization.StepParameters line 13
  2. abbrev OAI.CurrentKS.Realization.stepParametersCode line 14
  3. abbrev OAI.CurrentKS.Realization.UpdateData line 15
  4. abbrev OAI.CurrentKS.Realization.updateCode line 16
  5. def OAI.CurrentKS.Realization.roundedUpdateValue line 18
  6. def OAI.CurrentKS.Realization.roundedUpdate line 23
  7. lemma OAI.CurrentKS.Realization.roundedUpdate_ofFn line 35
  8. structure OAI.CurrentKS.Realization.PencilState line 48
  9. abbrev OAI.CurrentKS.Realization.pencilStateDataCode line 56
  10. def OAI.CurrentKS.Realization.pencilStateData line 57
  11. def OAI.CurrentKS.Realization.pencilStateCode line 59
  12. def OAI.CurrentKS.Realization.stateView line 61
  13. def OAI.CurrentKS.Realization.statePencil line 64
  14. def OAI.CurrentKS.Realization.stateParameters line 66
  15. def OAI.CurrentKS.Realization.stateY line 69
  16. def OAI.CurrentKS.Realization.stateWitness line 73
  17. lemma OAI.CurrentKS.Realization.nonempty_witness_dimension line 86
  18. def OAI.CurrentKS.Realization.stateNextVector line 92
  19. def OAI.CurrentKS.Realization.PencilState.next line 110
  20. def OAI.CurrentKS.Realization.pencilNext line 113