OAI/Analysis/CoulombIonization/FormDomain/TrialSmoothTest.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAtom.integrable_norm_sq_div_of_support line 20
  2. def OAI.CoulombAtom.smoothForm line 35
  3. theorem OAI.CoulombAtom.smoothForm_admissible line 39
  4. def OAI.CoulombAtom.antisymmetrize line 64
  5. lemma OAI.CoulombAtom.complex_sign_sq line 67
  6. lemma OAI.CoulombAtom.antisymmetrize_perm line 75
  7. lemma OAI.CoulombAtom.antisymmetrize_smooth line 98
  8. def OAI.CoulombAtom.permuteConfig line 106
  9. lemma OAI.CoulombAtom.antisymmetrize_compact line 115
  10. def OAI.CoulombAtom.trialCenter line 128
  11. lemma OAI.CoulombAtom.trialCenter_norm line 131
  12. lemma OAI.CoulombAtom.trialCenter_separated line 137
  13. def OAI.CoulombAtom.trialBump line 151
  14. def OAI.CoulombAtom.trialSeed line 157
  15. lemma OAI.CoulombAtom.trialSeed_smooth line 159
  16. lemma OAI.CoulombAtom.trialSeed_compact line 162
  17. lemma OAI.CoulombAtom.trialSeed_support line 165
  18. lemma OAI.CoulombAtom.trialSeed_dist line 172
  19. lemma OAI.CoulombAtom.trialSeed_nucleus line 176
  20. lemma OAI.CoulombAtom.trialSeed_pair line 184
  21. lemma OAI.CoulombAtom.trialSeed_center line 199
  22. lemma OAI.CoulombAtom.trialSeed_center_permuted line 204
  23. lemma OAI.CoulombAtom.antisymmetrize_trialSeed_nonzero line 217
  24. lemma OAI.CoulombAtom.antisymmetrize_has_nonzero_term line 227
  25. lemma OAI.CoulombAtom.antisymmetrize_trialSeed_nucleus line 234
  26. lemma OAI.CoulombAtom.antisymmetrize_trialSeed_pair line 239
  27. lemma OAI.CoulombAtom.norm_real_mul_sq line 246
  28. theorem OAI.CoulombAtom.exists_normalized_smoothForm line 249
  29. theorem OAI.CoulombAtom.formDomain_nonempty line 286
  30. lemma OAI.CoulombAtom.formValues_nonempty line 297