OAI/Analysis/CircleDomains/Uniformization/MetricConformality.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Metric conformality in the concrete sphere charts

Metric conformality records the pullback Gram matrix and positive orientation of the actual real differential. When the source metric is a positive scalar multiple of the Euclidean metric, these equations imply the complex Cauchy--Riemann equation and a nonzero derivative.

  1. def OAI.CircleDomainRigidity.sphereLocalMap line 24
  2. def OAI.CircleDomainRigidity.sphereChartMetric line 27
  3. def OAI.CircleDomainRigidity.IsMetricConformalAt line 31
  4. theorem OAI.CircleDomainRigidity.complex_linear_of_positive_orthogonal_columns line 40
  5. theorem OAI.CircleDomainRigidity.IsMetricConformalAt.isConformalAt line 74
  6. theorem OAI.CircleDomainRigidity.metric_conformal_on_spherical_background line 88