OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/TensorComplementBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Parseval identifies the coefficient occupation count with the actual partial integrals of a many-electron wave function.

  1. theorem OAI.ContinuumCoulomb.first_fiber_occupation_eq line 14
  2. theorem OAI.ContinuumCoulomb.first_fiber_complement_bound line 46