OAI/MathematicalPhysics/RapidForcing/FormulaPrograms.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RapidForcing.EffectiveArithmetic.computable_rat_min line 12
  2. lemma OAI.RapidForcing.EffectiveArithmetic.computable_fin_app line 15
  3. lemma OAI.RapidForcing.EffectiveArithmetic.computable_fin_lambda line 18
  4. lemma OAI.RapidForcing.EffectiveArithmetic.computable_fin_sum line 23
  5. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_bound line 38
  6. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_diff line 47
  7. abbrev OAI.RapidForcing.EffectiveProfile.Formula.EvalArgs line 56
  8. def OAI.RapidForcing.EffectiveProfile.Formula.evalConst line 58
  9. def OAI.RapidForcing.EffectiveProfile.Formula.evalVar line 59
  10. def OAI.RapidForcing.EffectiveProfile.Formula.evalAdd line 60
  11. def OAI.RapidForcing.EffectiveProfile.Formula.evalMul line 64
  12. def OAI.RapidForcing.EffectiveProfile.Formula.evalProfile line 71
  13. lemma OAI.RapidForcing.EffectiveProfile.Formula.partrec_evalConst line 76
  14. lemma OAI.RapidForcing.EffectiveProfile.Formula.partrec_evalVar line 78
  15. lemma OAI.RapidForcing.EffectiveProfile.Formula.partrec_evalAdd line 81
  16. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_operandBox line 91
  17. def OAI.RapidForcing.EffectiveProfile.Formula.mulTolerance line 97
  18. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_mulTolerance line 98
  19. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_evalMul_args line 101
  20. lemma OAI.RapidForcing.EffectiveProfile.Formula.partrec_evalMul line 115
  21. lemma OAI.RapidForcing.EffectiveProfile.Formula.partrec_evalProfile line 124
  22. def OAI.RapidForcing.EffectiveProfile.Formula.constProgram line 136
  23. def OAI.RapidForcing.EffectiveProfile.Formula.varProgram line 137
  24. def OAI.RapidForcing.EffectiveProfile.Formula.addProgram line 138
  25. def OAI.RapidForcing.EffectiveProfile.Formula.mulProgram line 139
  26. def OAI.RapidForcing.EffectiveProfile.Formula.profileProgram line 140
  27. def OAI.RapidForcing.EffectiveProfile.Formula.evaluator line 142
  28. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_evaluator line 149
  29. lemma OAI.RapidForcing.EffectiveProfile.Formula.runTyped_evaluator line 158
  30. lemma OAI.RapidForcing.EffectiveProfile.Formula.partrec_evalAt line 172