OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/TensorOccupationSector.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Every antisymmetric coefficient tensor lies in the complete fixed-particle occupation sector, including tensors obtained by continuum projection.

  1. theorem OAI.ContinuumCoulomb.totalNumber_wedgeModes line 14
  2. theorem OAI.ContinuumCoulomb.totalNumber_normalizedTensorExterior line 31
  3. theorem OAI.ContinuumCoulomb.normalizedTensorExterior_occupationSupport line 45
  4. theorem OAI.ContinuumCoulomb.exists_occupationTensor line 50