OAI/Analysis/CoulombIonization/FormDomain/FullSpectral.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.CoulombAtom.fermionSpace_nontrivial line 16
  2. def OAI.CoulombAtom.coulombResolvent line 26
  3. def OAI.CoulombAtom.coulombHamiltonian line 31
  4. lemma OAI.CoulombAtom.coulombResolvent_injective line 35
  5. lemma OAI.CoulombAtom.coulombResolvent_selfAdjoint line 40
  6. theorem OAI.CoulombAtom.coulombHamiltonian_selfAdjoint line 45
  7. lemma OAI.CoulombAtom.shiftedCoulombFormOperator_pair line 50
  8. theorem OAI.CoulombAtom.coulombHamiltonian_graph line 58
  9. def OAI.CoulombAtom.spectralEnergy line 69
  10. theorem OAI.CoulombAtom.coulombHamiltonian_spectrum_real line 72
  11. theorem OAI.CoulombAtom.spectralEnergy_eq_energy line 77