OAI/Analysis/CoulombIonization/Localization/RadialPacketBase.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.radialPacketBase line 132
  2. lemma OAI.CoulombAtom.radialPacketBase_smooth line 135
  3. lemma OAI.CoulombAtom.radialPacketBase_zero line 140
  4. lemma OAI.CoulombAtom.radialPacketBase_compact line 144
  5. lemma OAI.CoulombAtom.radialPacketBase_zero_value line 151
  6. def OAI.CoulombAtom.radialPacketSeed line 154
  7. lemma OAI.CoulombAtom.radialPacketSeed_smooth line 156
  8. lemma OAI.CoulombAtom.radialPacketSeed_compact line 159
  9. lemma OAI.CoulombAtom.radialPacketSeed_radial line 162
  10. lemma OAI.CoulombAtom.radialPacketSeed_support line 165
  11. lemma OAI.CoulombAtom.radialPacketSeed_mass_pos line 170
  12. def OAI.CoulombAtom.radialScaledSeed line 179
  13. def OAI.CoulombAtom.radialScaledRaw line 181
  14. lemma OAI.CoulombAtom.radialScaledSeed_smooth line 183
  15. lemma OAI.CoulombAtom.radialScaledSeed_compact line 186
  16. lemma OAI.CoulombAtom.radialScaledRaw_sobolev line 189
  17. lemma OAI.CoulombAtom.radialScaledRaw_mass_pos line 200
  18. lemma OAI.CoulombAtom.radialScaledRaw_gradient line 211
  19. lemma OAI.CoulombAtom.radialScaledRaw_mass line 220
  20. lemma OAI.CoulombAtom.radialScaledRaw_kinetic line 230
  21. def OAI.CoulombAtom.radialScaledOrbital line 242
  22. lemma OAI.CoulombAtom.radialScaledOrbital_admissible line 245
  23. def OAI.CoulombAtom.radialPacketKinetic line 248
  24. lemma OAI.CoulombAtom.radialPacketKinetic_nonneg line 251
  25. lemma OAI.CoulombAtom.radialScaledOrbital_kinetic line 254
  26. def OAI.CoulombAtom.radialCenterShift line 264
  27. def OAI.CoulombAtom.radialLocalSeed line 267
  28. def OAI.CoulombAtom.radialLocalRaw line 270
  29. lemma OAI.CoulombAtom.radialLocalSeed_smooth line 272
  30. lemma OAI.CoulombAtom.radialLocalSeed_compact line 275
  31. lemma OAI.CoulombAtom.radialLocalRaw_sobolev line 279
  32. lemma OAI.CoulombAtom.radialLocalRaw_gradient line 291
  33. lemma OAI.CoulombAtom.radialLocalRaw_mass line 302
  34. lemma OAI.CoulombAtom.radialLocalRaw_kinetic line 309
  35. def OAI.CoulombAtom.radialLocalOrbital line 320
  36. lemma OAI.CoulombAtom.radialLocalOrbital_admissible line 323
  37. lemma OAI.CoulombAtom.radialLocalOrbital_kinetic line 329
  38. lemma OAI.CoulombAtom.radialLocalSeed_support line 337
  39. lemma OAI.CoulombAtom.radialLocalRaw_zero line 344
  40. lemma OAI.CoulombAtom.radialLocalOrbital_zero line 358