OAI/Analysis/CircleDomains/Sobolev/SobolevConformalTransport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Continuous compactly supported Sobolev functions can be transported by the actual smooth conformal inverse. The local target witness has at most the source energy; no smoothness of the original test is assumed.

  1. theorem OAI.CircleDomainRigidity.planarMollification_tendsto_of_continuous line 18
  2. theorem OAI.CircleDomainRigidity.sobolev_conformal_transport line 28