OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/RealSpinOrbitals.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Spin lifting of real C1 orbitals into the actual fermionic weak-H1 domain. Any injective list of occupied orthonormal spatial/spin modes gives a normalized antisymmetric state on the full configuration space.

  1. def OAI.ContinuumCoulomb.realSpinOrbital line 14
  2. theorem OAI.ContinuumCoulomb.realSpinOrbital_C1 line 17
  3. theorem OAI.ContinuumCoulomb.realSpinOrbital_memLp line 23
  4. theorem OAI.ContinuumCoulomb.realSpinOrbital_fderiv line 31
  5. theorem OAI.ContinuumCoulomb.realSpinOrbital_partial_memLp line 41
  6. theorem OAI.ContinuumCoulomb.realSpinOrbital_inner line 52
  7. theorem OAI.ContinuumCoulomb.selectedRealSpinOrbitals_orthonormal line 73
  8. def OAI.ContinuumCoulomb.selectedRealSlaterState line 91
  9. theorem OAI.ContinuumCoulomb.selectedRealSlaterState_antisymmetric line 100
  10. theorem OAI.ContinuumCoulomb.selectedRealSlaterState_normalized line 106