OAI/Analysis/CircleDomains/Sobolev/CircleComplexEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Transport the actual smoothed stream to the complex physical chart. Its two L2 partial derivatives give finite full differential energy.

  1. theorem OAI.CircleDomainRigidity.complexPlaneCoordinates_symm_measurePreserving line 18
  2. theorem OAI.CircleDomainRigidity.smooth_circle_complex_energy_finite line 23