OAI/Analysis/CircleDomains/Sobolev/SmoothRealLift.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A continuous real lift of a smooth circle map is automatically smooth, with exactly its intrinsic differential and no additional energy cost.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.contDiffOn_real_lift line 16
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.fderiv_real_lift line 31
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.real_lift_energy_le line 43