OAI/Analysis/CircleDomains/Sobolev/SmoothPlaneSobolev.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Smoothness on an open plane set and integrable partial derivatives give an actual Sobolev witness.

  1. theorem OAI.CircleDomainRigidity.integrable_plane_mul_of_continuousOn line 14
  2. theorem OAI.CircleDomainRigidity.weakPartial_of_smooth_on line 21
  3. def OAI.CircleDomainRigidity.smoothPlaneSobolevWitness line 47
  4. def OAI.DeGiorgi.MemW1pWitness.sub line 61