OAI/Analysis/CircleDomains/Sobolev/RealCoordinateDifferential.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual quotient pullback of a constructed real coordinate has the smoothness and differential energy used in the path-law estimates.

  1. theorem OAI.CircleDomainRigidity.PhysicalRealCoordinate.complex_differential line 21
  2. theorem OAI.CircleDomainRigidity.quotientPlaneRepresentative_zero_near_infinity line 65