OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/HubbardReduction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Second-order estimate with the global charge penalty

The occupation configurations determine the penalty, its inverse, its positivity and its spectral gap. The resulting bottom-energy comparison retains every electron and spin configuration.

  1. abbrev OAI.ContinuumCoulomb.HubbardLowSpace line 18
  2. def OAI.ContinuumCoulomb.hubbardLowUnit line 20
  3. theorem OAI.ContinuumCoulomb.hubbardLowUnit_norm line 23
  4. theorem OAI.ContinuumCoulomb.hubbard_charge_second_order line 29

    Source documentation

    The zero first-order block Hubbard estimate, with its concrete global charge penalty and explicit cubic error. All electron and spin configurations are represented by the low space and the supplied high occupations.

    theorem hubbard_charge_second_order {m : ℕ} {Basis : Type*} [Fintype Basis]
    (U R : ℝ) (V : Fin m → Fin m → ℝ) (occupation : Basis → Fin m → Fin 3)
    (hsymm : ∀ i j, V i j = V j i) (hrow : ∀ i, ∑ j, |V i j| ≤ R)
    (hUR : R < U) (hfill : ∀ s, ∑ i, (occupation s i : ℕ) = m)
    (B : HubbardLowSpace m →L[ℝ] EuclideanSpace ℂ (ChargeHighBasis occupation))
    (D : EuclideanSpace ℂ (ChargeHighBasis occupation) →L[ℝ]
      EuclideanSpace ℂ (ChargeHighBasis occupation))
    {epsilon : ℝ} (hepsilon : 0 ≤ epsilon) (hsmall : epsilon < 1 / 2)
    (hB : ‖B‖ ≤ epsilon * (U - R)) (hD : ‖D‖ ≤ epsilon * (U - R)) :
    let weight : ChargeHighBasis occupation → ℝ :=
…

    Mentions: OAI.ContinuumCoulomb.HubbardLowSpace, OAI.ContinuumCoulomb.ChargeHighBasis