OAI/Analysis/CoulombRadii/Variational/CorrectionDensity.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.NeutralAtom.coulombKernel_le_one line 16
  2. theorem OAI.NeutralAtom.coulombKernel_sq_integrableOn_ball line 19
  3. theorem OAI.NeutralAtom.coulombKernel_sub_le line 28
  4. theorem OAI.NeutralAtom.potentialOf_lipschitz_bound line 51
  5. theorem OAI.NeutralAtom.potentialOf_lipschitz line 82
  6. theorem OAI.NeutralAtom.potentialOf_continuous line 91
  7. theorem OAI.NeutralAtom.translated_kernel_indicator_eq line 96
  8. theorem OAI.NeutralAtom.translated_kernel_indicator_integrable line 104
  9. theorem OAI.NeutralAtom.translated_kernel_indicator_integral line 111
  10. theorem OAI.NeutralAtom.kernelBallMass_nonneg line 118
  11. theorem OAI.NeutralAtom.potential_integrable_and_bound line 121
  12. theorem OAI.NeutralAtom.potential_le_inner_mass line 152
  13. theorem OAI.NeutralAtom.integral_exterior_inverse_sixth line 179
  14. theorem OAI.NeutralAtom.integrable_exterior_inverse_sixth line 194
  15. theorem OAI.NeutralAtom.potentialOf_nonneg line 205
  16. theorem OAI.NeutralAtom.inner_potential_tendsto_zero line 208
  17. theorem OAI.NeutralAtom.potential_tendsto_zero_of_local_bound line 219
  18. def OAI.NeutralAtom.correctionDensity line 229
  19. theorem OAI.NeutralAtom.correctionDensity_nonneg line 232
  20. theorem OAI.NeutralAtom.correctionDensity_measurable line 238
  21. theorem OAI.NeutralAtom.correctionDensity_le_exterior line 244
  22. theorem OAI.NeutralAtom.correctionDensity_integrable_and_mass line 265
  23. theorem OAI.NeutralAtom.correctionDensity_mass_bound line 279
  24. theorem OAI.NeutralAtom.correctionDensity_local_bound line 291
  25. theorem OAI.NeutralAtom.correction_potential_tendsto_zero line 307
  26. def OAI.NeutralAtom.WeakNuclearSubsolution line 332
  27. theorem OAI.NeutralAtom.integrable_mul_test_on line 338
  28. theorem OAI.NeutralAtom.integral_coordinateLaplacian line 345
  29. theorem OAI.NeutralAtom.corrected_test_identity line 352
  30. theorem OAI.NeutralAtom.cancel_nuclear_source line 408