OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/OccupationFock.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The actual n-particle exterior sector is exactly the Euclidean space of amplitudes on n-element occupied subsets, with no omitted states.

  1. def OAI.ContinuumCoulomb.OccupationFock.vector line 16
  2. lemma OAI.ContinuumCoulomb.OccupationFock.coordinates_basis line 19
  3. lemma OAI.ContinuumCoulomb.OccupationFock.vector_coordinates line 29
  4. lemma OAI.ContinuumCoulomb.OccupationFock.vector_mass line 39
  5. lemma OAI.ContinuumCoulomb.OccupationFock.vector_support line 43
  6. lemma OAI.ContinuumCoulomb.OccupationFock.exists_vector_of_support line 52
  7. lemma OAI.ContinuumCoulomb.OccupationFock.vector_normalizedTensorExterior line 70
  8. theorem OAI.ContinuumCoulomb.HubbardGlobal.isHalfFilled_exists_occupationVector line 79