OAI/Analysis/CoulombIonization/FormDomain/FormBody.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.formOneBody line 137
  2. def OAI.CoulombAtom.OneBodyIntegrable line 140
  3. lemma OAI.CoulombAtom.formOneBody_scale line 143
  4. lemma OAI.CoulombAtom.OneBodyIntegrable.scale line 148
  5. lemma OAI.CoulombAtom.OneBodyIntegrable.reindex line 153
  6. lemma OAI.CoulombAtom.formOneBody_reindex line 159
  7. lemma OAI.CoulombAtom.formOneBody_sum_disjoint line 174
  8. lemma OAI.CoulombAtom.formOneBody_insertionTerm line 190
  9. lemma OAI.CoulombAtom.formOneBody_wedge line 194
  10. lemma OAI.CoulombAtom.formOneBody_tensor line 203
  11. def OAI.CoulombAtom.insertOrbital line 233
  12. lemma OAI.CoulombAtom.insertOrbital_sobolev line 236
  13. lemma OAI.CoulombAtom.insertion_normalizer line 241
  14. lemma OAI.CoulombAtom.formMass_insertOrbital line 245
  15. lemma OAI.CoulombAtom.formEnergy_insertOrbital line 252
  16. lemma OAI.CoulombAtom.formOneBody_insertOrbital line 259
  17. def OAI.CoulombAtom.FormAvoids line 272
  18. lemma OAI.CoulombAtom.FormAvoids.scale line 275
  19. lemma OAI.CoulombAtom.FormAvoids.reindex line 285
  20. lemma OAI.CoulombAtom.FormAvoids.sum line 291
  21. lemma OAI.CoulombAtom.FormAvoids.tensor line 301
  22. lemma OAI.CoulombAtom.FormAvoids.wedge line 309
  23. lemma OAI.CoulombAtom.FormAvoids.insertOrbital line 315
  24. lemma OAI.CoulombAtom.FormAvoids.mono line 319
  25. lemma OAI.CoulombAtom.radialLocalOrbital_avoids line 323
  26. lemma OAI.CoulombAtom.integrable_coreCoulombAt line 335
  27. lemma OAI.CoulombAtom.coreCoulombAt_eq_formOneBody line 355
  28. lemma OAI.CoulombAtom.coreCoulombAt_insertOrbital line 359
  29. lemma OAI.CoulombAtom.coreCoulombAt_packet line 372