OAI/Analysis/CoulombRadii/ThomasFermi/TfFunctional.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Coulomb.tfFunctional line 26
2. lemma OAI.Coulomb.tfFunctional_continuous line 29
3. lemma OAI.Coulomb.tfFunctional_midpoint line 34
4. lemma OAI.Coulomb.tfFunctional_midpoint_nonneg line 42
5. lemma OAI.Coulomb.tfFunctional_lower line 49
6. lemma OAI.Coulomb.tf_superlinear_bound line 56
7. lemma OAI.Coulomb.tfFunctional_bddBelow line 77
8. lemma OAI.Coulomb.tfFunctional_sublevel_bound line 91