OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/OrbitalTensor.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Integrals of actual finite orbital tensors, including the exact one-body head-slot contraction. All coefficients come from the orbital integrals; no effective matrix identity is a premise.

  1. lemma OAI.ContinuumCoulomb.OrbitalTensor.delta_product line 16
  2. lemma OAI.ContinuumCoulomb.OrbitalTensor.prod_erase_zero line 26
  3. lemma OAI.ContinuumCoulomb.OrbitalTensor.head_pair_sum line 39
  4. lemma OAI.ContinuumCoulomb.OrbitalTensor.prod_erase_zero_one line 49
  5. lemma OAI.ContinuumCoulomb.OrbitalTensor.headTwo_pair_sum line 70
  6. lemma OAI.ContinuumCoulomb.OrbitalTensor.tensorValue_memLp line 84
  7. lemma OAI.ContinuumCoulomb.OrbitalTensor.bilinear_expansion line 94
  8. lemma OAI.ContinuumCoulomb.OrbitalTensor.inner_integral line 106
  9. lemma OAI.ContinuumCoulomb.OrbitalTensor.head_oneBody_integral line 133
  10. lemma OAI.ContinuumCoulomb.OrbitalTensor.oneBody_CAR_compression line 185
  11. lemma OAI.ContinuumCoulomb.OrbitalTensor.head_twoBody_integral line 204
  12. lemma OAI.ContinuumCoulomb.OrbitalTensor.twoBody_CAR_compression line 267
  13. lemma OAI.ContinuumCoulomb.OrbitalTensor.slater_oneBody_CAR_compression line 293
  14. lemma OAI.ContinuumCoulomb.OrbitalTensor.slater_twoBody_CAR_compression line 309