OAI/Analysis/CircleDomains/Sobolev/PlanarSobolevTransport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Transport the actual planar weak derivative identities to the Euclidean coordinates of the repository's Sobolev approximation library.

  1. theorem OAI.CircleDomainRigidity.weakPartial_of_planar_identity line 17
  2. theorem OAI.CircleDomainRigidity.memW1p_of_rectangle_weak_gradient line 68