OAI/MathematicalPhysics/ContinuumCoulomb/Programs/NormalizationProgram.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Actual polynomial TM2 computation of the normalization integral at inverse-polynomial precision. Every mesh and sample parameter is built using the proved unary arithmetic procedures.

  1. opaque OAI.ContinuumCoulomb.NormalizationSchedule.radiusRationalProgram line 12
  2. opaque OAI.ContinuumCoulomb.NormalizationSchedule.meshRationalProgram line 15
  3. opaque OAI.ContinuumCoulomb.NormalizationSchedule.doubleRadiusRationalProgram line 18
  4. opaque OAI.ContinuumCoulomb.NormalizationSchedule.lowerProgram line 22
  5. opaque OAI.ContinuumCoulomb.NormalizationSchedule.stepProgram line 25
  6. opaque OAI.ContinuumCoulomb.NormalizationSchedule.inputProgram line 30
  7. opaque OAI.ContinuumCoulomb.NormalizationSchedule.program line 35
  8. def OAI.ContinuumCoulomb.NormalizationSchedule.certificate line 38