OAI/MathematicalPhysics/ContinuumCoulomb/Programs/SourceNormalizationProgram.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Actual polynomial-time normalization of a literal source-bond list. The input coefficient bound and inverse precision are unary metadata; the rounding denominator uses the actual list length, and zero bonds are deleted.

  1. opaque OAI.ContinuumCoulomb.SourceNormalizationProgram.add line 12
  2. opaque OAI.ContinuumCoulomb.SourceNormalizationProgram.mul line 14
  3. opaque OAI.ContinuumCoulomb.SourceNormalizationProgram.xsProgram line 17
  4. opaque OAI.ContinuumCoulomb.SourceNormalizationProgram.environment line 19
  5. opaque OAI.ContinuumCoulomb.SourceNormalizationProgram.lengthProgram line 20
  6. opaque OAI.ContinuumCoulomb.SourceNormalizationProgram.wProgram line 22
  7. opaque OAI.ContinuumCoulomb.SourceNormalizationProgram.gProgram line 24
  8. opaque OAI.ContinuumCoulomb.SourceNormalizationProgram.nProgram line 27
  9. opaque OAI.ContinuumCoulomb.SourceNormalizationProgram.denominatorProgram line 31
  10. def OAI.ContinuumCoulomb.SourceNormalizationProgram.rounded line 39
  11. def OAI.ContinuumCoulomb.SourceNormalizationProgram.retained line 43
  12. opaque OAI.ContinuumCoulomb.SourceNormalizationProgram.roundList line 45
  13. opaque OAI.ContinuumCoulomb.SourceNormalizationProgram.roundedProgram line 49
  14. opaque OAI.ContinuumCoulomb.SourceNormalizationProgram.retainedProgram line 54
  15. opaque OAI.ContinuumCoulomb.SourceNormalizationProgram.retainedLength line 56
  16. opaque OAI.ContinuumCoulomb.SourceNormalizationProgram.boundProgram line 59
  17. def OAI.ContinuumCoulomb.SourceNormalizationProgram.normalized line 63
  18. opaque OAI.ContinuumCoulomb.SourceNormalizationProgram.normalizedEnv line 68
  19. opaque OAI.ContinuumCoulomb.SourceNormalizationProgram.normalizedProgram line 70
  20. def OAI.ContinuumCoulomb.SourceNormalizationProgram.certificate line 72