OAI/Analysis/CircleDomains/Sobolev/SphereRealDifferential.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The finite real chart of a metric-conformal sphere map

This identifies the actual real derivative matrix of the finite-chart map with the complex chart derivative used in metric conformality.

  1. def OAI.CircleDomainRigidity.sphereRealMap line 22
  2. def OAI.CircleDomainRigidity.complexToRealDerivative line 25
  3. theorem OAI.CircleDomainRigidity.planeMatrix_complexToRealDerivative line 29
  4. theorem OAI.CircleDomainRigidity.sphereRealMap_hasFDerivAt line 34
  5. theorem OAI.CircleDomainRigidity.metric_conformal_real_chart line 57
  6. theorem OAI.CircleDomainRigidity.sphereRealMap_injOn line 90