OAI/Analysis/CoulombRadii/ThomasFermi/TfFunctionalUniformBound.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.tfFunctional_uniform_bound line 49
2. lemma OAI.Coulomb.tfFunctional_minimizer_gap line 62
3. lemma OAI.Coulomb.tfFunctional_minimizers_tendsto line 80
4. lemma OAI.Coulomb.tf_complementarity_solve line 121
5. lemma OAI.Coulomb.tfEuler_equation line 137
6. def OAI.Coulomb.tfMinimizer line 152
7. lemma OAI.Coulomb.tfMinimizer_nonneg line 154
8. lemma OAI.Coulomb.tfMinimizer_min line 156
9. lemma OAI.Coulomb.tfMinimizer_unique line 159
10. lemma OAI.Coulomb.tfMinimizer_continuous line 163
11. lemma OAI.Coulomb.tfMinimizer_measurable line 169
12. lemma OAI.Coulomb.tf_power_tangent line 182
13. def OAI.Coulomb.tfBregman line 191
14. lemma OAI.Coulomb.tfKinetic_pair_integrable line 193
15. lemma OAI.Coulomb.tfBregman_integrable line 198
16. lemma OAI.Coulomb.tfBregman_formula line 207
17. lemma OAI.Coulomb.tfBregman_nonneg line 220
18. lemma OAI.Coulomb.tfEnergy_expansion line 227
19. lemma OAI.Coulomb.tfEnergy_minimizer_expansion line 250
20. lemma OAI.Coulomb.tfEnergy_gap_controls line 262