OAI/Analysis/MatrixSigning/Realization/EndpointRealization.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CurrentKS.Realization.vectorUpdateCode line 14
  2. def OAI.CurrentKS.Realization.updateData line 15
  3. def OAI.CurrentKS.Realization.updateVector line 17
  4. lemma OAI.CurrentKS.Realization.update_data line 28
  5. def OAI.CurrentKS.Realization.endpointEntry line 39
  6. def OAI.CurrentKS.Realization.endpointData line 45
  7. def OAI.CurrentKS.Realization.endpointCandidates line 47
  8. lemma OAI.CurrentKS.Realization.endpoint_data line 50
  9. def OAI.CurrentKS.Realization.freezeScalarData line 58
  10. lemma OAI.CurrentKS.Realization.nearestEndpoint_idem line 60
  11. lemma OAI.CurrentKS.Realization.freezeScalar_idem line 63
  12. def OAI.CurrentKS.Realization.freezeScalar line 67
  13. def OAI.CurrentKS.Realization.freezeVector line 74
  14. lemma OAI.CurrentKS.Realization.freezeOne_at line 75
  15. lemma OAI.CurrentKS.Realization.freezeList_at line 83
  16. lemma OAI.CurrentKS.Realization.freezeVector_data line 93