OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/MixedSlater.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Mixed determinant matrix elements for different occupied orbital families. Every coefficient is an actual integral; the remaining finite permutation sums are precisely the minors needed in Fock compression.

  1. lemma OAI.ContinuumCoulomb.MixedSlater.determinant_overlap_integral line 18
  2. lemma OAI.ContinuumCoulomb.MixedSlater.oneBodyTensor_integrable line 42
  3. lemma OAI.ContinuumCoulomb.MixedSlater.oneBodyTensor_integral line 52
  4. lemma OAI.ContinuumCoulomb.MixedSlater.twoBodyTensor_integrable line 61
  5. lemma OAI.ContinuumCoulomb.MixedSlater.twoBodyTensor_integral line 72
  6. lemma OAI.ContinuumCoulomb.MixedSlater.slotTensor_integral line 83
  7. lemma OAI.ContinuumCoulomb.MixedSlater.slotDeterminant_expansion line 103
  8. lemma OAI.ContinuumCoulomb.MixedSlater.slotDeterminant_integral line 117
  9. lemma OAI.ContinuumCoulomb.MixedSlater.determinant_oneBody_expansion line 141
  10. lemma OAI.ContinuumCoulomb.MixedSlater.determinant_oneBody_integral line 157
  11. lemma OAI.ContinuumCoulomb.MixedSlater.determinant_twoBody_expansion line 186
  12. lemma OAI.ContinuumCoulomb.MixedSlater.determinant_twoBody_integral line 206