OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/SlaterOccupation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The actual normalized Slater waves for the sorted occupied subsets of finitely many orthonormal spin orbitals form an orthonormal family. Their finite linear combination map is a genuine L2 isometry.

  1. abbrev OAI.ContinuumCoulomb.SlaterOccupation.Occupied line 17
  2. def OAI.ContinuumCoulomb.SlaterOccupation.selection line 19
  3. lemma OAI.ContinuumCoulomb.SlaterOccupation.selection_mem line 22
  4. lemma OAI.ContinuumCoulomb.SlaterOccupation.selection_coincidence line 26
  5. lemma OAI.ContinuumCoulomb.SlaterOccupation.selection_delta_product line 51
  6. def OAI.ContinuumCoulomb.SlaterOccupation.selectedOrbitals line 69
  7. def OAI.ContinuumCoulomb.SlaterOccupation.wave line 72
  8. lemma OAI.ContinuumCoulomb.SlaterOccupation.wave_memLp line 75
  9. lemma OAI.ContinuumCoulomb.SlaterOccupation.determinant_overlap line 79
  10. lemma OAI.ContinuumCoulomb.SlaterOccupation.wave_overlap line 97
  11. def OAI.ContinuumCoulomb.SlaterOccupation.orbitalL2 line 125
  12. lemma OAI.ContinuumCoulomb.SlaterOccupation.orbitalL2_inner line 128
  13. lemma OAI.ContinuumCoulomb.SlaterOccupation.orbitalL2_orthonormal line 140
  14. def OAI.ContinuumCoulomb.SlaterOccupation.synthesis line 147
  15. def OAI.ContinuumCoulomb.SlaterOccupation.synthesisIsometry line 153