OAI/Analysis/MatrixSigning/Realization/ScalarRealization.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CurrentKS.Realization.ratCode line 13
  2. def OAI.CurrentKS.Realization.boolCode line 14
  3. def OAI.CurrentKS.Realization.ratOp line 16
  4. def OAI.CurrentKS.Realization.ratLE line 21
  5. def OAI.CurrentKS.Realization.ratFloor line 25
  6. def OAI.CurrentKS.Realization.conditional line 31
  7. def OAI.CurrentKS.Realization.Realizes.ite line 42
  8. def OAI.CurrentKS.Realization.Realizes.add line 47
  9. def OAI.CurrentKS.Realization.Realizes.sub line 49
  10. def OAI.CurrentKS.Realization.Realizes.mul line 51
  11. def OAI.CurrentKS.Realization.Realizes.pow line 54
  12. def OAI.CurrentKS.Realization.Realizes.div line 60
  13. def OAI.CurrentKS.Realization.Realizes.le line 62
  14. def OAI.CurrentKS.Realization.Realizes.lt line 65
  15. def OAI.CurrentKS.Realization.Realizes.neg line 74
  16. def OAI.CurrentKS.Realization.Realizes.abs line 78
  17. def OAI.CurrentKS.Realization.roundScalar line 86
  18. lemma OAI.CurrentKS.Realization.fold_add_zero line 92
  19. def OAI.CurrentKS.Realization.sumRationals line 99
  20. def OAI.CurrentKS.Realization.l1Rationals line 103