OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumLocalLift.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Exact tensor-local operators, with explicit finite supports.

  1. abbrev OAI.ContinuumCoulomb.QMASupportBasis line 15
  2. abbrev OAI.ContinuumCoulomb.QMASpectatorBasis line 16
  3. def OAI.ContinuumCoulomb.qmaSupportSplit line 18
  4. def OAI.ContinuumCoulomb.qmaLocalLift line 22
  5. def OAI.ContinuumCoulomb.QMALocalOn line 27
  6. theorem OAI.ContinuumCoulomb.qmaLocalLift_add line 30
  7. theorem OAI.ContinuumCoulomb.qmaLocalLift_smul line 34
  8. theorem OAI.ContinuumCoulomb.qmaLocalLift_mul line 39
  9. theorem OAI.ContinuumCoulomb.qmaLocalLift_adjoint line 44
  10. theorem OAI.ContinuumCoulomb.qmaLocalLift_one line 48
  11. theorem OAI.ContinuumCoulomb.QMALocalOn.add line 52
  12. theorem OAI.ContinuumCoulomb.QMALocalOn.mul line 58
  13. theorem OAI.ContinuumCoulomb.QMALocalOn.smul line 64
  14. theorem OAI.ContinuumCoulomb.QMALocalOn.adjoint line 69