OAI/Analysis/CoulombIonization/ThomasFermi/FlatFermionAverage.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombNeumann.flat_complex_sign_norm line 19
  2. lemma OAI.CoulombNeumann.flat_sum_spins_permutation line 23
  3. def OAI.CoulombNeumann.flatPermutation line 32
  4. lemma OAI.CoulombNeumann.flatPermutation_apply line 36
  5. lemma OAI.CoulombNeumann.flatPermutation_preserving line 40
  6. lemma OAI.CoulombNeumann.flatPermutation_mul line 44
  7. lemma OAI.CoulombNeumann.flatPermutation_single line 50
  8. def OAI.CoulombNeumann.flatSignedPermutation line 55
  9. def OAI.CoulombNeumann.flatFermionAverage line 60
  10. lemma OAI.CoulombNeumann.flatSignedPermutation_mul line 64
  11. lemma OAI.CoulombNeumann.flatFermionAverage_fixed line 72
  12. lemma OAI.CoulombNeumann.flatFermionAverage_anti line 87
  13. lemma OAI.CoulombNeumann.flatSignedPermutation_contDiff line 96
  14. lemma OAI.CoulombNeumann.flatFermionAverage_contDiff line 102
  15. lemma OAI.CoulombNeumann.flatSignedPermutation_memLp line 108
  16. lemma OAI.CoulombNeumann.flatFermionAverage_memLp line 115
  17. lemma OAI.CoulombNeumann.flatSignedPermutation_mass line 120
  18. lemma OAI.CoulombNeumann.flatFermionAverage_mass_le line 133