OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ManufacturedManyElectron.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual manufactured Coulomb lower bound on the complete spinful many-electron weak-H1 domain. The sum of orbital occupations is the sum of the actual L2 slice contractions, not a restriction on the admitted states.

  1. theorem OAI.ContinuumCoulomb.manufacturedSlab_manyElectron_lower line 15