OAI/Analysis/CircleDomains/Sobolev/ComplexSobolevTransport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The two physical complex-coordinate derivative identities give the Euclidean-plane weak derivatives, with the same area measure.

  1. theorem OAI.CircleDomainRigidity.complexPlaneCoordinates_zero line 13
  2. theorem OAI.CircleDomainRigidity.complexPlaneCoordinates_one line 19
  3. theorem OAI.CircleDomainRigidity.complexPlaneCoordinates_measurePreserving line 25
  4. theorem OAI.CircleDomainRigidity.weakPartial_of_complex_identity line 30