OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/LocalizedOrbitalGram.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The actual localized L2 orbitals form a well-conditioned independent family whenever the exponentially small pair overlaps have a small row sum. In particular their finite span has an actual orthonormal basis.

  1. theorem OAI.ContinuumCoulomb.dualMatrix_quadratic_upper line 16
  2. def OAI.ContinuumCoulomb.localizedOrbitalL2 line 25
  3. theorem OAI.ContinuumCoulomb.localizedOrbitalL2_inner line 29
  4. theorem OAI.ContinuumCoulomb.localizedOrbitalL2_norm line 40
  5. theorem OAI.ContinuumCoulomb.localizedOrbitalL2_sum_norm_sq line 46
  6. def OAI.ContinuumCoulomb.localizedOverlapBound line 59
  7. theorem OAI.ContinuumCoulomb.localizedOverlapBound_nonnegative line 61
  8. theorem OAI.ContinuumCoulomb.planarModeOverlap_offsite line 64
  9. theorem OAI.ContinuumCoulomb.localizedOrbitalL2_sum_bounds line 71
  10. theorem OAI.ContinuumCoulomb.localizedOrbitalL2_linearIndependent line 84
  11. def OAI.ContinuumCoulomb.orthonormalLocalizedOrbitals line 99
  12. theorem OAI.ContinuumCoulomb.orthonormalLocalizedOrbitals_orthonormal line 103
  13. theorem OAI.ContinuumCoulomb.orthonormalLocalizedOrbitals_span line 109