OAI/Geometry/Perimeter/Regularity/EllipticCurl.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RPISingularHarnack.scalarDirection line 12
  2. theorem OAI.RPISingularHarnack.scalarDirection_contDiff line 14
  3. theorem OAI.RPISingularHarnack.scalarDirection_tsupport line 18
  4. theorem OAI.RPISingularHarnack.scalarDirection_fderiv line 25
  5. def OAI.RPISingularHarnack.directionLocalTest line 33
  6. def OAI.RPISingularHarnack.curlTest line 38
  7. theorem OAI.RPISingularHarnack.curlTest_contDiff line 41
  8. theorem OAI.RPISingularHarnack.curlTest_tsupport line 46
  9. theorem OAI.RPISingularHarnack.curlTest_divergence line 53
  10. def OAI.RPISingularHarnack.curlTestLp line 64
  11. theorem OAI.RPISingularHarnack.curlTestLp_ae line 69
  12. def OAI.RPISingularHarnack.CurlFreeLpOn line 72
  13. theorem OAI.RPISingularHarnack.testGradient_curlTest_inner line 75
  14. theorem OAI.RPISingularHarnack.testGradientSpace_curlFree line 91
  15. theorem OAI.RPISingularHarnack.CurlFreeLpOn.sub line 101
  16. theorem OAI.RPISingularHarnack.weak_curl_harmonic_comparison line 106