OAI/Analysis/CoulombIonization/FormDomain/Form.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.FormZeroAt line 115
  2. lemma OAI.CoulombAtom.insertionTerm_zero line 118
  3. lemma OAI.CoulombAtom.insertionTerms_disjoint line 129
  4. lemma OAI.CoulombAtom.formMass_wedge line 157
  5. lemma OAI.CoulombAtom.formEnergy_wedge line 163
  6. lemma OAI.CoulombAtom.tensor_zero_left line 169
  7. lemma OAI.CoulombAtom.tensor_zero_right line 184
  8. lemma OAI.CoulombAtom.tensor_insertion_disjoint line 199
  9. theorem OAI.CoulombAtom.normalized_wedge_trial line 211
  10. def OAI.CoulombAtom.formKinetic line 236
  11. def OAI.CoulombAtom.formNuclear line 239
  12. def OAI.CoulombAtom.formRepulsion line 242
  13. lemma OAI.CoulombAtom.formEnergy_parts line 245
  14. lemma OAI.CoulombAtom.formKinetic_nonneg line 248
  15. lemma OAI.CoulombAtom.formNuclear_nonneg line 252
  16. lemma OAI.CoulombAtom.integral_product_join line 257
  17. lemma OAI.CoulombAtom.tensor_kinetic_left line 265
  18. lemma OAI.CoulombAtom.tensor_kinetic_right line 272
  19. lemma OAI.CoulombAtom.formKinetic_tensor line 279
  20. lemma OAI.CoulombAtom.tensor_nuclear_left line 292
  21. lemma OAI.CoulombAtom.tensor_nuclear_right line 302
  22. lemma OAI.CoulombAtom.formNuclear_tensor line 311
  23. lemma OAI.CoulombAtom.tensor_pair_left line 323
  24. def OAI.CoulombAtom.tensorCross line 334
  25. lemma OAI.CoulombAtom.formRepulsion_tensor_one line 338
  26. lemma OAI.CoulombAtom.formEnergy_tensor_one line 374