OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/LocalizedFourIndex.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Four-index Coulomb integrals of the actual localized orbitals. Each unequal-index pair gives exponentially small Coulomb coefficients, uniformly in the other pair. Diagonal pairs recover the actual direct interaction.

  1. theorem OAI.ContinuumCoulomb.localizedPotentialBound_nonnegative line 13
  2. theorem OAI.ContinuumCoulomb.localizedTransition_coulomb_integrable_bound line 18
  3. theorem OAI.ContinuumCoulomb.localizedTransition_potential_nonnegative line 29
  4. theorem OAI.ContinuumCoulomb.localizedTransition_potential_continuous line 35
  5. def OAI.ContinuumCoulomb.localizedFourIndex line 40
  6. theorem OAI.ContinuumCoulomb.localizedFourIndex_integrable line 43
  7. theorem OAI.ContinuumCoulomb.localizedFourIndex_nonnegative line 52
  8. theorem OAI.ContinuumCoulomb.localizedTransitionPacket_pair line 57
  9. theorem OAI.ContinuumCoulomb.localizedFourIndex_symmetric line 71
  10. theorem OAI.ContinuumCoulomb.localizedFourIndex_diagonal line 76
  11. theorem OAI.ContinuumCoulomb.localizedFourIndex_le_overlap line 83
  12. def OAI.ContinuumCoulomb.localizedFourIndexConstant line 92
  13. theorem OAI.ContinuumCoulomb.localizedFourIndexConstant_nonnegative line 94
  14. theorem OAI.ContinuumCoulomb.localizedFourIndex_decay_left line 97
  15. theorem OAI.ContinuumCoulomb.localizedFourIndex_decay_right line 107
  16. theorem OAI.ContinuumCoulomb.localizedFourIndex_offsite line 113