OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumFourTensorGap.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The actual many-block four-spin penalty has a uniform full-complement gap.

  1. theorem OAI.ContinuumCoulomb.qmaFourProjection_star line 12
  2. theorem OAI.ContinuumCoulomb.qmaFourProjection_square line 15
  3. def OAI.ContinuumCoulomb.qmaFourTensorEncoding line 22
  4. def OAI.ContinuumCoulomb.qmaFourTensorProjection line 25
  5. def OAI.ContinuumCoulomb.qmaFourTensorPenalty line 28
  6. theorem OAI.ContinuumCoulomb.qmaFourTensorEncoding_gram line 31
  7. theorem OAI.ContinuumCoulomb.qmaFourTensorEncoding_projector line 35
  8. theorem OAI.ContinuumCoulomb.qmaFourTensorComplement_posSemidef line 40
  9. theorem OAI.ContinuumCoulomb.qmaFourTensorGap_posSemidef line 45
  10. theorem OAI.ContinuumCoulomb.qmaFourTensor_complement_gap line 83