OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/OrbitalBasisExtension.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Extending the finitely many chosen orbitals supplies Parseval for arbitrary continuum states, including their orthogonal remainder.

  1. theorem OAI.ContinuumCoulomb.finite_orbitals_basis_extension line 12