OAI/Geometry/Perimeter/Regularity/EllipticTestSpace.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.RPISingularHarnack.VectorL2 line 12
  2. def OAI.RPISingularHarnack.SmoothLocalTest line 14
  3. def OAI.RPISingularHarnack.testGradientLp line 17
  4. theorem OAI.RPISingularHarnack.testGradientLp_ae line 21
  5. def OAI.RPISingularHarnack.testGradientSpace line 25
  6. instance OAI.RPISingularHarnack.testGradientSpace_complete line 28
  7. theorem OAI.RPISingularHarnack.testGradient_mem line 31
  8. theorem OAI.RPISingularHarnack.inner_zero_on_closed_span line 35
  9. theorem OAI.RPISingularHarnack.testGradient_pairing_ext line 43
  10. theorem OAI.RPISingularHarnack.testGradient_inner line 52
  11. theorem OAI.RPISingularHarnack.testGradient_integrable_pairing line 59
  12. def OAI.RPISingularHarnack.DivFreeLpOn line 65
  13. theorem OAI.RPISingularHarnack.orthogonal_testGradient_divFree line 68
  14. theorem OAI.RPISingularHarnack.weak_harmonic_gradient_comparison line 74