OAI/Analysis/CoulombIonization/FormDomain/FermionicDensity.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAtom.fermionPermutation_apply line 14
  2. lemma OAI.CoulombAtom.permuteConfiguration_mul line 20
  3. lemma OAI.CoulombAtom.fermionPermutation_mul line 26
  4. lemma OAI.CoulombAtom.sectorDirections_permute line 47
  5. def OAI.CoulombAtom.sectorGraphPermutation line 61
  6. lemma OAI.CoulombAtom.sectorGraphPermutation_value line 70
  7. def OAI.CoulombAtom.fermionAverage line 74
  8. lemma OAI.CoulombAtom.fermionAverage_mem line 77
  9. lemma OAI.CoulombAtom.fermionAverage_eq_self line 86
  10. lemma OAI.CoulombAtom.sectorGraphValue_average line 92
  11. def OAI.CoulombAtom.fermionGraphAverage line 99
  12. lemma OAI.CoulombAtom.fermionGraphAverage_value line 107
  13. lemma OAI.CoulombAtom.sectorGraphValue_denseRange line 111
  14. theorem OAI.CoulombAtom.fermionGraphValue_denseRange line 120