OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/OrbitalComplementCount.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A coefficient array orthogonal to all tensors of the chosen orbitals has at least one particle outside them. This counts particles, not basis configurations, and so introduces no exponential dimension factor.

  1. theorem OAI.ContinuumCoulomb.complement_coefficient_pointwise line 13
  2. theorem OAI.ContinuumCoulomb.complement_coefficient_occupation_sum line 28
  3. theorem OAI.ContinuumCoulomb.coefficient_set_occupation_eq line 41
  4. theorem OAI.ContinuumCoulomb.complement_coefficient_single_occupation line 52