OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumFourCross.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact second-order columns for a Heisenberg edge between two encoded blocks.

  1. def OAI.ContinuumCoulomb.qmaFourDoubleEncoding line 12
  2. def OAI.ContinuumCoulomb.qmaFourDoublePenalty line 15
  3. def OAI.ContinuumCoulomb.qmaFourCross line 19
  4. theorem OAI.ContinuumCoulomb.qmaFourDoubleEncoding_gram line 22
  5. theorem OAI.ContinuumCoulomb.qmaFourCross_column line 27
  6. theorem OAI.ContinuumCoulomb.qmaFourCross_orthogonal line 32
  7. theorem OAI.ContinuumCoulomb.qmaFourCross_excitation line 38
  8. theorem OAI.ContinuumCoulomb.qmaFourCross_gram line 47