OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/OccupationSector.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The occupation-amplitude map is a linear equivalence onto the entire fixed-particle exterior sector, preserving its actual occupation inner product. No state in that sector is excluded.

  1. def OAI.ContinuumCoulomb.OccupationFock.coordinateIsometry line 16
  2. lemma OAI.ContinuumCoulomb.OccupationFock.vector_injective line 21
  3. lemma OAI.ContinuumCoulomb.OccupationFock.vector_inner line 27
  4. def OAI.ContinuumCoulomb.OccupationFock.particleSector line 36
  5. def OAI.ContinuumCoulomb.OccupationFock.synthesisLinear line 46
  6. def OAI.ContinuumCoulomb.OccupationFock.sectorSynthesis line 51
  7. def OAI.ContinuumCoulomb.OccupationFock.sectorEquiv line 55
  8. lemma OAI.ContinuumCoulomb.OccupationFock.sectorEquiv_apply line 65
  9. lemma OAI.ContinuumCoulomb.OccupationFock.sectorEquiv_inner line 68
  10. lemma OAI.ContinuumCoulomb.OccupationFock.sectorEquiv_mass line 72