OAI/Analysis/CoulombIonization/Variational/RootCoulomb.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAtom.lp_norm_sq line 21
  2. lemma OAI.CoulombAtom.div_sqrt_norm_sq line 30
  3. def OAI.CoulombAtom.rootCoulombFn line 35
  4. lemma OAI.CoulombAtom.rootCoulombFn_memLp line 39
  5. def OAI.CoulombAtom.rootCoulombLp line 53
  6. lemma OAI.CoulombAtom.rootCoulombLp_norm_sq line 58
  7. lemma OAI.CoulombAtom.rootCoulombLp_add line 69
  8. lemma OAI.CoulombAtom.rootCoulombLp_smul line 89
  9. lemma OAI.CoulombAtom.rootCoulombLp_bound line 106
  10. def OAI.CoulombAtom.rootCoulombMap line 121