OAI/Analysis/CoulombRadii/ThomasFermi/LpParameter.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Coulomb.aestronglyMeasurable_of_dist line 14
  2. lemma OAI.Coulomb.tfField_parameter_aestronglyMeasurable line 33
  3. lemma OAI.Coulomb.coreScreenedField_memLp line 57
  4. def OAI.Coulomb.coreTFField line 77
  5. lemma OAI.Coulomb.coreTFField_coe line 82
  6. lemma OAI.Coulomb.coreScreenedField_normalized_slice_joint line 87
  7. lemma OAI.Coulomb.coreTFField_slice_aestronglyMeasurable line 98
  8. lemma OAI.Coulomb.continuous_tfEnergy_joint line 118
  9. lemma OAI.Coulomb.continuous_tfMass line 125
  10. lemma OAI.Coulomb.integral_tfDensity line 139
  11. lemma OAI.Coulomb.localTFEnergy_nonpos line 145
  12. lemma OAI.Coulomb.localTFEnergy_abs_bound line 153
  13. lemma OAI.Coulomb.localTFMass_bound line 167
  14. lemma OAI.Coulomb.conditional_localTF_integrable line 176
  15. lemma OAI.Coulomb.coreTF_conditional_integrable line 213