OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/HubbardBottomBounds.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Polynomial bounds on the actual half-filled Hubbard bottom. These control its contribution to the full-continuum complement smallness test.

  1. theorem OAI.ContinuumCoulomb.HubbardGlobal.chargePenalty_abs_bound line 13
  2. theorem OAI.ContinuumCoulomb.HubbardGlobal.fockOperator_diagonal_norm line 47
  3. theorem OAI.ContinuumCoulomb.HubbardGlobal.chargePenaltyFock_norm line 59
  4. theorem OAI.ContinuumCoulomb.HubbardGlobal.hubbardFermionBottom_abs_bound line 67