OAI/Analysis/CircleDomains/Sobolev/MetricChartEnergy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Energy of the actual metric-conformal chart differential

The Gram equations defining metric conformality identify the source metric with a scalar multiple of the pulled-back Euclidean metric. Consequently the covector energy changes by the positive Jacobian.

  1. def OAI.CircleDomainRigidity.complexRealMatrix line 22
  2. theorem OAI.CircleDomainRigidity.det_complexRealMatrix line 25
  3. theorem OAI.CircleDomainRigidity.metric_eq_scaled_chart_gram line 30
  4. theorem OAI.CircleDomainRigidity.IsMetricConformalAt.covectorEnergy line 50