OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CoreOrbitalCongruence.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The core occupation depends only on the L2 state. A global phase and fermionic coordinate permutations preserve it.

  1. theorem OAI.ContinuumCoulomb.coreOrbitalCoefficient_phase_ae line 13
  2. theorem OAI.ContinuumCoulomb.coreOrbitalMass_phase line 33
  3. theorem OAI.ContinuumCoulomb.coreOrbitalMass_permutation line 49
  4. theorem OAI.ContinuumCoulomb.totalOrbitalMass_antisymmetric line 59