OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/HeisenbergOffsets.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Exact scalar offsets and positive homogeneity connecting the ordinary finite-spin Hamiltonian with the Hubbard superexchange source form.

  1. def OAI.ContinuumCoulomb.finiteHeisenbergMatrix line 16
  2. def OAI.ContinuumCoulomb.finiteHeisenbergBottom line 20
  3. theorem OAI.ContinuumCoulomb.sourceMatrixForm_smul line 23
  4. theorem OAI.ContinuumCoulomb.sourceMatrixBottom_smul line 33
  5. theorem OAI.ContinuumCoulomb.finiteHeisenbergBottom_smul line 45
  6. theorem OAI.ContinuumCoulomb.finiteHeisenbergBottom_bonds line 55
  7. theorem OAI.ContinuumCoulomb.HubbardGlobal.graphSourceAction_matrix line 61
  8. theorem OAI.ContinuumCoulomb.HubbardGlobal.graphSourceForm_matrix line 72
  9. theorem OAI.ContinuumCoulomb.HubbardGlobal.graphSourceBottom_offset line 92

    Source documentation

    Hubbard's Heisenberg - I convention contributes exactly one scalar minus the sum of all edge coefficients.

    theorem graphSourceBottom_offset (m : ℕ) (left right : Edge → Fin (m + 1)) (J : Edge → ℝ) :
    graphSourceBottom m left right J =
      finiteHeisenbergBottom (m + 1) left right J - ∑ e, J e := by
…

    Mentions: OAI.ContinuumCoulomb.HubbardGlobal.graphSourceBottom, OAI.ContinuumCoulomb.finiteHeisenbergBottom

  10. theorem OAI.ContinuumCoulomb.HubbardGlobal.graphSourceBottom_smul line 114
  11. theorem OAI.ContinuumCoulomb.HubbardGlobal.graphSourceBottom_bonds_smul line 121