OAI/Analysis/CoulombIonization/Fermionic/Spin.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombPauli.memLp_spin line 27
  2. lemma OAI.CoulombPauli.prod_spin_norm_sq line 41
  3. lemma OAI.CoulombPauli.pi_count_eq line 47
  4. abbrev OAI.CoulombAtom.Pauli.OneParticle line 58
  5. abbrev OAI.CoulombAtom.Pauli.oneMeasure line 59
  6. abbrev OAI.CoulombAtom.Pauli.Many line 60
  7. def OAI.CoulombAtom.Pauli.splitSpin line 62
  8. lemma OAI.CoulombAtom.Pauli.splitSpin_apply line 65
  9. lemma OAI.CoulombAtom.Pauli.splitSpin_preserving line 68
  10. lemma OAI.CoulombAtom.Pauli.memLp_value line 75
  11. def OAI.CoulombAtom.Pauli.toMany line 80
  12. lemma OAI.CoulombAtom.Pauli.toMany_ae line 83
  13. lemma OAI.CoulombAtom.Pauli.toMany_norm_sq line 87
  14. lemma OAI.CoulombAtom.Pauli.toMany_permute line 99
  15. theorem OAI.CoulombAtom.Pauli.form_occupation_le_one line 121
  16. def OAI.CoulombPauli.countVector line 137
  17. lemma OAI.CoulombPauli.countVector_inner line 141
  18. lemma OAI.CoulombPauli.countVector_ae line 147
  19. lemma OAI.CoulombPauli.spin_test_total line 159
  20. lemma OAI.CoulombPauli.spin_test_inner line 174