OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumFourPositive.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The checked rational certificate is nonnegative on all complex states.

  1. def OAI.ContinuumCoulomb.qmaFourSymmetricColumn line 15
  2. theorem OAI.ContinuumCoulomb.qmaFourSymmetricRational_factor line 18
  3. theorem OAI.ContinuumCoulomb.qmaRatMatrix_adjoint line 33
  4. def OAI.ContinuumCoulomb.qmaFourSymmetricColumnComplex line 38
  5. def OAI.ContinuumCoulomb.qmaFourSymmetricDiagonal line 41
  6. theorem OAI.ContinuumCoulomb.qmaFourSymmetricDiagonal_cast line 44
  7. theorem OAI.ContinuumCoulomb.qmaFourSymmetricComplex_factor line 53
  8. theorem OAI.ContinuumCoulomb.qmaFourSymmetric_nonneg line 60
  9. def OAI.ContinuumCoulomb.qmaFourProjection line 73
  10. def OAI.ContinuumCoulomb.qmaFourPenalty line 74
  11. theorem OAI.ContinuumCoulomb.qmaFourGap_complex line 76
  12. theorem OAI.ContinuumCoulomb.qmaFourGap_form line 84