OAI/Analysis/CoulombIonization/Localization/PacketDensity.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAtom.integral_one_position line 136
  2. lemma OAI.CoulombAtom.integral_one_configuration line 141
  3. def OAI.CoulombAtom.packetDensity line 147
  4. lemma OAI.CoulombAtom.packetDensity_formula line 150
  5. lemma OAI.CoulombAtom.packetDensity_continuous line 159
  6. lemma OAI.CoulombAtom.packetDensity_support line 168
  7. lemma OAI.CoulombAtom.packetDensity_compact line 178
  8. lemma OAI.CoulombAtom.packetDensity_integrable line 184
  9. lemma OAI.CoulombAtom.packetDensity_memLp line 188
  10. lemma OAI.CoulombAtom.packetDensity_mass line 192
  11. lemma OAI.CoulombAtom.packetDensity_translate line 207
  12. lemma OAI.CoulombAtom.packetDensity_radial line 211
  13. theorem OAI.CoulombAtom.packetDensity_potential line 215
  14. lemma OAI.CoulombAtom.packetDensity_eq_two line 234
  15. lemma OAI.CoulombAtom.radialLocalOrbital_value_config line 240
  16. lemma OAI.CoulombAtom.radialLocalOrbital_potential line 248
  17. lemma OAI.CoulombAtom.radialLocalOrbital_nuclear line 263
  18. lemma OAI.CoulombAtom.integral_join_left line 273
  19. def OAI.CoulombAtom.coreCoulombAt line 283
  20. lemma OAI.CoulombAtom.tensor_packet_pair line 286
  21. lemma OAI.CoulombAtom.tensorCross_packet line 315
  22. theorem OAI.CoulombAtom.local_point_field line 326