OAI/Geometry/Perimeter/Regularity/HarmonicTaylor.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RPISingularHarnack.compactSupport_bounded_derivative line 12
  2. theorem OAI.RPISingularHarnack.compact_kernel_bounded_second line 19
  3. theorem OAI.RPISingularHarnack.kernel_derivative_lipschitz line 25
  4. theorem OAI.RPISingularHarnack.kernel_taylor_of_derivative_lipschitz line 34
  5. theorem OAI.RPISingularHarnack.compact_kernel_uniform_taylor line 47
  6. def OAI.RPISingularHarnack.kernelLinear line 55
  7. theorem OAI.RPISingularHarnack.kernelLinear_integrable line 58
  8. theorem OAI.RPISingularHarnack.kernelLinear_apply line 66
  9. theorem OAI.RPISingularHarnack.convolution_uniform_taylor line 71