OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/DiagonalPenalty.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The concrete inverse of a charge-sector penalty

The high block of the Hubbard penalty is diagonal in the occupation basis. That block and its inverse are continuous linear maps satisfying the positivity, symmetry and inverse-norm hypotheses of the second-order perturbation theorem.

  1. def OAI.ContinuumCoulomb.diagonalPenaltyLinear line 22
  2. def OAI.ContinuumCoulomb.diagonalPenalty line 31
  3. theorem OAI.ContinuumCoulomb.diagonalPenalty_apply line 35
  4. theorem OAI.ContinuumCoulomb.diagonalPenalty_form line 39
  5. theorem OAI.ContinuumCoulomb.diagonalPenalty_symmetric line 44
  6. theorem OAI.ContinuumCoulomb.diagonalPenalty_gap line 50
  7. theorem OAI.ContinuumCoulomb.diagonalPenalty_norm_le line 56
  8. theorem OAI.ContinuumCoulomb.diagonalPenalty_inverse_right line 74
  9. theorem OAI.ContinuumCoulomb.diagonalPenalty_inverse_norm line 80
  10. abbrev OAI.ContinuumCoulomb.ChargeHighBasis line 90

    Source documentation

    High occupations exclude the singly occupied spin subspace.

    abbrev ChargeHighBasis {m : ℕ} (occupation : Basis → Fin m → Fin 3) :=
…
  11. theorem OAI.ContinuumCoulomb.chargePenalty_inverse_data line 95

    Source documentation

    The charge-transfer gap gives a concrete bounded inverse on the high occupation space.

    theorem chargePenalty_inverse_data {m : ℕ} (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) :
    let weight : ChargeHighBasis occupation → ℝ :=
…

    Mentions: OAI.ContinuumCoulomb.ChargeHighBasis