OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/GramPenalty.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ContinuumCoulomb.chargePenalty_Gram_gap line 15

   Source documentation

   Full quadratic coercivity gives a gap on every half-filled charge defect.

   theorem chargePenalty_Gram_gap {m : ℕ} (U c : ℝ) (V : Fin m → Fin m → ℝ)
       (hc : 0 ≤ c)
       (hGram : ∀ d : Fin m → ℝ,
         c * ∑ i, d i ^ 2 ≤ U * ∑ i, d i ^ 2 + ∑ i, ∑ j, V i j * d i * d j)
       (occupation : Fin m → Fin 3) (hfill : ∑ i, (occupation i : ℕ) = m)
       (hdefect : ¬∀ i, occupation i = 1) : c ≤ chargePenalty U V occupation := by
   …

   Mentions: OAI.ContinuumCoulomb.chargePenalty

2. theorem OAI.ContinuumCoulomb.chargeTransfer_Gram_denominator line 29

   Source documentation

   The same Gram condition controls the physical virtual excitation without replacing its exact denominator by the global coercivity constant.

   theorem chargeTransfer_Gram_denominator {m : ℕ} (U c : ℝ) (V : Fin m → Fin m → ℝ)
       (hGram : ∀ d : Fin m → ℝ,
         c * ∑ i, d i ^ 2 ≤ U * ∑ i, d i ^ 2 + ∑ i, ∑ j, V i j * d i * d j)
       (hole double : Fin m) (hne : hole ≠ double)
       (hsymm : ∀ i j, V i j = V j i) (hdiag : ∀ i, V i i = 0) :
       c ≤ U - V hole double := by
   …

3. theorem OAI.ContinuumCoulomb.chargePenalty_Gram_inverse_data line 41
4. theorem OAI.ContinuumCoulomb.HubbardGlobal.actual_hubbard_Gram_second_order line 63

   Source documentation

   Actual full Fock blocks, with smallness measured against the Gram gap.

   theorem actual_hubbard_Gram_second_order (m : ℕ) (U c : ℝ)
       (V : Fin (m + 1) → Fin (m + 1) → ℝ) (hc : 0 < c)
       (hGram : ∀ d : Fin (m + 1) → ℝ,
         c * ∑ i, d i ^ 2 ≤ U * ∑ i, d i ^ 2 + ∑ i, ∑ j, V i j * d i * d j)
       (left right : Edge → Fin (m + 1)) (t : Edge → ℝ)
       {epsilon : ℝ} (hepsilon : 0 ≤ epsilon) (hsmall : epsilon < 1 / 2)
       (ht : 4 * ∑ e, |t e| ≤ epsilon * c) :
       let weight : HalfFilledHighBasis m → ℝ :=
   …

   Mentions: OAI.ContinuumCoulomb.HubbardGlobal.HalfFilledHighBasis

5. theorem OAI.ContinuumCoulomb.HubbardGlobal.hubbardFermionBottom_Gram_Heisenberg line 92

   Source documentation

   Complete fixed-particle fermion-to-spin spectrum under full Gram coercivity. The exact denominators U−Vij follow from that same condition.

   theorem hubbardFermionBottom_Gram_Heisenberg (m : ℕ) (U c : ℝ)
       (V : Fin (m + 1) → Fin (m + 1) → ℝ)
       (hsymm : ∀ i j, V i j = V j i) (hdiag : ∀ i, V i i = 0) (hc : 0 < c)
       (hGram : ∀ d : Fin (m + 1) → ℝ,
         c * ∑ i, d i ^ 2 ≤ U * ∑ i, d i ^ 2 + ∑ i, ∑ j, V i j * d i * d j)
       (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))
       (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 * c) :
   …