OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/ComputableResolvent.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The explicit rational machine approximates the actual planar resolvent to inverse-polynomial accuracy. No numerical oracle occurs in the statement or the program.

  1. theorem OAI.ContinuumCoulomb.ResolventSchedule.scheduled_error_bound line 12
  2. theorem OAI.ContinuumCoulomb.ResolventSchedule.approximation_error line 56