OAI/Analysis/CoulombRadii/SpectralTheory/EigenspaceBasisSet.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Coulomb.eigenspaceBasisSet line 69
  2. def OAI.Coulomb.eigenspaceHilbertBasis line 73
  3. def OAI.Coulomb.spectralVectors line 78
  4. lemma OAI.Coulomb.spectralVectors_orthonormal line 80
  5. lemma OAI.Coulomb.spectralVectors_eigen line 84
  6. lemma OAI.Coulomb.spectralVectors_orthogonal_eq_bot line 87
  7. def OAI.Coulomb.compactSpectralBasis line 111
  8. lemma OAI.Coulomb.compactSpectralBasis_eigen line 116
  9. lemma OAI.Coulomb.orthonormal_countable line 121
  10. lemma OAI.Coulomb.compactSpectralBasis_eigen_real line 134
  11. lemma OAI.Coulomb.compactSpectralBasis_eigen_nonneg line 140
  12. lemma OAI.Coulomb.compactSpectralBasis_eigen_le_one line 146