OAI/Analysis/CoulombRadii/FieldAnalysis/FermionicCoefficients.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Coulomb.FermionicCoefficients line 14
  2. lemma OAI.Coulomb.FermionicCoefficients.vanish_of_repeat line 17
  3. lemma OAI.Coulomb.FermionicCoefficients.pointwise_occupation line 34
  4. lemma OAI.Coulomb.FermionicCoefficients.occupation_sum line 56
  5. def OAI.Coulomb.coefficientPermEquiv line 64
  6. lemma OAI.Coulomb.FermionicCoefficients.norm_permute line 71
  7. lemma OAI.Coulomb.FermionicCoefficients.occupation_eq line 79
  8. theorem OAI.Coulomb.FermionicCoefficients.pauli_bound line 92
  9. def OAI.Coulomb.permuteIsometry line 109
  10. lemma OAI.Coulomb.permuteIsometry_apply line 113
  11. lemma OAI.Coulomb.permute_measurePreserving line 118
  12. lemma OAI.Coulomb.integral_permute line 122
  13. def OAI.Coulomb.spinPermEquiv line 129
  14. lemma OAI.Coulomb.sign_complex_norm line 135
  15. lemma OAI.Coulomb.Antisymmetric.norm_permute line 139
  16. lemma OAI.Coulomb.antisymmetric_expectation_permute line 145
  17. def OAI.Coulomb.tensorOrbital line 161
  18. lemma OAI.Coulomb.position_permute line 165
  19. lemma OAI.Coulomb.tensorOrbital_permute line 168
  20. def OAI.Coulomb.orbitalCoefficient line 176
  21. lemma OAI.Coulomb.orbitalCoefficient_antisymmetric line 180