OAI/Analysis/CoulombIonization/Variational/FullCoulomb.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.electronProjection line 15
  2. def OAI.CoulombAtom.graphComponent line 18
  3. lemma OAI.CoulombAtom.graphComponent_apply line 25
  4. def OAI.CoulombAtom.graphNuclear line 28
  5. def OAI.CoulombAtom.graphPair line 35
  6. def OAI.CoulombAtom.coulombFormOperator line 45
  7. lemma OAI.CoulombAtom.gram_selfAdjoint line 52
  8. lemma OAI.CoulombAtom.gram_inner line 57
  9. def OAI.CoulombAtom.graphFormVector line 63
  10. lemma OAI.CoulombAtom.graphNuclear_norm_sq line 67
  11. lemma OAI.CoulombAtom.graphPair_norm_sq line 72
  12. lemma OAI.CoulombAtom.coulombFormOperator_selfAdjoint line 82
  13. lemma OAI.CoulombAtom.coulombFormOperator_inner line 112