OAI/Analysis/CoulombRadii/FieldAnalysis/Occupancy.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Coulomb.occupancy line 53
  2. def OAI.Coulomb.bernoulliWeight line 54
  3. lemma OAI.Coulomb.bernoulliWeight_nonneg line 56
  4. lemma OAI.Coulomb.bernoulli_product_mean line 64
  5. lemma OAI.Coulomb.bernoulliWeight_sum line 72
  6. lemma OAI.Coulomb.bernoulli_forced_mean line 75
  7. lemma OAI.Coulomb.bernoulli_one_mean line 88
  8. lemma OAI.Coulomb.bernoulli_two_mean line 91
  9. lemma OAI.Coulomb.bernoulli_linear_mean line 94
  10. lemma OAI.Coulomb.bernoulli_pair_mean line 101
  11. def OAI.Coulomb.occupiedIndex line 122
  12. lemma OAI.Coulomb.sum_occupiedIndex line 126
  13. lemma OAI.Coulomb.sum_occupiedIndex_real line 135
  14. def OAI.Coulomb.slaterPairEntry line 142
  15. lemma OAI.Coulomb.slaterPairEntry_self line 149
  16. lemma OAI.Coulomb.slaterWave_two_body_exact line 153
  17. lemma OAI.Coulomb.bernoulli_slater_pair_mean line 179