OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumLatticeEnvelope.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

A literal polynomial program computes the final coefficient envelope; the exponent in the source promise is uniform over all inputs.

  1. def OAI.ContinuumCoulomb.QuantumCoefficientPrograms.addP line 12
  2. def OAI.ContinuumCoulomb.QuantumCoefficientPrograms.mulP line 15
  3. def OAI.ContinuumCoulomb.QuantumCoefficientPrograms.iteratedOfProgram line 19
  4. abbrev OAI.ContinuumCoulomb.QuantumCoefficientPrograms.LatticeInput line 28
  5. def OAI.ContinuumCoulomb.QuantumCoefficientPrograms.latticeInputCode line 29
  6. opaque OAI.ContinuumCoulomb.QuantumCoefficientPrograms.latticeM line 32
  7. opaque OAI.ContinuumCoulomb.QuantumCoefficientPrograms.latticeTail line 33
  8. opaque OAI.ContinuumCoulomb.QuantumCoefficientPrograms.latticeR line 35
  9. opaque OAI.ContinuumCoulomb.QuantumCoefficientPrograms.latticeLT line 37
  10. opaque OAI.ContinuumCoulomb.QuantumCoefficientPrograms.latticeL line 39
  11. opaque OAI.ContinuumCoulomb.QuantumCoefficientPrograms.latticeT line 41
  12. opaque OAI.ContinuumCoulomb.QuantumCoefficientPrograms.latticeBoundProgram line 44
  13. theorem OAI.ContinuumCoulomb.QuantumCoefficientPrograms.latticeBound_power line 55