OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/ElectronSlotBound.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The one-electron finite-rank lower bound acts on every electron slot. All coordinate changes preserve the full spinful weak-H1 domain.

  1. def OAI.ContinuumCoulomb.electronSlotKinetic line 15
  2. theorem OAI.ContinuumCoulomb.sum_electronSlotKinetic line 18
  3. theorem OAI.ContinuumCoulomb.coreKinetic_permutation_one line 24
  4. theorem OAI.ContinuumCoulomb.oneElectronCoordinates_core line 42
  5. theorem OAI.ContinuumCoulomb.corePotential_permutation_one line 53
  6. def OAI.ContinuumCoulomb.electronSlotOrbitalMass line 71
  7. def OAI.ContinuumCoulomb.totalOrbitalMass line 76
  8. theorem OAI.ContinuumCoulomb.electronSlot_projection_lower line 81
  9. theorem OAI.ContinuumCoulomb.manyElectron_projection_lower line 96