OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/OrthonormalLocalizedModes.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The actual spectral inverse-square-root correction applied to the manufactured orbitals. These are C1 decaying orthonormal spatial functions; injectively occupied spatial/spin modes give actual normalized fermions.

  1. def OAI.ContinuumCoulomb.localizedModeGram line 16
  2. theorem OAI.ContinuumCoulomb.localizedModeGram_isHermitian line 19
  3. def OAI.ContinuumCoulomb.correctedLocalizedCoefficients line 29
  4. def OAI.ContinuumCoulomb.correctedLocalizedMode line 32
  5. theorem OAI.ContinuumCoulomb.correctedLocalizedCoefficients_gram line 35
  6. theorem OAI.ContinuumCoulomb.correctedLocalizedCoefficients_entries line 47
  7. theorem OAI.ContinuumCoulomb.correctedLocalizedMode_inner line 55
  8. theorem OAI.ContinuumCoulomb.correctedLocalizedMode_C1 line 73
  9. theorem OAI.ContinuumCoulomb.correctedLocalizedMode_memLp line 77
  10. theorem OAI.ContinuumCoulomb.correctedLocalizedMode_partial_memLp line 81
  11. def OAI.ContinuumCoulomb.correctedLocalizedSlaterState line 86
  12. theorem OAI.ContinuumCoulomb.correctedLocalizedSlaterState_antisymmetric line 91
  13. theorem OAI.ContinuumCoulomb.correctedLocalizedSlaterState_normalized line 96