OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumFourTensorFamily.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact effective Hamiltonian of a family of distinct logical edges.

  1. theorem OAI.ContinuumCoulomb.qmaOrthogonalColumns_sum_gram line 15
  2. theorem OAI.ContinuumCoulomb.qmaFourTensorCoupling_distinct line 29
  3. def OAI.ContinuumCoulomb.qmaFourTensorFamilyCoupling line 36
  4. def OAI.ContinuumCoulomb.qmaFourTensorFamilyCounterterm line 40
  5. theorem OAI.ContinuumCoulomb.qmaFourTensorFamily_effective line 45