OAI/Analysis/CoulombRadii/FieldAnalysis/UnitNucleus.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Coulomb.unitNucleus line 65
  2. lemma OAI.Coulomb.attraction_unitNucleus line 72
  3. lemma OAI.Coulomb.crossPotential_nuclear line 76
  4. lemma OAI.Coulomb.crossPotential_slice_integrable line 85
  5. lemma OAI.Coulomb.crossPotential_spin_integral line 90
  6. lemma OAI.Coulomb.tensor_cross_prod_integrable line 100
  7. lemma OAI.Coulomb.cross_integral_core_integrable line 114
  8. lemma OAI.Coulomb.crossEnergy_iterated line 125
  9. lemma OAI.Coulomb.cross_core_integrable line 150
  10. lemma OAI.Coulomb.crossEnergy_core line 156
  11. def OAI.Coulomb.coreInteractionDensity line 167
  12. lemma OAI.Coulomb.selectedSlater_spatialSupport line 171
  13. lemma OAI.Coulomb.bernoulli_core_cross_mean line 189
  14. theorem OAI.Coulomb.finite_fermi_core_trial line 216