OAI/Probability/SATComputability/ArithmeticEnclosures.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FixedClauseThreshold.Computability.FiniteArithmetic.rat_max_computable line 13
  2. theorem OAI.FixedClauseThreshold.Computability.FiniteArithmetic.exp_effective line 17
  3. theorem OAI.FixedClauseThreshold.Computability.FiniteArithmetic.log_effective line 20
  4. def OAI.FixedClauseThreshold.Computability.FiniteArithmetic.expApprox line 26
  5. def OAI.FixedClauseThreshold.Computability.FiniteArithmetic.logApprox line 27
  6. theorem OAI.FixedClauseThreshold.Computability.FiniteArithmetic.expApprox_computable line 29
  7. theorem OAI.FixedClauseThreshold.Computability.FiniteArithmetic.logApprox_computable line 30
  8. theorem OAI.FixedClauseThreshold.Computability.FiniteArithmetic.expApprox_error line 32
  9. theorem OAI.FixedClauseThreshold.Computability.FiniteArithmetic.logApprox_error line 36
  10. def OAI.FixedClauseThreshold.Computability.FiniteArithmetic.interval line 40
  11. theorem OAI.FixedClauseThreshold.Computability.FiniteArithmetic.interval_computable line 42
  12. theorem OAI.FixedClauseThreshold.Computability.FiniteArithmetic.interval_covers line 46
  13. theorem OAI.FixedClauseThreshold.Computability.FiniteArithmetic.interval_encloses line 52
  14. theorem OAI.FixedClauseThreshold.Computability.FiniteArithmetic.approximate_tendsto line 61
  15. def OAI.FixedClauseThreshold.Computability.FiniteArithmetic.expBall line 70
  16. def OAI.FixedClauseThreshold.Computability.FiniteArithmetic.logBall line 74
  17. theorem OAI.FixedClauseThreshold.Computability.FiniteArithmetic.expBall_computable line 78
  18. theorem OAI.FixedClauseThreshold.Computability.FiniteArithmetic.logBall_computable line 81
  19. theorem OAI.FixedClauseThreshold.Computability.FiniteArithmetic.expBall_covers line 85
  20. theorem OAI.FixedClauseThreshold.Computability.FiniteArithmetic.logBall_covers line 100
  21. theorem OAI.FixedClauseThreshold.Computability.FiniteArithmetic.Encloses.exp line 118
  22. theorem OAI.FixedClauseThreshold.Computability.FiniteArithmetic.Encloses.log line 133