OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/FullTensorComplement.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual antisymmetric H1 remainder has a missing orbital occupation on the full spin-space product measure.

  1. theorem OAI.ContinuumCoulomb.finiteTensorRemainder_flat_occupation line 14