OAI/Analysis/CircleDomains/Sobolev/CoordinateEnergy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The separate coordinate energies in the chosen metric

The inverse-matrix trace density is exactly the sum of the nonnegative squared covector norms. Thus control of the Gram energy controls every coordinate, and in the identity metric these are the usual squared Euclidean differential norms.

  1. def OAI.CircleDomainRigidity.FiniteTransfer.covectorEnergy line 21
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.covectorEnergy_eq_matrixEnergy line 24
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.covectorEnergy_nonneg line 29
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.covectorEnergy_identity line 34
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.gramEnergy_eq_sum_covectorEnergy line 38
  6. theorem OAI.CircleDomainRigidity.FiniteTransfer.covectorEnergy_le_gramEnergy line 45
  7. theorem OAI.CircleDomainRigidity.FiniteTransfer.gramEnergy_nonneg line 52