OAI/Analysis/CircleDomains/Sobolev/SmoothImageArea.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The smooth Jacobian boundary integral is the signed area of the actual image curve, expressed using its real and imaginary coordinates.

  1. def OAI.CircleDomainRigidity.signedCurveArea line 12
  2. theorem OAI.CircleDomainRigidity.complex_real_linear_decomposition line 15
  3. theorem OAI.CircleDomainRigidity.signedCurveArea_smooth_image line 23
  4. theorem OAI.CircleDomainRigidity.signedCurveArea_congr line 48