OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumFourTensorInverse.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The bounded inverse acts exactly on the physical two-block excitations.

  1. theorem OAI.ContinuumCoulomb.qmaFourTensor_padded_star line 13
  2. theorem OAI.ContinuumCoulomb.qmaFourTensorPadded_symmetric line 19
  3. theorem OAI.ContinuumCoulomb.qmaFourTensorPadded_encoding line 26
  4. theorem OAI.ContinuumCoulomb.qmaFourTensorPadded_restrict line 32
  5. theorem OAI.ContinuumCoulomb.qmaFourTensorInverse_high line 50
  6. theorem OAI.ContinuumCoulomb.qmaFourTensorPadded_column line 59
  7. theorem OAI.ContinuumCoulomb.qmaFourTensorInverse_column line 67