ChargePenalty.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Charge-transfer penalty at half filling

The diagonal part of the finite fermion model keeps long-range direct Coulomb interactions. A symmetric interaction matrix with bounded absolute row sums gives a gap against every nonsingly occupied configuration.

theorem OAI.ContinuumCoulomb.symmetric_interaction_form_bound line 20

Source documentation

Symmetric row-sum control bounds the entire quadratic interaction form.

theorem symmetric_interaction_form_bound {m : ℕ} (V : Fin m → Fin m → ℝ)
    (d : Fin m → ℝ) (R : ℝ) (hsymm : ∀ i j, V i j = V j i)
    (hrow : ∀ i, ∑ j, |V i j| ≤ R) :
    |∑ i, ∑ j, V i j * d i * d j| ≤ R * ∑ i, d i ^ 2 := by
…

def OAI.ContinuumCoulomb.occupationDeviation line 64
theorem OAI.ContinuumCoulomb.occupation_defect_size line 69
Source documentation
Number conservation forces a charge defect to contain at least one empty and one doubly occupied site, so its squared charge is at least two.
```
theorem occupation_defect_size {m : ℕ} (occupation : Fin m → Fin 3)
    (hfill : ∑ i, (occupation i : ℕ) = m)
    (hdefect : ¬ ∀ i, occupation i = 1) :
    2 ≤ ∑ i, occupationDeviation occupation i ^ 2 := by
…
```
Mentions: OAI.ContinuumCoulomb.occupationDeviation
def OAI.ContinuumCoulomb.chargePenalty line 109

theorem OAI.ContinuumCoulomb.chargePenalty_offset_identity line 119

Source documentation

The direct Coulomb term and the compensating diagonal one-body term are exactly the charge penalty minus its fixed scalar shift. Here V i i=0 is the physical off-site convention; the algebraic identity needs only symmetry and conservation of total particle number.

theorem chargePenalty_offset_identity {m : ℕ} (U : ℝ) (V : Fin m → Fin m → ℝ)
    (occupation : Fin m → Fin 3) (hsymm : ∀ i j, V i j = V j i)
    (hfill : ∑ i, (occupation i : ℕ) = m) :
    U / 2 * (∑ i, ((occupation i : ℕ) : ℝ) * (((occupation i : ℕ) : ℝ) - 1)) +
        (1 / 2 : ℝ) * (∑ i, ∑ j,
          V i j * ((occupation i : ℕ) : ℝ) * ((occupation j : ℕ) : ℝ)) -
        (∑ i, (∑ j, V i j) * ((occupation i : ℕ) : ℝ)) =
      chargePenalty U V occupation - (1 / 2 : ℝ) * ∑ i, ∑ j, V i j := by
…

Mentions: OAI.ContinuumCoulomb.chargePenalty

theorem OAI.ContinuumCoulomb.chargePenalty_gap line 175

Source documentation

All number-conserving charge-transfer configurations cost at least U-R, including every long-range interaction in the row-sum budget.

theorem chargePenalty_gap {m : ℕ} (U R : ℝ) (V : Fin m → Fin m → ℝ)
    (occupation : Fin m → Fin 3) (hsymm : ∀ i j, V i j = V j i)
    (hrow : ∀ i, ∑ j, |V i j| ≤ R) (hUR : R ≤ U)
    (hfill : ∑ i, (occupation i : ℕ) = m) (hdefect : ¬ ∀ i, occupation i = 1) :
    U - R ≤ chargePenalty U V occupation := by
…

Mentions: OAI.ContinuumCoulomb.chargePenalty

theorem OAI.ContinuumCoulomb.chargePenalty_singly_occupied line 187

theorem OAI.ContinuumCoulomb.chargePenalty_complement_form_gap line 193

Source documentation

The configuration gap is a gap on arbitrary superpositions, including spin spectators. The kernel consists of every singly occupied spin state.

theorem chargePenalty_complement_form_gap {m : ℕ} {Basis : Type*} [Fintype Basis]
    (U R : ℝ) (V : Fin m → Fin m → ℝ)
    (occupation : Basis → Fin m → Fin 3) (u : Basis → ℂ)
    (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)
    (hkernel : ∀ s, (∀ i, occupation s i = 1) → u s = 0) :
    (U - R) * ∑ s, ‖u s‖ ^ 2 ≤
      ∑ s, chargePenalty U V (occupation s) * ‖u s‖ ^ 2 := by
…

Mentions: OAI.ContinuumCoulomb.chargePenalty