OAI/Analysis/CircleDomains/Sobolev/SmoothPhysicalPullback.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Smooth quasiconformal pullback energy in the actual physical plane. Only the finite compact-set estimate needed for the limiting scalar transport is asserted.

  1. def OAI.CircleDomainRigidity.physicalSmoothEnergy line 16
  2. lemma OAI.CircleDomainRigidity.physicalSmoothEnergy_eq_complex line 20
  3. lemma OAI.CircleDomainRigidity.physicalSmoothEnergy_integral line 30
  4. lemma OAI.CircleDomainRigidity.physicalHomeomorph_contDiff line 47
  5. lemma OAI.CircleDomainRigidity.physicalSmoothPullback_energy line 52