OAI/Analysis/CoulombRadii/Packets/CoulombKernel.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NeutralAtom.coulombKernel line 15
  2. def OAI.NeutralAtom.potentialOf line 17
  3. def OAI.NeutralAtom.kernelBallMass line 20
  4. theorem OAI.NeutralAtom.coulombKernel_nonneg line 22
  5. theorem OAI.NeutralAtom.measurable_coulombKernel line 25
  6. theorem OAI.NeutralAtom.coulombKernel_integrableOn_ball line 28
  7. theorem OAI.NeutralAtom.radial_integral_exterior line 37
  8. theorem OAI.NeutralAtom.radial_integrable_exterior line 65
  9. def OAI.NeutralAtom.regularizedKernel line 86
  10. def OAI.NeutralAtom.regularizedCharge line 89
  11. theorem OAI.NeutralAtom.contDiff_regularizedKernel line 92
  12. theorem OAI.NeutralAtom.laplacian_regularizedKernel line 99
  13. def OAI.NeutralAtom.chargePrimitive line 130
  14. theorem OAI.NeutralAtom.hasDerivAt_chargePrimitive line 132
  15. theorem OAI.NeutralAtom.chargePrimitive_eq_ratio line 147
  16. theorem OAI.NeutralAtom.tendsto_chargePrimitive line 160
  17. theorem OAI.NeutralAtom.integrable_radial_regularizedCharge_one line 170
  18. theorem OAI.NeutralAtom.integral_radial_regularizedCharge_one line 175
  19. theorem OAI.NeutralAtom.regularizedCharge_one_eq line 183
  20. theorem OAI.NeutralAtom.integrable_regularizedCharge_one line 188
  21. theorem OAI.NeutralAtom.integral_regularizedCharge_one line 194
  22. theorem OAI.NeutralAtom.regularizedCharge_smul line 207
  23. theorem OAI.NeutralAtom.integral_regularizedCharge_scale line 220
  24. theorem OAI.NeutralAtom.regularizedCharge_nonneg line 232
  25. theorem OAI.NeutralAtom.continuous_regularizedCharge_one line 235
  26. theorem OAI.NeutralAtom.regularizedCharge_tendsto_dirac line 244
  27. theorem OAI.NeutralAtom.locallyIntegrable_coulombKernel line 267
  28. theorem OAI.NeutralAtom.coulombKernel_eq_rpow line 273
  29. theorem OAI.NeutralAtom.regularizedKernel_le line 278
  30. theorem OAI.NeutralAtom.regularizedKernel_nonneg line 284
  31. theorem OAI.NeutralAtom.regularizedKernel_tendsto line 287
  32. theorem OAI.NeutralAtom.regularizedKernel_integral_tendsto line 296
  33. theorem OAI.NeutralAtom.integral_coulombKernel_laplacian line 316
  34. theorem OAI.NeutralAtom.integrable_coulomb_test_product line 338
  35. theorem OAI.NeutralAtom.coordinateLaplacian_translate line 381
  36. theorem OAI.NeutralAtom.integral_translated_coulombKernel_laplacian line 386
  37. theorem OAI.NeutralAtom.potentialOf_weakLaplacian line 397
  38. theorem OAI.NeutralAtom.bounded_density_convolution line 418