OAI/Analysis/CoulombRadii/Localization/HarmonicInterior.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.NeutralAtom.dirPartial_mul line 12
2. theorem OAI.NeutralAtom.dirPartial_add line 19
3. theorem OAI.NeutralAtom.coordinateLaplacian_mul line 26
4. theorem OAI.NeutralAtom.dirPartial_regularizedKernel line 56
5. def OAI.NeutralAtom.coulombPartial line 81
6. theorem OAI.NeutralAtom.regularizedPartial_tendsto line 84
7. theorem OAI.NeutralAtom.dirPartial_regularizedKernel_bound line 93
8. theorem OAI.NeutralAtom.locallyIntegrable_coulombKernel_sq line 109
9. theorem OAI.NeutralAtom.regularizedPartial_integral_tendsto line 116
10. theorem OAI.NeutralAtom.weak_harmonic_reproduction line 138
11. def OAI.NeutralAtom.cutoffHarmonicKernel line 208
12. theorem OAI.NeutralAtom.contDiffAt_coulombKernel line 212
13. theorem OAI.NeutralAtom.contDiffAt_coulombPartial line 220
14. theorem OAI.NeutralAtom.contDiff_coordinateLaplacian line 225
15. theorem OAI.NeutralAtom.cutoffHarmonicKernel_eq_zero_of_eventually_const line 238
16. theorem OAI.NeutralAtom.hasCompactSupport_cutoffHarmonicKernel line 249
17. theorem OAI.NeutralAtom.contDiff_cutoffHarmonicKernel line 258
18. theorem OAI.NeutralAtom.coulombPartial_bound line 279
19. theorem OAI.NeutralAtom.measurable_coulombPartial line 290
20. theorem OAI.NeutralAtom.coulombPartial_integrable_mul_compact line 294
21. theorem OAI.NeutralAtom.weak_harmonic_reproduction_kernel line 306
22. theorem OAI.NeutralAtom.coordinateLaplacian_sub_right line 334
23. theorem OAI.NeutralAtom.HasWeakLaplacian.translate line 345
24. theorem OAI.NeutralAtom.weak_harmonic_reproduction_at line 366
25. theorem OAI.NeutralAtom.harmonic_value_bound line 378
26. theorem OAI.NeutralAtom.harmonic_difference_bound line 405
27. theorem OAI.NeutralAtom.harmonic_interior_estimates line 447
28. theorem OAI.NeutralAtom.HasWeakLaplacian.congrOn line 493
29. theorem OAI.NeutralAtom.harmonic_interior_estimates_local line 507