OAI/Analysis/CoulombRadii/FieldAnalysis/FermionicNear.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Coulomb.nearWeight line 17
  2. def OAI.Coulomb.nearPotential line 19
  3. lemma OAI.Coulomb.nearWeight_nonneg line 21
  4. lemma OAI.Coulomb.nearWeight_measurable line 24
  5. lemma OAI.Coulomb.nearWeight_le line 26
  6. lemma OAI.Coulomb.nearPotential_nonneg line 29
  7. lemma OAI.Coulomb.nearPotential_integrable line 31
  8. lemma OAI.Coulomb.nearPotential_physical line 44
  9. def OAI.Coulomb.fermionicNearConstant line 70
  10. lemma OAI.Coulomb.fermionicNearConstant_nonneg line 71
  11. lemma OAI.Coulomb.nearPotential_normalized line 73
  12. lemma OAI.Coulomb.rpow_three_fifths_linear line 107
  13. theorem OAI.Coulomb.nearPotential_linear line 121
  14. lemma OAI.Coulomb.nearWeight_site_integrable line 150
  15. lemma OAI.Coulomb.nearPotential_outer_integrable line 162
  16. theorem OAI.Coulomb.outer_nearPotential_linear line 168
  17. lemma OAI.Coulomb.supported_core_nearPotential line 192
  18. lemma OAI.Coulomb.nearPotential_reindex line 210
  19. lemma OAI.Coulomb.nearPotential_measurable line 215
  20. lemma OAI.Coulomb.RecordedEnsemble.Conserves.nearPotential line 218
  21. theorem OAI.Coulomb.RecordedEnsemble.nearPotential_le line 226