OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumLocalTensor.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Tensor products with identity spectators are actual finite-support operators, with their small matrix given explicitly.

  1. theorem OAI.ContinuumCoulomb.qmaLocalLift_apply line 15
  2. theorem OAI.ContinuumCoulomb.qmaLocalOn_permutation line 22
  3. theorem OAI.ContinuumCoulomb.qmaLocalOn_sourceTensor line 48