OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/MediatorSimple.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Fresh mediator pairs give a simple unordered edge enumeration. This supplies the cross-edge cancellation hypothesis in the global Hubbard model.

  1. def OAI.ContinuumCoulomb.MediatorIteration.edgeMatches line 11
  2. theorem OAI.ContinuumCoulomb.MediatorIteration.edgeMatches_symm line 14
  3. def OAI.ContinuumCoulomb.MediatorIteration.Bonds.Simple line 20
  4. theorem OAI.ContinuumCoulomb.MediatorIteration.Bonds.Simple.hypothesis line 23
  5. theorem OAI.ContinuumCoulomb.MediatorIteration.lift_simple line 30
  6. theorem OAI.ContinuumCoulomb.MediatorIteration.central_simple line 38
  7. theorem OAI.ContinuumCoulomb.MediatorIteration.spokes_simple line 47
  8. theorem OAI.ContinuumCoulomb.MediatorIteration.join_simple line 67
  9. theorem OAI.ContinuumCoulomb.MediatorIteration.central_spokes_simple line 92
  10. theorem OAI.ContinuumCoulomb.MediatorIteration.lift_stage_simple line 101
  11. theorem OAI.ContinuumCoulomb.MediatorIteration.firstGraph_simple line 120
  12. theorem OAI.ContinuumCoulomb.MediatorIteration.secondPaths_simple line 124
  13. theorem OAI.ContinuumCoulomb.MediatorIteration.finalGraph_simple line 128