OAI/Analysis/CoulombRadii/Localization/TruncatedCoulomb.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Coulomb.coulombKernel_nonneg line 46
  2. lemma OAI.Coulomb.coulombKernel_measurable line 47
  3. lemma OAI.Coulomb.coulombKernel_integrableOn_ball line 48
  4. lemma OAI.Coulomb.coulombKernel_ball_integral line 53
  5. def OAI.Coulomb.truncatedCoulomb line 85
  6. lemma OAI.Coulomb.truncatedCoulomb_nonneg line 87
  7. lemma OAI.Coulomb.truncatedCoulomb_integrable line 89
  8. lemma OAI.Coulomb.truncatedCoulomb_integral line 91
  9. lemma OAI.Coulomb.coulomb_integrand_bound line 96
  10. lemma OAI.Coulomb.coulomb_convolution_integrable line 107
  11. lemma OAI.Coulomb.coulomb_convolution_bound line 118
  12. lemma OAI.Coulomb.coulomb_signed_convolution_integrable line 131
  13. lemma OAI.Coulomb.coulomb_pair_integrable line 141
  14. lemma OAI.Coulomb.compact_coulomb_cross_integrable line 168
  15. lemma OAI.Coulomb.flatSpinOrbital_coulomb_cross_integrable line 188