OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumUnaryEnergy.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The local endpoint penalties dominate the finite history penalties.

  1. def OAI.ContinuumCoulomb.qmaInputMarker line 11
  2. def OAI.ContinuumCoulomb.qmaOutputMarker line 12
  3. def OAI.ContinuumCoulomb.qmaUnaryInputEnergy line 14
  4. def OAI.ContinuumCoulomb.qmaUnaryOutputEnergy line 18
  5. def OAI.ContinuumCoulomb.qmaUnaryEnergy line 23
  6. theorem OAI.ContinuumCoulomb.qmaInitialCountDiagonal_sum line 27
  7. theorem OAI.ContinuumCoulomb.qmaOutputPenalty_sum line 33
  8. theorem OAI.ContinuumCoulomb.qmaUnaryInputEnergy_valid_le line 45
  9. theorem OAI.ContinuumCoulomb.qmaUnaryOutputEnergy_valid_le line 60
  10. theorem OAI.ContinuumCoulomb.qmaUnaryEnergy_restriction line 80