OAI/MathematicalPhysics/ContinuumCoulomb/Programs/PiProgram.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

A rational polynomial-time approximation to π from the integral of 4 / (1+x²) on [0,1]. The unary sample count gives absolute error 8/N. This supplies the normalizing constant in the heat-kernel evaluator.

  1. def OAI.ContinuumCoulomb.PiProgram.evaluate line 15
  2. def OAI.ContinuumCoulomb.PiProgram.input line 17
  3. def OAI.ContinuumCoulomb.PiProgram.approximate line 19
  4. def OAI.ContinuumCoulomb.PiProgram.evaluateProgram line 21
  5. def OAI.ContinuumCoulomb.PiProgram.inputProgram line 29
  6. def OAI.ContinuumCoulomb.PiProgram.program line 35
  7. def OAI.ContinuumCoulomb.PiProgram.certificate line 40
  8. theorem OAI.ContinuumCoulomb.PiProgram.reciprocal_continuous line 43
  9. theorem OAI.ContinuumCoulomb.PiProgram.reciprocal_lipschitz line 47
  10. theorem OAI.ContinuumCoulomb.PiProgram.endpoint line 66
  11. theorem OAI.ContinuumCoulomb.PiProgram.error line 70