OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumBlockExchange.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Both internal and cross-block couplings are ordinary source Heisenberg exchanges.

  1. theorem OAI.ContinuumCoulomb.qmaBlockExchange_source line 13
  2. theorem OAI.ContinuumCoulomb.qmaBlockCross_source line 26