OAI/Analysis/CoulombRadii/Variational/WeakLaplacian.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.NeutralAtom.WeakLaplacianLower.congr line 15
  2. theorem OAI.NeutralAtom.WeakLaplacianLower.mono line 25
  3. theorem OAI.NeutralAtom.no_maximum_of_strict_weakLaplacian_local line 30
  4. theorem OAI.NeutralAtom.integrable_mul_compact_of_continuousAt line 45
  5. theorem OAI.NeutralAtom.tsupport_dirPartial_subset line 60
  6. theorem OAI.NeutralAtom.integral_mul_coordinateLaplacian_eq line 63
  7. theorem OAI.NeutralAtom.continuousAt_coordinateLaplacian line 135
  8. theorem OAI.NeutralAtom.continuous_coordinateLaplacian line 151
  9. theorem OAI.NeutralAtom.hasCompactSupport_coordinateLaplacian line 155
  10. def OAI.NeutralAtom.HasWeakLaplacian line 162
  11. theorem OAI.NeutralAtom.HasWeakLaplacian.mono line 166
  12. theorem OAI.NeutralAtom.HasWeakLaplacian.sub_smooth_lower line 171
  13. theorem OAI.NeutralAtom.weakLaplacian_le_at_local_max line 210
  14. theorem OAI.NeutralAtom.coordinateLaplacian_neg line 242
  15. theorem OAI.NeutralAtom.HasWeakLaplacian.neg line 252
  16. theorem OAI.NeutralAtom.weakLaplacian_ge_at_local_min line 258
  17. theorem OAI.NeutralAtom.coordinateLaplacian_add_at line 270
  18. theorem OAI.NeutralAtom.coordinateLaplacian_const_mul line 292
  19. def OAI.NeutralAtom.punctured line 297
  20. theorem OAI.NeutralAtom.isOpen_punctured line 299
  21. theorem OAI.NeutralAtom.contDiffOn_radialPower line 301
  22. def OAI.NeutralAtom.radialBarrier line 306
  23. theorem OAI.NeutralAtom.contDiffOn_radialBarrier line 309
  24. theorem OAI.NeutralAtom.radialBarrier_scaled line 314
  25. theorem OAI.NeutralAtom.laplacian_radialBarrier_scaled line 320
  26. def OAI.NeutralAtom.radialPenalty line 335
  27. theorem OAI.NeutralAtom.radialPenalty_pos line 337
  28. theorem OAI.NeutralAtom.continuousOn_radialPenalty line 341
  29. theorem OAI.NeutralAtom.exists_penalized_max line 345
  30. theorem OAI.NeutralAtom.exists_penalized_min line 411