OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumUnaryForm.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The full unary-clock form retains every clock configuration.

  1. abbrev OAI.ContinuumCoulomb.QMAUnaryBasis line 13
  2. def OAI.ContinuumCoulomb.qmaUnaryRestrict line 16
  3. def OAI.ContinuumCoulomb.qmaUnaryMass line 19
  4. def OAI.ContinuumCoulomb.qmaUnaryInvalidMass line 22
  5. def OAI.ContinuumCoulomb.qmaUnaryClockEnergy line 26
  6. theorem OAI.ContinuumCoulomb.qmaUnaryMass_split line 30
  7. theorem OAI.ContinuumCoulomb.qmaUnaryInvalidMass_le line 38
  8. def OAI.ContinuumCoulomb.qmaUnaryResidual line 44
  9. def OAI.ContinuumCoulomb.qmaUnaryPropagationEnergy line 50
  10. theorem OAI.ContinuumCoulomb.qmaUnaryResidual_valid line 55
  11. theorem OAI.ContinuumCoulomb.qmaUnaryPropagationEnergy_valid_le line 64