OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPathScaleProgram.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Exact rational calibration from the retained and selected edge weights. The sums are computed by the proved polynomial rational-list accumulator.

  1. abbrev OAI.ContinuumCoulomb.QuantumPathScaleProgram.Input line 14
  2. def OAI.ContinuumCoulomb.QuantumPathScaleProgram.inputCode line 15
  3. def OAI.ContinuumCoulomb.QuantumPathScaleProgram.linearCost line 18
  4. def OAI.ContinuumCoulomb.QuantumPathScaleProgram.squareCost line 19
  5. def OAI.ContinuumCoulomb.QuantumPathScaleProgram.base line 20
  6. def OAI.ContinuumCoulomb.QuantumPathScaleProgram.active line 21
  7. def OAI.ContinuumCoulomb.QuantumPathScaleProgram.correction line 22
  8. def OAI.ContinuumCoulomb.QuantumPathScaleProgram.value line 23
  9. def OAI.ContinuumCoulomb.QuantumPathScaleProgram.linearProgram line 26
  10. def OAI.ContinuumCoulomb.QuantumPathScaleProgram.squareProgram line 31
  11. def OAI.ContinuumCoulomb.QuantumPathScaleProgram.sumMapProgram line 35
  12. def OAI.ContinuumCoulomb.QuantumPathScaleProgram.program line 39
  13. def OAI.ContinuumCoulomb.QuantumPathScaleProgram.actualInput line 59
  14. theorem OAI.ContinuumCoulomb.QuantumPathScaleProgram.value_actual line 64