OAI/Analysis/CoulombIonization/FormDomain/CoerciveOperator.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAtom.coercive_operator_bijective line 15
  2. def OAI.CoulombAtom.coerciveEquiv line 50
  3. lemma OAI.CoulombAtom.selfAdjoint_denseRange line 60
  4. def OAI.CoulombAtom.inverseOperator line 69
  5. lemma OAI.CoulombAtom.toPMap_top_ker line 72
  6. lemma OAI.CoulombAtom.inverseOperator_graph line 80
  7. lemma OAI.CoulombAtom.inverseOperator_domain line 94
  8. theorem OAI.CoulombAtom.inverseOperator_selfAdjoint line 104
  9. lemma OAI.CoulombAtom.selfAdjoint_equiv_symm line 132
  10. lemma OAI.CoulombAtom.adjoint_injective_of_denseRange line 141
  11. def OAI.CoulombAtom.formResolvent line 148
  12. lemma OAI.CoulombAtom.formResolvent_injective line 152
  13. lemma OAI.CoulombAtom.formResolvent_selfAdjoint line 158
  14. def OAI.CoulombAtom.representedOperator line 164
  15. theorem OAI.CoulombAtom.representedOperator_selfAdjoint line 168
  16. theorem OAI.CoulombAtom.representedOperator_graph line 175