OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkListBoundProgram.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Literal unary programs compute the coefficient envelopes. For each fixed number of rounds, the complete numerical envelope is polynomial in its inputs.

  1. def OAI.ContinuumCoulomb.QuantumForkList.budgetNat line 13
  2. def OAI.ContinuumCoulomb.QuantumForkList.radiusNat line 14
  3. def OAI.ContinuumCoulomb.QuantumForkList.coefficientNat line 15
  4. def OAI.ContinuumCoulomb.QuantumForkList.envelopeNat line 16
  5. theorem OAI.ContinuumCoulomb.QuantumForkList.budgetNat_cast line 20
  6. theorem OAI.ContinuumCoulomb.QuantumForkList.radiusNat_cast line 22
  7. theorem OAI.ContinuumCoulomb.QuantumForkList.coefficientNat_cast line 24
  8. theorem OAI.ContinuumCoulomb.QuantumForkList.envelopeNat_cast line 27
  9. def OAI.ContinuumCoulomb.QuantumForkList.add line 33
  10. def OAI.ContinuumCoulomb.QuantumForkList.mul line 36
  11. def OAI.ContinuumCoulomb.QuantumForkList.konst line 39
  12. def OAI.ContinuumCoulomb.QuantumForkList.sq line 41
  13. def OAI.ContinuumCoulomb.QuantumForkList.cube line 44
  14. def OAI.ContinuumCoulomb.QuantumForkList.budgetNatProgram line 48
  15. def OAI.ContinuumCoulomb.QuantumForkList.radiusNatProgram line 57
  16. def OAI.ContinuumCoulomb.QuantumForkList.coefficientNatProgram line 66
  17. def OAI.ContinuumCoulomb.QuantumForkList.envelopeNatProgram line 74
  18. theorem OAI.ContinuumCoulomb.QuantumForkList.envelopeNat_power line 82
  19. def OAI.ContinuumCoulomb.QuantumForkList.outputCoefficientNat line 87
  20. theorem OAI.ContinuumCoulomb.QuantumForkList.outputCoefficientNat_cast line 91
  21. def OAI.ContinuumCoulomb.QuantumForkList.outputCoefficientNatProgram line 95
  22. theorem OAI.ContinuumCoulomb.QuantumForkList.outputCoefficientNat_power line 103