OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/SuperexchangeSpectrum.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Exact spectral identification of the global Hubbard inverse term.

  1. def OAI.ContinuumCoulomb.HubbardGlobal.graphHeisenbergFock line 13
  2. def OAI.ContinuumCoulomb.HubbardGlobal.graphSourceAction line 18
  3. def OAI.ContinuumCoulomb.HubbardGlobal.graphSourceForm line 22
  4. theorem OAI.ContinuumCoulomb.HubbardGlobal.graphHeisenbergFock_spinEmbedding line 26
  5. theorem OAI.ContinuumCoulomb.HubbardGlobal.graphSuperexchange_spinEmbedding line 39

    Source documentation

    The checked basis compression extends to every entangled spin state.

    theorem graphSuperexchange_spinEmbedding (m : ℕ) (U : ℝ)
    (V : Fin (m + 1) → Fin (m + 1) → ℝ)
    (hsymm : ∀ i j, V i j = V j i) (hdiag : ∀ i, V i i = 0)
    (left right : Edge → Fin (m + 1)) (t J : Edge → ℂ)
    (hloop : ∀ e, left e ≠ right e)
    (hsimple : ∀ e f, e ≠ f →
      ¬(left e = left f ∧ right e = right f) ∧ ¬(left e = right f ∧ right e = left f))
    (hgap : ∀ e, U - V (left e) (right e) ≠ 0)
    (hcal : ∀ e, t e ^ 2 = J e * ((U - V (left e) (right e) : ℝ) : ℂ))
    (u : SourceSpinVector (m + 1)) :
    -(lowProjection m (graphHopping m left right t
      (chargeInverse m U V (graphHopping m left right t (spinEmbedding m u))))) =
…

    Mentions: OAI.ContinuumCoulomb.SourceSpinVector, OAI.ContinuumCoulomb.HubbardGlobal.lowProjection, OAI.ContinuumCoulomb.HubbardGlobal.graphHopping, OAI.ContinuumCoulomb.HubbardGlobal.chargeInverse, OAI.ContinuumCoulomb.HubbardGlobal.spinEmbedding

  6. theorem OAI.ContinuumCoulomb.HubbardGlobal.lowFockInclusion_spinEmbedding line 68
  7. theorem OAI.ContinuumCoulomb.HubbardGlobal.lowFockRestriction_inclusion line 79
  8. theorem OAI.ContinuumCoulomb.HubbardGlobal.lowFockInclusion_injective line 86
  9. theorem OAI.ContinuumCoulomb.HubbardGlobal.fockOperator_diagonal_apply line 90
  10. def OAI.ContinuumCoulomb.HubbardGlobal.actualChargeInverse line 97
  11. theorem OAI.ContinuumCoulomb.HubbardGlobal.highFockInclusion_chargeInverse line 101
  12. theorem OAI.ContinuumCoulomb.HubbardGlobal.actualChargeInverse_coupling_inclusion line 119

    Source documentation

    The inverse on the concrete high block is the same actual occupation-diagonal inverse used in the global CAR compression.

    theorem actualChargeInverse_coupling_inclusion (m : ℕ) (U : ℝ)
    (V : Fin (m + 1) → Fin (m + 1) → ℝ)
    (left right : Edge → Fin (m + 1)) (t : Edge → ℝ)
    (hloop : ∀ e, left e ≠ right e) (p : ActualHubbardLowSpace m) :
    highFockInclusion m (actualChargeInverse m U V (actualHubbardCoupling m left right t p)) =
      fockCoordinates (2 * m + 1)
        (chargeInverse m U V (graphHopping m left right (fun e => (t e : ℂ))
          (spinEmbedding m (fun s => p s)))) := by
…

    Mentions: OAI.ContinuumCoulomb.HubbardGlobal.ActualHubbardLowSpace, OAI.ContinuumCoulomb.HubbardGlobal.highFockInclusion, OAI.ContinuumCoulomb.HubbardGlobal.actualChargeInverse, OAI.ContinuumCoulomb.HubbardGlobal.actualHubbardCoupling, OAI.ContinuumCoulomb.HubbardGlobal.fockCoordinates, OAI.ContinuumCoulomb.HubbardGlobal.chargeInverse, OAI.ContinuumCoulomb.HubbardGlobal.graphHopping, OAI.ContinuumCoulomb.HubbardGlobal.spinEmbedding

  13. theorem OAI.ContinuumCoulomb.HubbardGlobal.graphSourceForm_expectation line 134
  14. theorem OAI.ContinuumCoulomb.HubbardGlobal.lowFockRestriction_superexchange line 154
  15. theorem OAI.ContinuumCoulomb.HubbardGlobal.actualHubbard_effectiveForm line 175

    Source documentation

    The effective quadratic form of the actual Hubbard blocks is the entire graph Heisenberg form, with the exact scalar offset.

    theorem actualHubbard_effectiveForm (m : ℕ) (U : ℝ)
    (V : Fin (m + 1) → Fin (m + 1) → ℝ)
    (hsymm : ∀ i j, V i j = V j i) (hdiag : ∀ i, V i i = 0)
    (left right : Edge → Fin (m + 1)) (t J : Edge → ℝ)
    (hloop : ∀ e, left e ≠ right e)
    (hsimple : ∀ e f, e ≠ f →
      ¬(left e = left f ∧ right e = right f) ∧ ¬(left e = right f ∧ right e = left f))
    (hgap : ∀ e, U - V (left e) (right e) ≠ 0)
    (hcal : ∀ e, t e ^ 2 = J e * (U - V (left e) (right e)))
    (p : ActualHubbardLowSpace m) :
    Perturbation.effectiveForm
        (0 : ActualHubbardLowSpace m →L[ℝ] ActualHubbardLowSpace m)
…

    Mentions: OAI.ContinuumCoulomb.HubbardGlobal.ActualHubbardLowSpace, OAI.ContinuumCoulomb.Perturbation.effectiveForm

  16. def OAI.ContinuumCoulomb.HubbardGlobal.graphSourceBottom line 246
  17. theorem OAI.ContinuumCoulomb.HubbardGlobal.sourceSpinMass_euclidean line 250
  18. theorem OAI.ContinuumCoulomb.HubbardGlobal.actualHubbard_effectiveBottom line 256

    Source documentation

    Equality of the two actual variational bottoms; no minimizer or assertion about the desired source energy is supplied as an assumption.

    theorem actualHubbard_effectiveBottom (m : ℕ) (U : ℝ)
    (V : Fin (m + 1) → Fin (m + 1) → ℝ)
    (hsymm : ∀ i j, V i j = V j i) (hdiag : ∀ i, V i i = 0)
    (left right : Edge → Fin (m + 1)) (t J : Edge → ℝ)
    (hloop : ∀ e, left e ≠ right e)
    (hsimple : ∀ e f, e ≠ f →
      ¬(left e = left f ∧ right e = right f) ∧ ¬(left e = right f ∧ right e = left f))
    (hgap : ∀ e, U - V (left e) (right e) ≠ 0)
    (hcal : ∀ e, t e ^ 2 = J e * (U - V (left e) (right e))) :
    Perturbation.effectiveBottom
        (0 : ActualHubbardLowSpace m →L[ℝ] ActualHubbardLowSpace m)
        (actualChargeInverse m U V) (actualHubbardCoupling m left right t) =
…

    Mentions: OAI.ContinuumCoulomb.Perturbation.effectiveBottom, OAI.ContinuumCoulomb.HubbardGlobal.ActualHubbardLowSpace, OAI.ContinuumCoulomb.HubbardGlobal.actualChargeInverse, OAI.ContinuumCoulomb.HubbardGlobal.actualHubbardCoupling

  19. theorem OAI.ContinuumCoulomb.HubbardGlobal.actual_hubbard_Heisenberg_bottom line 290

    Source documentation

    Global second-order energy comparison with concrete Fock blocks and the actual normalized graph-spin spectral bottom.

    theorem actual_hubbard_Heisenberg_bottom (m : ℕ) (U R : ℝ)
    (V : Fin (m + 1) → Fin (m + 1) → ℝ)
    (hsymm : ∀ i j, V i j = V j i) (hdiag : ∀ i, V i i = 0)
    (hrow : ∀ i, ∑ j, |V i j| ≤ R) (hUR : R < U)
    (left right : Edge → Fin (m + 1)) (t J : Edge → ℝ)
    (hloop : ∀ e, left e ≠ right e)
    (hsimple : ∀ e f, e ≠ f →
      ¬(left e = left f ∧ right e = right f) ∧ ¬(left e = right f ∧ right e = left f))
    (hgap : ∀ e, U - V (left e) (right e) ≠ 0)
    (hcal : ∀ e, t e ^ 2 = J e * (U - V (left e) (right e)))
    {epsilon : ℝ} (hepsilon : 0 ≤ epsilon) (hsmall : epsilon < 1 / 2)
    (ht : 4 * ∑ e, |t e| ≤ epsilon * (U - R)) :
…