OAI/Geometry/Perimeter/Regularity/WeakHarmonicRadial.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RPISingularHarnack.WeakHarmonicOn line 12
2. theorem OAI.RPISingularHarnack.divergence_displacement line 16
3. theorem OAI.RPISingularHarnack.gradient_radialPrimitive line 22
4. theorem OAI.RPISingularHarnack.laplacian_radialPrimitive line 39
5. theorem OAI.RPISingularHarnack.radial_average_hasDerivAt line 60
6. theorem OAI.RPISingularHarnack.tsupport_gradient_subset line 93
7. theorem OAI.RPISingularHarnack.weakHarmonic_radial_derivative_zero line 97
8. theorem OAI.RPISingularHarnack.weakHarmonic_radial_average_eq line 132