OAI/Analysis/CoulombRadii/ThomasFermi/TfFunctionalGapControl.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Coulomb.tfFunctional_gap_control line 31
  2. lemma OAI.Coulomb.tfFunctional_exists_minimizer line 65
  3. lemma OAI.Coulomb.tfFunctional_minimizer_unique line 76
  4. abbrev OAI.Coulomb.TFFieldExponent line 98
  5. instance OAI.Coulomb.(instance at line 99) line 99
  6. abbrev OAI.Coulomb.TFLq line 100
  7. lemma OAI.Coulomb.tfLq_norm line 102
  8. def OAI.Coulomb.tfFieldPairing line 108
  9. lemma OAI.Coulomb.tfFieldPairing_integrable line 109
  10. lemma OAI.Coulomb.tfFieldPairing_bound line 112
  11. lemma OAI.Coulomb.tfFieldPairing_add_left line 119
  12. lemma OAI.Coulomb.tfFieldPairing_smul_left line 126
  13. lemma OAI.Coulomb.tfFieldPairing_add_right line 133
  14. lemma OAI.Coulomb.tfFieldPairing_smul_right line 140
  15. def OAI.Coulomb.tfFieldLinear line 148
  16. def OAI.Coulomb.tfFieldContinuous line 151
  17. lemma OAI.Coulomb.tfFieldContinuous_apply line 155
  18. lemma OAI.Coulomb.tfFieldContinuous_bound line 157
  19. def OAI.Coulomb.tfEnergy line 167
  20. lemma OAI.Coulomb.tfEnergy_formula line 170
  21. lemma OAI.Coulomb.tfEnergy_exists_unique_minimizer line 177