OAI/Analysis/CoulombIonization/Variational/MasterWidth.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.masterExponent line 16
  2. def OAI.CoulombAtom.masterBaseDistance line 18
  3. def OAI.CoulombAtom.masterWidth line 20
  4. lemma OAI.CoulombAtom.masterExponent_pos line 23
  5. lemma OAI.CoulombAtom.masterExponent_nonneg line 24
  6. lemma OAI.CoulombAtom.powerProfile_interval line 26
  7. def OAI.CoulombAtom.cappedWidthProfile line 42
  8. lemma OAI.CoulombAtom.cappedWidthProfile_small line 44
  9. lemma OAI.CoulombAtom.cappedWidthProfile_large line 48
  10. lemma OAI.CoulombAtom.cappedWidthProfile_ordered_bound line 51
  11. lemma OAI.CoulombAtom.cappedWidthProfile_norm_bound line 82
  12. lemma OAI.CoulombAtom.masterBaseDistance_lipschitz line 92
  13. lemma OAI.CoulombAtom.masterWidth_pos line 95
  14. lemma OAI.CoulombAtom.masterWidth_upper line 100
  15. lemma OAI.CoulombAtom.masterWidth_lower line 107
  16. lemma OAI.CoulombAtom.masterWidth_lipschitz line 115
  17. def OAI.CoulombAtom.widthKernel line 147
  18. lemma OAI.CoulombAtom.invCube_norm_sub_le line 150
  19. lemma OAI.CoulombAtom.normalizedArgument_distance line 164
  20. lemma OAI.CoulombAtom.widthKernel_active_norm_bound line 192
  21. lemma OAI.CoulombAtom.widthKernel_lipschitz line 230