OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/FockSlaterTensor.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

The normalized determinant of finite Kronecker orbitals is the actual antisymmetric coefficient tensor of an occupation basis vector. Substitution of physical orbitals gives exactly the continuum Slater wave, also for every complex superposition of occupations.

  1. lemma OAI.ContinuumCoulomb.FockSlaterTensor.delta_product line 16
  2. def OAI.ContinuumCoulomb.FockSlaterTensor.basisTensor line 26
  3. lemma OAI.ContinuumCoulomb.FockSlaterTensor.basisTensor_expansion line 29
  4. lemma OAI.ContinuumCoulomb.FockSlaterTensor.basisTensor_antisymmetric line 35
  5. lemma OAI.ContinuumCoulomb.FockSlaterTensor.orderedWedge_selection line 42
  6. lemma OAI.ContinuumCoulomb.FockSlaterTensor.orderedWedge_perm line 48
  7. lemma OAI.ContinuumCoulomb.FockSlaterTensor.tensorExterior_deltas line 53
  8. lemma OAI.ContinuumCoulomb.FockSlaterTensor.tensorExterior_scale line 66
  9. lemma OAI.ContinuumCoulomb.FockSlaterTensor.tensorExterior_basisTensor line 70
  10. lemma OAI.ContinuumCoulomb.FockSlaterTensor.normalizedTensorExterior_basisTensor line 90
  11. lemma OAI.ContinuumCoulomb.FockSlaterTensor.normalizedTensorReadout_basis line 104
  12. def OAI.ContinuumCoulomb.FockSlaterTensor.tensorValue line 109
  13. lemma OAI.ContinuumCoulomb.FockSlaterTensor.tensorValue_basisTensor line 113
  14. def OAI.ContinuumCoulomb.FockSlaterTensor.occupationTensor line 128
  15. lemma OAI.ContinuumCoulomb.FockSlaterTensor.occupationTensor_antisymmetric line 131
  16. lemma OAI.ContinuumCoulomb.FockSlaterTensor.normalizedTensorExterior_occupationTensor line 137
  17. lemma OAI.ContinuumCoulomb.FockSlaterTensor.tensorValue_occupationTensor line 153