OAI/Analysis/CircleDomains/Sobolev/MetricComposition.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Metric conformality after a holomorphic change of target

The actual chart differential is multiplied by the nonzero complex derivative of the target map. Its Gram matrix is consequently multiplied by the squared norm of that derivative, and its orientation stays positive.

  1. theorem OAI.CircleDomainRigidity.complex_mul_column_norm line 20
  2. theorem OAI.CircleDomainRigidity.complex_mul_column_dot line 26
  3. theorem OAI.CircleDomainRigidity.complex_mul_column_det line 32
  4. theorem OAI.CircleDomainRigidity.complex_column_norm_pos line 38
  5. theorem OAI.CircleDomainRigidity.IsMetricConformalAt.comp_conformal line 46