OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCrossingScaleProgram.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Exact rational scale for a simultaneous crossing layer, computed from its retained coefficients and the two crossing coefficients at each cell.

  1. abbrev OAI.ContinuumCoulomb.QuantumCrossingScaleProgram.Pair line 14
  2. def OAI.ContinuumCoulomb.QuantumCrossingScaleProgram.pairCode line 15
  3. abbrev OAI.ContinuumCoulomb.QuantumCrossingScaleProgram.Input line 16
  4. def OAI.ContinuumCoulomb.QuantumCrossingScaleProgram.inputCode line 17
  5. def OAI.ContinuumCoulomb.QuantumCrossingScaleProgram.linearCost line 19
  6. def OAI.ContinuumCoulomb.QuantumCrossingScaleProgram.squareCost line 20
  7. def OAI.ContinuumCoulomb.QuantumCrossingScaleProgram.base line 21
  8. def OAI.ContinuumCoulomb.QuantumCrossingScaleProgram.active line 22
  9. def OAI.ContinuumCoulomb.QuantumCrossingScaleProgram.correction line 23
  10. def OAI.ContinuumCoulomb.QuantumCrossingScaleProgram.value line 24
  11. opaque OAI.ContinuumCoulomb.QuantumCrossingScaleProgram.linearProgram line 27
  12. opaque OAI.ContinuumCoulomb.QuantumCrossingScaleProgram.squareProgram line 32
  13. def OAI.ContinuumCoulomb.QuantumCrossingScaleProgram.sumMapProgram line 34
  14. opaque OAI.ContinuumCoulomb.QuantumCrossingScaleProgram.program line 37
  15. def OAI.ContinuumCoulomb.QuantumCrossingScaleProgram.actualInput line 55
  16. theorem OAI.ContinuumCoulomb.QuantumCrossingScaleProgram.value_actual line 60