OAI/Analysis/CircleDomains/Sobolev/SmoothPhysicalPullbackBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Global and localized energy bounds for a compact smooth scalar under the actual smooth plane homeomorphism.

  1. lemma OAI.CircleDomainRigidity.physicalSmoothPartial_memLp line 12
  2. lemma OAI.CircleDomainRigidity.physicalSmoothEnergy_integrable line 18
  3. lemma OAI.CircleDomainRigidity.physicalSmoothEnergy_nonneg line 24
  4. lemma OAI.CircleDomainRigidity.physicalSmoothPullback_energy_global line 27
  5. lemma OAI.CircleDomainRigidity.physicalSmoothPullback_energy_subset line 45