OAI/Analysis/CoulombRadii/FieldAnalysis/RestrictedField.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Coulomb.restrictedCorePotential line 13
  2. lemma OAI.Coulomb.restrictedCore_integrable line 17
  3. lemma OAI.Coulomb.restrictedCorePotential_nonneg line 23
  4. lemma OAI.Coulomb.restrictedCorePotential_le line 34
  5. lemma OAI.Coulomb.restrictedCorePotential_mono line 46
  6. lemma OAI.Coulomb.restrictedCorePotential_eq line 60
  7. lemma OAI.Coulomb.restrictedCorePotential_aestronglyMeasurable line 73
  8. lemma OAI.Coulomb.restrictedCore_density_prod_integrable line 87
  9. lemma OAI.Coulomb.restrictedCorePotential_mul_integrable line 96
  10. lemma OAI.Coulomb.restrictedCorePotential_fubini line 112
  11. lemma OAI.Coulomb.restrictedCorePotential_ballCloud line 153
  12. def OAI.Coulomb.restrictedOutPotential line 170
  13. lemma OAI.Coulomb.restrictedOutPotential_nonneg line 173
  14. lemma OAI.Coulomb.restrictedOutPotential_mono line 179
  15. def OAI.Coulomb.recordedFarField line 188
  16. lemma OAI.Coulomb.recordedFarField_le_attraction line 192
  17. lemma OAI.Coulomb.recordedFarField_anti line 197
  18. lemma OAI.Coulomb.coreField_le_far_addback line 203