OAI/Analysis/CircleDomains/Sobolev/EnergyTransportIntegrability.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Integrability in the metric energy change of variables

The Jacobian theorem gives integrability equivalence as well as equality of integrals. This supplies the target finite-energy hypotheses required by parallel-line payment from the actual source energy estimates.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.integrable_covectorEnergy_change_variables_iff line 24
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.integrable_circleEnergy_change_variables_iff line 44
  3. theorem OAI.CircleDomainRigidity.integrable_filled_circleEnergy_metric_sphere_map_iff line 69
  4. theorem OAI.CircleDomainRigidity.integrable_transported_real_coordinate_iff line 96