OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCoefficientPrograms.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Literal unary programs for the actual routing coefficient envelopes. Their output lengths give polynomial bounds without choosing giant exponents.

  1. abbrev OAI.ContinuumCoulomb.QuantumCoefficientPrograms.Input line 14
  2. def OAI.ContinuumCoulomb.QuantumCoefficientPrograms.inputCode line 15
  3. def OAI.ContinuumCoulomb.QuantumCoefficientPrograms.pathBudget line 17
  4. def OAI.ContinuumCoulomb.QuantumCoefficientPrograms.pathRadius line 18
  5. def OAI.ContinuumCoulomb.QuantumCoefficientPrograms.pathCoefficient line 19
  6. def OAI.ContinuumCoulomb.QuantumCoefficientPrograms.iterated line 21
  7. theorem OAI.ContinuumCoulomb.QuantumCoefficientPrograms.pathBudget_cast line 25
  8. theorem OAI.ContinuumCoulomb.QuantumCoefficientPrograms.pathRadius_cast line 27
  9. theorem OAI.ContinuumCoulomb.QuantumCoefficientPrograms.pathCoefficient_cast line 29
  10. theorem OAI.ContinuumCoulomb.QuantumCoefficientPrograms.iterated_cast line 32
  11. def OAI.ContinuumCoulomb.QuantumCoefficientPrograms.add line 38
  12. def OAI.ContinuumCoulomb.QuantumCoefficientPrograms.mul line 41
  13. def OAI.ContinuumCoulomb.QuantumCoefficientPrograms.constant line 44
  14. def OAI.ContinuumCoulomb.QuantumCoefficientPrograms.square line 46
  15. def OAI.ContinuumCoulomb.QuantumCoefficientPrograms.cube line 49
  16. opaque OAI.ContinuumCoulomb.QuantumCoefficientPrograms.pathBudgetProgram line 53
  17. opaque OAI.ContinuumCoulomb.QuantumCoefficientPrograms.pathRadiusProgram line 61
  18. opaque OAI.ContinuumCoulomb.QuantumCoefficientPrograms.pathCoefficientProgram line 70
  19. opaque OAI.ContinuumCoulomb.QuantumCoefficientPrograms.mProgram line 78
  20. opaque OAI.ContinuumCoulomb.QuantumCoefficientPrograms.lProgram line 79
  21. opaque OAI.ContinuumCoulomb.QuantumCoefficientPrograms.tProgram line 81
  22. def OAI.ContinuumCoulomb.QuantumCoefficientPrograms.iteratedProgram line 84
  23. theorem OAI.ContinuumCoulomb.QuantumCoefficientPrograms.iterated_power line 91
  24. def OAI.ContinuumCoulomb.QuantumCoefficientPrograms.crossingBudget line 95
  25. def OAI.ContinuumCoulomb.QuantumCoefficientPrograms.crossingRadius line 96
  26. def OAI.ContinuumCoulomb.QuantumCoefficientPrograms.crossingCoefficient line 97
  27. theorem OAI.ContinuumCoulomb.QuantumCoefficientPrograms.crossingBudget_cast line 99
  28. theorem OAI.ContinuumCoulomb.QuantumCoefficientPrograms.crossingRadius_cast line 101
  29. theorem OAI.ContinuumCoulomb.QuantumCoefficientPrograms.crossingCoefficient_cast line 103
  30. opaque OAI.ContinuumCoulomb.QuantumCoefficientPrograms.crossingBudgetProgram line 107
  31. opaque OAI.ContinuumCoulomb.QuantumCoefficientPrograms.crossingRadiusProgram line 115
  32. opaque OAI.ContinuumCoulomb.QuantumCoefficientPrograms.crossingCoefficientProgram line 124