OAI/Analysis/CircleDomains/Sobolev/TransportedRealEnergy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite-chart energy of the actual transported real function

Both integrability and the energy identity follow from the Jacobian formula. Restriction to the bounded disk used by line payment only decreases this energy.

  1. theorem OAI.CircleDomainRigidity.transported_sphereRealFunction_eq line 24
  2. theorem OAI.CircleDomainRigidity.transported_real_energy line 32
  3. theorem OAI.CircleDomainRigidity.transported_real_energy_on_disk_le line 73