OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/SourceGraphIndex.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The actual contact-site enumeration and the finite Hubbard graph use one common electron index. Relabeling changes no bond or coordinate order.

  1. theorem OAI.ContinuumCoulomb.SourcePositiveProgram.rawSiteCount line 13
  2. def OAI.ContinuumCoulomb.SourcePositiveProgram.siteEquiv line 21
  3. def OAI.ContinuumCoulomb.SourcePositiveProgram.indexedGraph line 25
  4. def OAI.ContinuumCoulomb.SourcePositiveProgram.indexedSites line 29
  5. theorem OAI.ContinuumCoulomb.SourcePositiveProgram.graph_left line 33
  6. theorem OAI.ContinuumCoulomb.SourcePositiveProgram.graph_right line 41
  7. theorem OAI.ContinuumCoulomb.SourcePositiveProgram.indexedGraph_left line 49
  8. theorem OAI.ContinuumCoulomb.SourcePositiveProgram.indexedGraph_right line 57
  9. theorem OAI.ContinuumCoulomb.SourcePositiveProgram.indexedGraph_toList line 65
  10. theorem OAI.ContinuumCoulomb.SourcePositiveProgram.indexedGraph_weight line 70
  11. theorem OAI.ContinuumCoulomb.SourcePositiveProgram.indexedGraph_noLoops line 75
  12. theorem OAI.ContinuumCoulomb.SourcePositiveProgram.indexedGraph_simple line 80
  13. theorem OAI.ContinuumCoulomb.SourcePositiveProgram.ofFn_finCongr line 85
  14. theorem OAI.ContinuumCoulomb.SourcePositiveProgram.indexedSites_ofFn line 90