OAI/Analysis/CoulombIonization/Variational/CorrelatedFiniteInsertion.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CoulombAtom.price_le_correlated_finite_insertion line 17
  2. def OAI.CoulombAtom.spinLift line 49
  3. lemma OAI.CoulombAtom.spinLift_smooth line 51
  4. lemma OAI.CoulombAtom.spinLift_compact line 57
  5. lemma OAI.CoulombAtom.spinLift_separated line 63
  6. lemma OAI.CoulombAtom.spinLift_fderiv line 70
  7. lemma OAI.CoulombAtom.spinLift_inner line 75
  8. lemma OAI.CoulombAtom.spinLift_weight line 95
  9. lemma OAI.CoulombAtom.spinLift_mass line 107
  10. lemma OAI.CoulombAtom.spinLift_derivative_mass line 111
  11. lemma OAI.CoulombAtom.spinSpace_integral_spatial line 117
  12. def OAI.CoulombAtom.finiteOrbitalDensity line 128
  13. def OAI.CoulombAtom.finiteOrbitalKinetic line 131
  14. def OAI.CoulombAtom.finiteOrbitalEnergy line 136
  15. lemma OAI.CoulombAtom.finiteOrbitalEnergy_reindex line 144
  16. theorem OAI.CoulombAtom.price_le_correlated_fintype_insertion line 164