OAI/Analysis/CoulombRadii/ThomasFermi/TfExtendNonneg.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Coulomb.tfExtend_nonneg line 58
  2. lemma OAI.Coulomb.tfPotential_nonneg line 65
  3. lemma OAI.Coulomb.tfPotential_restrict line 71
  4. lemma OAI.Coulomb.tfPotential_restrict_integrable line 78
  5. lemma OAI.Coulomb.tfPotential_mass_lower line 84
  6. lemma OAI.Coulomb.tfMass_nonneg line 99
  7. lemma OAI.Coulomb.tfCoulomb_mass_lower line 101
  8. lemma OAI.Coulomb.tfEnergy_mass_lower line 116
  9. lemma OAI.Coulomb.tfEnergy_sublevel_mass_bound line 131
  10. lemma OAI.Coulomb.coulombBilinear_congr_ae line 160
  11. lemma OAI.Coulomb.rawThomasFermiEnergy_congr_ae line 172
  12. lemma OAI.Coulomb.rawThomasFermiEnergy_tfExtend line 180
  13. def OAI.Coulomb.tfDensity line 201
  14. lemma OAI.Coulomb.tfDensity_nonneg line 204
  15. lemma OAI.Coulomb.tfDensity_measurable line 206
  16. lemma OAI.Coulomb.tfDensity_eq_zero line 208
  17. lemma OAI.Coulomb.tfDensity_ae_tfExtend line 210
  18. lemma OAI.Coulomb.tfDensity_memLp line 214
  19. lemma OAI.Coulomb.tfDensity_power_integrable line 218
  20. lemma OAI.Coulomb.rawThomasFermiEnergy_tfDensity line 223
  21. lemma OAI.Coulomb.thomasFermiKineticConstant_pos line 231
  22. def OAI.Coulomb.localTFMinimizer line 235
  23. lemma OAI.Coulomb.localTFMinimizer_nonneg line 238
  24. lemma OAI.Coulomb.localTFMinimizer_minimizes line 242
  25. lemma OAI.Coulomb.continuous_localTFMinimizer line 249
  26. def OAI.Coulomb.localTFDensity line 253
  27. lemma OAI.Coulomb.localTFDensity_hole line 257
  28. def OAI.Coulomb.rawTFBregman line 283
  29. lemma OAI.Coulomb.tfExtend_sub_ae line 287
  30. lemma OAI.Coulomb.coulombBilinear_tfDensity_sub line 295
  31. lemma OAI.Coulomb.rawTFBregman_congr_ae line 305
  32. lemma OAI.Coulomb.rawTFBregman_tfDensity line 314
  33. lemma OAI.Coulomb.raw_localTF_gap line 325
  34. def OAI.Coulomb.rawToTFLp line 341
  35. lemma OAI.Coulomb.rawToTFLp_nonneg line 344
  36. lemma OAI.Coulomb.tfDensity_rawToTFLp line 350
  37. lemma OAI.Coulomb.raw_localTF_gap_density line 360