OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/FockResidualIntegral.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact CAR compression of differential orbital residuals. The residual family is only assumed to lie in L2, so the result applies to the actual manufactured orbitals and their finite-box error.

  1. theorem OAI.ContinuumCoulomb.FockResidualIntegral.tensor_pair_slot_integrable line 18
  2. theorem OAI.ContinuumCoulomb.FockResidualIntegral.tensor_pair_slot_integral line 30
  3. theorem OAI.ContinuumCoulomb.FockResidualIntegral.tensorValue_slot_expansion line 50
  4. theorem OAI.ContinuumCoulomb.FockResidualIntegral.tensorValue_slot_integral line 64
  5. theorem OAI.ContinuumCoulomb.FockResidualIntegral.tensorValue_residual_integral line 85