OAI/Analysis/CoulombIonization/Variational/InsertionSwap.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAtom.corePerm_last line 114
  2. lemma OAI.CoulombAtom.corePerm_castSucc line 121
  3. lemma OAI.CoulombAtom.perm_fixed_last_is_core line 126
  4. def OAI.CoulombAtom.insertionSwap line 144
  5. lemma OAI.CoulombAtom.insertionSwap_last line 147
  6. lemma OAI.CoulombAtom.insertionSwap_self line 149
  7. lemma OAI.CoulombAtom.insertionSwap_symm line 151
  8. lemma OAI.CoulombAtom.insertion_coset line 154
  9. lemma OAI.CoulombAtom.real_sign_sq line 165
  10. lemma OAI.CoulombAtom.tensor_coreAntisymmetric line 178
  11. lemma OAI.CoulombAtom.CoreAntisymmetric.fixed_last line 206
  12. def OAI.CoulombAtom.insertionTerm line 213
  13. def OAI.CoulombAtom.wedgeForm line 217
  14. lemma OAI.CoulombAtom.insertionTerm_value line 220
  15. lemma OAI.CoulombAtom.SobolevVector.insertionTerm line 226
  16. lemma OAI.CoulombAtom.wedgeForm_fermion line 230
  17. lemma OAI.CoulombAtom.formMass_insertionTerm line 273
  18. lemma OAI.CoulombAtom.formEnergy_insertionTerm line 277