OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/FockEnergyError.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Operator errors control every normalized occupation-sector energy with polynomial mode dependence. The tensor and exterior norms are identified.

  1. theorem OAI.ContinuumCoulomb.occupationInner_fockCoordinates line 16
  2. theorem OAI.ContinuumCoulomb.occupationNormSq_fockCoordinates line 21
  3. theorem OAI.ContinuumCoulomb.occupationInner_operator_error line 26
  4. theorem OAI.ContinuumCoulomb.finiteTensorState_occupationMass line 44