OAI/Analysis/CircleDomains/Sobolev/EnergyChangeCoordinates.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The energy density under a change of coordinates

Pulling back a covector and its metric multiplies the planar Dirichlet energy density by the absolute Jacobian determinant. Positive scalar changes of metric have no effect in dimension two.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.covectorEnergy_pos_smul line 20
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.covectorEnergy_pullback line 25
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.pullback_metric_posDef line 45
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.covectorEnergy_conformal_pullback line 51