OAI/MathematicalPhysics/ContinuumCoulomb/Programs/RationalExponentialProgram.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

A polynomial-time rational exponential evaluator. Magnitude and precision bounds are supplied in unary; the rational argument and result are encoded in binary. Every arithmetic operation is an actual stack program, including the shared-denominator Taylor recurrence.

  1. def OAI.ContinuumCoulomb.RationalExponentialProgram.stepProgram line 15
  2. def OAI.ContinuumCoulomb.RationalExponentialProgram.repeatProgram line 37
  3. def OAI.ContinuumCoulomb.RationalExponentialProgram.initialProgram line 41
  4. def OAI.ContinuumCoulomb.RationalExponentialProgram.resultProgram line 51
  5. def OAI.ContinuumCoulomb.RationalExponentialProgram.partialProgram line 61
  6. def OAI.ContinuumCoulomb.RationalExponentialProgram.orderProgram line 68
  7. abbrev OAI.ContinuumCoulomb.RationalExponentialProgram.Input line 83
  8. def OAI.ContinuumCoulomb.RationalExponentialProgram.inputCode line 85
  9. def OAI.ContinuumCoulomb.RationalExponentialProgram.approximate line 87
  10. def OAI.ContinuumCoulomb.RationalExponentialProgram.program line 89
  11. def OAI.ContinuumCoulomb.RationalExponentialProgram.certificate line 97
  12. theorem OAI.ContinuumCoulomb.RationalExponentialProgram.error line 100