OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/FockOneBodyIntegral.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The one-body potential integral of an actual finite orbital tensor is the corresponding CAR matrix element. Singular potentials need only the integrability of the one-orbital matrix entries.

  1. theorem OAI.ContinuumCoulomb.FockOneBodyIntegral.tensorValue_bilinear line 22
  2. theorem OAI.ContinuumCoulomb.FockOneBodyIntegral.tensorValue_weighted_expansion line 37
  3. theorem OAI.ContinuumCoulomb.FockOneBodyIntegral.weighted_tensor_pair_integrable line 50
  4. theorem OAI.ContinuumCoulomb.FockOneBodyIntegral.tensorValue_weighted_integrable line 61
  5. theorem OAI.ContinuumCoulomb.FockOneBodyIntegral.tensorValue_weighted_integral line 71
  6. theorem OAI.ContinuumCoulomb.FockOneBodyIntegral.delta_insert_product line 97
  7. theorem OAI.ContinuumCoulomb.FockOneBodyIntegral.oneBody_contraction line 114
  8. theorem OAI.ContinuumCoulomb.FockOneBodyIntegral.tensorValue_oneBody_integral line 142