OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/TransformedGaussList.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The same certified node program is applied to the whole finite list of Gauss labels. It preserves the nucleus count and, at the proved precision, pairwise distinctness.

  1. abbrev OAI.ContinuumCoulomb.TransformedGauss.Environment line 17
  2. abbrev OAI.ContinuumCoulomb.TransformedGauss.Label line 18
  3. def OAI.ContinuumCoulomb.TransformedGauss.labelCode line 19
  4. def OAI.ContinuumCoulomb.TransformedGauss.environmentCode line 20
  5. def OAI.ContinuumCoulomb.TransformedGauss.listInputCode line 23
  6. def OAI.ContinuumCoulomb.TransformedGauss.nodes line 26
  7. opaque OAI.ContinuumCoulomb.TransformedGauss.nodeEnvironmentProgram line 29
  8. opaque OAI.ContinuumCoulomb.TransformedGauss.nodeLabelProgram line 32
  9. opaque OAI.ContinuumCoulomb.TransformedGauss.nodeParametersProgram line 34
  10. opaque OAI.ContinuumCoulomb.TransformedGauss.nodeFieldProgram line 37
  11. opaque OAI.ContinuumCoulomb.TransformedGauss.nodeArgumentProgram line 41
  12. opaque OAI.ContinuumCoulomb.TransformedGauss.listProgram line 48
  13. def OAI.ContinuumCoulomb.TransformedGauss.listCertificate line 55
  14. theorem OAI.ContinuumCoulomb.TransformedGauss.nodes_length line 59
  15. theorem OAI.ContinuumCoulomb.TransformedGauss.nodes_nodup line 62