OAI/Analysis/CoulombRadii/FieldAnalysis/FiniteProdSum.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.finiteProd_sum line 53
2. lemma OAI.Coulomb.finite_weighted_bilinear_integrable line 58
3. lemma OAI.Coulomb.exists_le_weighted_average line 74
4. lemma OAI.Coulomb.finiteFermiDensity_direct_flat line 84
5. lemma OAI.Coulomb.bernoulli_slater_pairEnergy_upper line 116
6. lemma OAI.Coulomb.bernoulli_slater_form_upper line 156
7. theorem OAI.Coulomb.finite_fermi_coulomb_trial line 173