OAI/Analysis/CoulombIonization/FormDomain/CompactEigenbasis.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.compactEigenspaceIndex line 20
  2. def OAI.CoulombAtom.compactEigenspaceBasis line 23
  3. abbrev OAI.CoulombAtom.CompactSpectralIndex line 27
  4. def OAI.CoulombAtom.compactSpectralVector line 29
  5. lemma OAI.CoulombAtom.compactSpectralVector_eigen line 32
  6. lemma OAI.CoulombAtom.compactSpectralVector_orthonormal line 36
  7. lemma OAI.CoulombAtom.compactSpectralVector_orthogonal_eq_bot line 41
  8. def OAI.CoulombAtom.compactSpectralBasis line 63
  9. lemma OAI.CoulombAtom.compactSpectralBasis_apply line 69
  10. lemma OAI.CoulombAtom.compactSpectralBasis_eigen line 74
  11. lemma OAI.CoulombAtom.orthonormal_countable line 87
  12. lemma OAI.CoulombAtom.hilbertBasis_hasSum_norm_inner line 111
  13. lemma OAI.CoulombAtom.hilbertBasis_frame_trace line 116
  14. instance OAI.CoulombAtom.orbitalHilbert_secondCountable line 137
  15. abbrev OAI.CoulombAtom.CoherentIndex line 141
  16. def OAI.CoulombAtom.coherentBasis line 144
  17. instance OAI.CoulombAtom.coherentIndex_countable line 150
  18. lemma OAI.CoulombAtom.coherentBasis_eigen line 154
  19. lemma OAI.CoulombAtom.coherentBasis_inner_eigen line 159
  20. lemma OAI.CoulombAtom.coherentBasis_eigenvalue_eq line 166
  21. def OAI.CoulombAtom.coherentWeight line 175
  22. lemma OAI.CoulombAtom.coherentWeight_eq line 178
  23. lemma OAI.CoulombAtom.coherentWeight_nonneg line 184
  24. lemma OAI.CoulombAtom.coherentBasis_real_eigen line 190
  25. lemma OAI.CoulombAtom.coherentWeight_le_one line 198
  26. lemma OAI.CoulombAtom.coherentWeight_hasSum line 207