OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/HubbardVariationalWitness.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Near-minimizers of the actual half-filled Hubbard Rayleigh quotient are represented by antisymmetric tensors, with no restriction to spin product states or a proper subspace of the occupation sector.

  1. theorem OAI.ContinuumCoulomb.HubbardGlobal.exists_halfFilled_unit_mass line 16
  2. theorem OAI.ContinuumCoulomb.HubbardGlobal.hubbardFermionBottom_approximate line 23
  3. theorem OAI.ContinuumCoulomb.HubbardGlobal.halfFilled_exists_tensor line 38
  4. theorem OAI.ContinuumCoulomb.HubbardGlobal.hubbardFermionBottom_tensor_approximate line 46