OAI/Geometry/Perimeter/Regularity/HarmonicKernel.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RPISingularHarnack.harmonicKernelRaw line 12
  2. def OAI.RPISingularHarnack.harmonicKernelMass line 13
  3. theorem OAI.RPISingularHarnack.harmonicKernelRaw_contDiff line 15
  4. theorem OAI.RPISingularHarnack.harmonicKernelRaw_tsupport line 18
  5. theorem OAI.RPISingularHarnack.harmonicKernelRaw_compact line 24
  6. theorem OAI.RPISingularHarnack.harmonicKernelMass_pos line 27
  7. def OAI.RPISingularHarnack.harmonicKernel line 33
  8. theorem OAI.RPISingularHarnack.harmonicKernel_contDiff line 35
  9. theorem OAI.RPISingularHarnack.harmonicKernel_tsupport line 38
  10. theorem OAI.RPISingularHarnack.harmonicKernel_compact line 44
  11. theorem OAI.RPISingularHarnack.harmonicKernel_integral line 47
  12. def OAI.RPISingularHarnack.scaledHarmonicKernel line 51
  13. theorem OAI.RPISingularHarnack.scaledHarmonicKernel_contDiff line 53
  14. theorem OAI.RPISingularHarnack.scaledHarmonicKernel_eq line 57
  15. theorem OAI.RPISingularHarnack.scaledHarmonicKernel_integral line 63
  16. theorem OAI.RPISingularHarnack.scaledHarmonicKernel_tsupport line 73
  17. theorem OAI.RPISingularHarnack.scaledHarmonicKernel_bound line 83
  18. theorem OAI.RPISingularHarnack.shifted_scaledHarmonicKernel_integral line 91
  19. theorem OAI.RPISingularHarnack.shifted_scaledHarmonicKernel_support line 96