OAI/Analysis/CoulombRadii/FieldAnalysis/DeterminantWave.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Coulomb.determinantWave line 28
  2. lemma OAI.Coulomb.determinantWave_expansion line 31
  3. lemma OAI.Coulomb.determinantWave_permute line 36
  4. lemma OAI.Coulomb.determinantWave_memLp line 41
  5. lemma OAI.Coulomb.sign_star_mul line 48
  6. lemma OAI.Coulomb.determinantWave_norm_sq line 52
  7. def OAI.Coulomb.slaterWave line 101
  8. lemma OAI.Coulomb.slaterWave_memLp line 104
  9. lemma OAI.Coulomb.slaterWave_antisymmetric line 109
  10. lemma OAI.Coulomb.slaterWave_normalized line 116
  11. lemma OAI.Coulomb.perm_eq_of_eq_off line 126
  12. lemma OAI.Coulomb.permutation_minor_orthogonality line 138
  13. lemma OAI.Coulomb.slater_one_body_trace_algebra line 155
  14. lemma OAI.Coulomb.tensor_weight_factor line 176
  15. lemma OAI.Coulomb.weighted_tensor_integrable line 195
  16. lemma OAI.Coulomb.weighted_tensor_integral line 207
  17. lemma OAI.Coulomb.one_body_tensor_integral line 220
  18. lemma OAI.Coulomb.one_body_tensor_integrable line 232
  19. lemma OAI.Coulomb.determinant_bilinear_expansion line 244
  20. lemma OAI.Coulomb.determinant_one_body_expansion line 259
  21. lemma OAI.Coulomb.determinant_one_body_integrable line 276
  22. lemma OAI.Coulomb.determinant_one_body_integral line 291