OAI/Analysis/CoulombRadii/Variational/Axis.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.NeutralAtom.second_deriv_nonpos_of_local_max line 13
  2. def OAI.NeutralAtom.axis line 28
  3. def OAI.NeutralAtom.coordinateLaplacian line 30
  4. theorem OAI.NeutralAtom.coordinateLaplacian_nonpos_of_local_max line 33
  5. theorem OAI.NeutralAtom.norm_sq_axis_shift line 44
  6. theorem OAI.NeutralAtom.second_deriv_quadratic_rpow line 51
  7. def OAI.NeutralAtom.radialPower line 80
  8. theorem OAI.NeutralAtom.coordinateLaplacian_radialPower line 82
  9. theorem OAI.NeutralAtom.deriv_affine_line line 110
  10. theorem OAI.NeutralAtom.second_deriv_affine_line line 117
  11. theorem OAI.NeutralAtom.coordinateLaplacian_reflect line 132
  12. def OAI.NeutralAtom.dirPartial line 155
  13. theorem OAI.NeutralAtom.contDiff_partial line 158
  14. theorem OAI.NeutralAtom.hasCompactSupport_partial line 162
  15. theorem OAI.NeutralAtom.partial_convolution line 165
  16. theorem OAI.NeutralAtom.coordinateLaplacian_eq_partials line 175
  17. theorem OAI.NeutralAtom.coordinateLaplacian_convolution line 182
  18. theorem OAI.NeutralAtom.dirPartial_sub line 210
  19. theorem OAI.NeutralAtom.coordinateLaplacian_sub line 216
  20. theorem OAI.NeutralAtom.coordinateLaplacian_quadratic line 229
  21. def OAI.NeutralAtom.WeakLaplacianLower line 254
  22. theorem OAI.NeutralAtom.normed_bump_reflect_tsupport line 259
  23. theorem OAI.NeutralAtom.continuous_convolution_comm line 268
  24. theorem OAI.NeutralAtom.weakLaplacianLower_mollify line 276
  25. theorem OAI.NeutralAtom.integrable_normed_bump_reflect line 291
  26. theorem OAI.NeutralAtom.mollify_le_of_bound line 298
  27. theorem OAI.NeutralAtom.no_maximum_of_strict_weakLaplacian line 316
  28. theorem OAI.NeutralAtom.coordinateLaplacian_congr_nhds line 383
  29. theorem OAI.NeutralAtom.coordinateLaplacian_zero line 393
  30. theorem OAI.NeutralAtom.coordinateLaplacian_eq_zero_of_notMem_tsupport line 397