OAI/MathematicalPhysics/AlternatingFlow/Compilers.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.AlternatingNS.Effective.space_norm_le_sum line 13
  2. lemma OAI.AlternatingNS.Effective.rationalVector_error line 22
  3. lemma OAI.AlternatingNS.Effective.mul_precision line 38
  4. abbrev OAI.AlternatingNS.Effective.EvalInput line 42
  5. abbrev OAI.AlternatingNS.Effective.ModInput line 43
  6. abbrev OAI.AlternatingNS.Effective.BoundInput line 44
  7. def OAI.AlternatingNS.Effective.sample line 46
  8. def OAI.AlternatingNS.Effective.values line 50
  9. lemma OAI.AlternatingNS.Effective.sample_computable line 54
  10. lemma OAI.AlternatingNS.Effective.values_computable line 64
  11. def OAI.AlternatingNS.Effective.modulus line 68
  12. lemma OAI.AlternatingNS.Effective.modulus_computable line 71
  13. def OAI.AlternatingNS.Effective.bound line 79
  14. lemma OAI.AlternatingNS.Effective.bound_computable line 82
  15. lemma OAI.AlternatingNS.Effective.Certified.programs line 89
  16. lemma OAI.AlternatingNS.ProgramFor.congr_half line 141