OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CoreTensorFiber.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The last-coordinate contraction in full spin space is exactly the core-slice orbital coefficient used by the many-electron energy bound.

  1. def OAI.ContinuumCoulomb.spinConfigurationPoint line 18
  2. theorem OAI.ContinuumCoulomb.spinConfigurationPoint_coordinates line 21
  3. theorem OAI.ContinuumCoulomb.cubeState_snoc line 27
  4. theorem OAI.ContinuumCoulomb.lastTensorFiber_coreSlice line 51
  5. theorem OAI.ContinuumCoulomb.coreOrbitalCoefficient_slice line 65
  6. theorem OAI.ContinuumCoulomb.lastTensorFiber_realOrbital_core line 74
  7. theorem OAI.ContinuumCoulomb.lastTensorFiber_realOrbital_integral line 115
  8. theorem OAI.ContinuumCoulomb.coreOrbitalMass_last_occupation line 143
  9. theorem OAI.ContinuumCoulomb.coreOrbitalMass_first_occupation line 174