OAI/Geometry/Perimeter/Regularity/PlaneWindowLift.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RPISingularHarnack.normalProjection_decomposition line 12
  2. theorem OAI.RPISingularHarnack.chartInclusion_projection line 17
  3. theorem OAI.RPISingularHarnack.norm_chartInclusion line 22
  4. def OAI.RPISingularHarnack.planeWindowLift line 25
  5. theorem OAI.RPISingularHarnack.planeWindowLift_contDiff line 28
  6. theorem OAI.RPISingularHarnack.planeWindowLift_tsupport line 34
  7. theorem OAI.RPISingularHarnack.planeWindowLift_hasCompactSupport line 52
  8. theorem OAI.RPISingularHarnack.gradient_eventuallyEq line 61
  9. theorem OAI.RPISingularHarnack.planeWindowLift_laplacian line 66