OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/LocalizedLinearOrbitals.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Actual finite linear combinations of localized orbitals. Their classical partials remain L2, and their integral Gram matrix is the corresponding finite congruence of the actual overlap matrix.

  1. def OAI.ContinuumCoulomb.localizedLinearOrbital line 15
  2. theorem OAI.ContinuumCoulomb.localizedLinearOrbital_C7 line 19
  3. theorem OAI.ContinuumCoulomb.localizedLinearOrbital_memLp line 23
  4. theorem OAI.ContinuumCoulomb.localizedLinearOrbital_fderiv line 30
  5. theorem OAI.ContinuumCoulomb.localizedLinearOrbital_fderiv_memLp line 40
  6. theorem OAI.ContinuumCoulomb.localizedLinearOrbital_inner line 51